chore: Update Lean to v4.34.1

Lean4Lean/Experimental/MoreStepIndexed.lean

@@ -168,7 +168,7 @@ theorem Shape.lift_self {s : Shape n} : s.lift = s := by
   have {α} {lift : α → α} (IH : ∀ {s}, lift s = s) {s} : ShapeFun.lift lift s = s := by
     simp [ShapeFun.lift]; apply List.map_id''; simp [IH]
   unfold lift <;> split <;> (try rfl) <;> dsimp
-  -- · rw [dif_pos ‹_›]
+  -- · rw [dite_eq_left ‹_›]
   · rw [Shape.lift_self, this Shape.lift_self]
   · rw [this Shape.lift_self]
 
@@ -198,7 +198,7 @@ theorem Shape.lift_le_lift {s t : Shape n} (le : n ≤ m) : (s.lift : Shape m) 
         ShapeFun.ble ble s t := by
       simp only [ShapeFun.ble, ShapeFun.lift, List.all_map, List.any_map, Function.comp_def, ih]
     -- have sif {i} (h : i ≤ n) : (if h : i ≤ m then .sort i h else .bot : Shape (m+1)) =
-    --     .sort i (Nat.le_trans h le) := dif_pos _
+    --     .sort i (Nat.le_trans h le) := dite_eq_left _
     cases s <;> cases t <;> simp [ble, lift, *]
 
 omit [Params] in

Lean4Lean/Experimental/SExpr.lean

@@ -69,7 +69,7 @@ theorem mk_of_wf (h : l.WF univs) :
   have hm : mk l = if h' : l.WF univs then
       (⟨_, l, h', rfl⟩ : SLevel) else SLevel.zero := rfl
   rw [hm]
-  exact dif_pos h
+  exact dite_eq_left h
 
 @[simp] theorem mk_reify (l : SLevel) : mk (reify l) = l := by
   rw [mk_of_wf (reify_wf l)]

Lean4Lean/Experimental/SExprParamsD2.lean

@@ -136,9 +136,9 @@ theorem addConst_le_of_le {e₁ e₂ s₁ s₂ : VEnv} {n : Name} {ci : VConstan
     have h' : (if n = n' then some ci else e₁.constants n') = some a := h
     show (if n = n' then some ci else e₂.constants n') = some a
     by_cases hn : n = n'
-    · rw [if_pos hn] at h' ⊢
+    · rw [ite_eq_left hn] at h' ⊢
       exact h'
-    · rw [if_neg hn] at h' ⊢
+    · rw [ite_eq_right hn] at h' ⊢
       exact hle.constants h'
   · exact fun h => hle.defeqs h
   · exact fun h => hle.structEtas h
@@ -1024,7 +1024,7 @@ theorem foldlM_addConst_constants_old {α : Type _} (name : α → Name)
     · cases hx
     · cases hx
       show (if name x = c then some (ci x) else _) = _
-      rw [if_neg (hne x (.head _))]
+      rw [ite_eq_right (hne x (.head _))]
 
 theorem foldl_addDefEq_constants :
     ∀ (dfs : List VDefEq) (env : VEnv) (c : Name),
@@ -1739,7 +1739,7 @@ theorem d2Imax_pos (univs : Nat) (u v : @SLevel (d2Params univs))
   have hw := hv w
   show 0 < Lean.Nat.imax (u.1 w) (v.1 w)
   simp only [Lean.Nat.imax]
-  rw [if_neg (by omega)]
+  rw [ite_eq_right (by omega)]
   exact Nat.lt_of_lt_of_le hw (Nat.le_max_right _ _)
 
 theorem d2Succ_pos (univs : Nat) (u : @SLevel (d2Params univs)) :

Lean4Lean/Experimental/ShapeLogRelAdequacy.lean

@@ -4472,7 +4472,7 @@ theorem LR.constDefEq
             ih x₀ y₀ hmem hchildLe hchildLeaf
               hchildTerm ⟨v, hchildType⟩ hchildSpineX hchildSpineY
               houtK hAK hy
-        rw [dif_pos hg]
+        rw [dite_eq_left hg]
         refine (LRS.DefEq.lam_forallE
           (M := xs.foldr (fun a f => f.app a) (.const c ls))
           (N := ys.foldr (fun a f => f.app a) (.const c ls))
@@ -4491,7 +4491,7 @@ theorem LR.constDefEq
             evalChild (Nat.max_eq_right (Nat.le_succ q))
               hleaf.aligned hterm hspineX hspineY
               hp hxy hv hmem hx hy⟩)
-      · rw [dif_neg hg]
+      · rw [dite_eq_right hg]
         exact (LR Γ₀).bot hout.isType
     | ctor => exact (TShape.ctor_not_le_lam' hlam').elim
     | indTy => exact (TShape.indTy_not_le_lam' hlam').elim

Lean4Lean/Experimental/Thierry2.lean

@@ -302,7 +302,7 @@ theorem Shape.lift_le_lift {s t : Shape n} (le : n ≤ m) : (s.lift : Shape m) 
         ShapeFun.ble ble s t := by
       simp only [ShapeFun.ble, ShapeFun.lift, List.all_map, List.any_map, Function.comp_def, ih]
     -- have sif {i} (h : i ≤ n) : (if h : i ≤ m then .sort i h else .bot : Shape (m+1)) =
-    --     .sort i (Nat.le_trans h le) := dif_pos _
+    --     .sort i (Nat.le_trans h le) := dite_eq_left _
     cases s <;> cases t <;> simp [ble, lift, *]
 
 theorem Shape.lift_mono {s t : Shape n} : s ≤ t → (s.lift : Shape m) ≤ t.lift := by

Lean4Lean/Inductive/Add.lean

@@ -1130,7 +1130,7 @@ theorem checkInductiveTypes_loop_of_candidate
         .ok bodyCandidate.rootWhnf at hvalid
       rw [show fuel = (fuel - 1) + 1 by omega]
       simp only [rootWhnf, checkInductiveTypes.loopInd.loop,
-        Nat.lt_irrefl, if_false, withLocalDecl_apply]
+        Nat.lt_irrefl, ite_false, withLocalDecl_apply]
       rw [← hmatch]
       simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply]
       rw [hvalid]
@@ -1152,7 +1152,7 @@ theorem checkInductiveTypes_loop_of_candidate
           (TypeChecker.whnf (body.instantiate1 context.freshExpr)) =
         .ok bodyCandidate.rootWhnf at hvalid
       rw [show fuel = (fuel - 1) + 1 by omega]
-      simp only [rootWhnf, checkInductiveTypes.loopInd.loop, hil, if_true,
+      simp only [rootWhnf, checkInductiveTypes.loopInd.loop, hil, ite_true,
         hempty, withLocalDecl_apply]
       rw [← hmatch]
       simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply]
@@ -1223,7 +1223,7 @@ theorem checkInductiveTypes_singleton_of_candidate
     ReaderT.bind, Bind.bind, Pure.pure, Except.pure, Except.bind]
   rw [checkInductiveTypes.loopInd.eq_1]
   have hsize : 0 < #[indType].size := by simp
-  rw [dif_pos hsize]
+  rw [dite_eq_left hsize]
   rw [show #[indType][0] = indType by rfl]
   simp only [readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read,
     ReaderT.bind, Bind.bind, Pure.pure, Except.pure, Except.bind,
@@ -1239,14 +1239,14 @@ theorem checkInductiveTypes_singleton_of_candidate
   simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply]
   rw [hensure]
   simp only [Except.bind]
-  rw [if_pos (show ((InductiveStats.initial
+  rw [ite_eq_left (show ((InductiveStats.initial
       (List.map Level.param context.lparams)).indConsts).isEmpty = true from
     rfl)]
   simp only [Expr.sortLevel!, InductiveStats.initial, Nat.zero_add]
   simp only [ReaderT.bind, Bind.bind, Except.pure, Except.bind]
   rw [checkInductiveTypes.loopInd.eq_1]
   have hdone : ¬1 < #[indType].size := by simp
-  rw [dif_neg hdone]
+  rw [dite_eq_right hdone]
   simp only [readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read,
     ReaderT.bind, Bind.bind, Pure.pure, Except.pure, Except.bind]
   simp [singletonCandidateInductiveStats, hterminalLparams,

Lean4Lean/Inductive/EliminationTrace.lean

@@ -104,25 +104,25 @@ theorem run
       rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply]
       have notField : ¬ argIdx ≥ stats.params.size :=
         Nat.not_le.mpr isParameter
-      simp only [notField, if_false, Bind.bind]
+      simp only [notField, ite_false, Bind.bind]
       exact ih
   | proofField context fuel argIdx toCheck name domain body binderInfo
       sortResult isField ensureStep isProp tail ih =>
       rw [show fuel + 1 = Nat.succ fuel by omega]
       rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply]
-      simp only [isField, if_true, ReaderT.bind, Bind.bind,
+      simp only [isField, ite_true, ReaderT.bind, Bind.bind,
         liftTypeChecker_apply]
       rw [ensureStep]
-      simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, if_false]
+      simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, ite_false]
       exact ih
   | dataField context fuel argIdx toCheck name domain body binderInfo
       sortResult isField ensureStep isProp tail ih =>
       rw [show fuel + 1 = Nat.succ fuel by omega]
       rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply]
-      simp only [isField, if_true, ReaderT.bind, Bind.bind,
+      simp only [isField, ite_true, ReaderT.bind, Bind.bind,
         liftTypeChecker_apply]
       rw [ensureStep]
-      simp only [Except.bind, isProp, Bool.not_false, if_true]
+      simp only [Except.bind, isProp, Bool.not_false, ite_true]
       exact ih
   | terminal context source fuel argIdx toCheck notForall =>
       cases source <;>

Lean4Lean/Inductive/ValidationTrace.lean

@@ -131,19 +131,19 @@ theorem run
       rw [whnf]
       simp only [Except.bind]
       rw [occurs]
-      simp only [Bool.not_true, Bool.false_eq_true, if_false,
+      simp only [Bool.not_true, Bool.false_eq_true, ite_false,
         ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
         Except.bind, Except.pure]
       rw [domainFree]
-      simp only [Bool.false_eq_true, if_false, withLocalDecl_apply]
+      simp only [Bool.false_eq_true, ite_false, withLocalDecl_apply]
       exact ih
   | target context source result fuel targetIdx whnf occurs terminal valid =>
       unfold checkPositivity.loop
       simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply]
       rw [whnf]
       simp only [Except.bind]
       rw [occurs]
-      simp only [Bool.not_true, Bool.false_eq_true, if_false,
+      simp only [Bool.not_true, Bool.false_eq_true, ite_false,
         ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
         Except.bind, Except.pure]
       cases result <;>
@@ -174,7 +174,7 @@ theorem exists_of_run
           | false => exact ⟨.absent context source result fuel hwhnf hocc⟩
           | true =>
             rw [hocc] at success
-            simp only [Bool.not_true, Bool.false_eq_true, if_false,
+            simp only [Bool.not_true, Bool.false_eq_true, ite_false,
               ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
               Except.bind, Except.pure] at success
             cases result
@@ -183,7 +183,7 @@ theorem exists_of_run
                 cases hdomain : hasIndOcc stats.indConsts domain with
                 | false =>
                   rw [hdomain] at success
-                  simp only [Bool.false_eq_true, if_false,
+                  simp only [Bool.false_eq_true, ite_false,
                     withLocalDecl_apply] at success
                   obtain ⟨tail⟩ := ih success
                   exact ⟨.forallE context source fuel name domain body
@@ -272,7 +272,7 @@ theorem buildExecution_ok_of_run
         next hoccurs => exact ⟨_, rfl⟩
         next hoccurs =>
           rw [hoccurs] at success
-          simp only [Bool.not_true, Bool.false_eq_true, if_false,
+          simp only [Bool.not_true, Bool.false_eq_true, ite_false,
             ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
             Except.bind, Except.pure] at success
           cases result <;> simp only [Expr.isForall] <;> simp only at success
@@ -347,7 +347,7 @@ theorem run
   cases trace with
   | skipped h => simp [h, ReaderT.pure, Pure.pure, Except.pure]
   | safe h trace =>
-      simp only [h, Bool.not_false, if_true]
+      simp only [h, Bool.not_false, ite_true]
       unfold checkPositivity
       simpa only [readThe, MonadReaderOf.read, ReaderT.read,
         ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure,
@@ -386,7 +386,7 @@ theorem exists_of_run
       stats isUnsafe ctor argIdx context source) := by
   cases hUnsafe : isUnsafe with
   | false =>
-      simp only [hUnsafe, Bool.not_false, if_true] at success
+      simp only [hUnsafe, Bool.not_false, ite_true] at success
       unfold checkPositivity at success
       simp only [readThe, MonadReaderOf.read, ReaderT.read,
         ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure,
@@ -420,7 +420,7 @@ theorem buildExecution_ok_of_run
   cases isUnsafe with
   | true => exact ⟨_, rfl⟩
   | false =>
-      simp only [Bool.not_false, if_true] at success
+      simp only [Bool.not_false, ite_true] at success
       unfold checkPositivity at success
       simp only [readThe, MonadReaderOf.read, ReaderT.read,
         ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure,
@@ -520,7 +520,7 @@ theorem run
       rw [parameterTypeRun]
       simp only [Except.bind, liftTypeChecker_apply]
       rw [defeq]
-      simp only [if_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
+      simp only [ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
         Except.bind, Except.pure]
       exact ih
   | ordinary context fuel argIdx name domain body binderInfo sortResult noParameter
@@ -546,12 +546,12 @@ theorem run
       cases universeTrace with
       | structural valid =>
           rw [valid]
-          simp only [if_true, ReaderT.pure, Pure.pure,
+          simp only [ite_true, ReaderT.pure, Pure.pure,
             ReaderT.bind, Bind.bind, Except.bind, Except.pure]
           exact restRun
       | fallback structuralFailed valid =>
           rw [structuralFailed, valid]
-          simp only [Bool.true_eq_false, Bool.not_true, if_false,
+          simp only [Bool.true_eq_false, Bool.not_true, ite_false,
             Bool.false_eq_true,
             ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
             Except.bind, Except.pure]
@@ -602,7 +602,7 @@ theorem exists_of_run
                         change Except.error _ = Except.ok () at success
                         contradiction
                     | true =>
-                        simp only [if_true, ReaderT.pure, Pure.pure,
+                        simp only [ite_true, ReaderT.pure, Pure.pure,
                           ReaderT.bind, Bind.bind, Except.bind,
                           Except.pure] at success
                         obtain ⟨tail⟩ := ih success
@@ -636,7 +636,7 @@ theorem exists_of_run
                       (.forallE name domain body binderInfo) argIdx (fuel + 1)) := by
                   cases isUnsafe with
                   | false =>
-                      simp only [Bool.not_false, if_true,
+                      simp only [Bool.not_false, ite_true,
                         ReaderT.bind, Bind.bind] at restSuccess
                       cases hpos : checkPositivity stats domain ctor argIdx context with
                       | error err => simp_all [Except.bind]
@@ -658,7 +658,7 @@ theorem exists_of_run
                             binderInfo sortResult hparam hensure universeTrace
                             (.safe rfl positivityTrace) tail⟩
                   | true =>
-                      simp only [Bool.not_true, if_false,
+                      simp only [Bool.not_true, ite_false,
                         ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
                         Except.bind, Except.pure,
                         withLocalDecl_apply] at restSuccess
@@ -670,13 +670,13 @@ theorem exists_of_run
                     sortResult.sortLevel! with
                 | true =>
                     rw [hstruct] at success
-                    simp only [if_true, ReaderT.pure, Pure.pure,
+                    simp only [ite_true, ReaderT.pure, Pure.pure,
                       ReaderT.bind, Bind.bind, Except.bind,
                       Except.pure] at success
                     exact finish (.structural hstruct) success
                 | false =>
                     rw [hstruct] at success
-                    simp only [Bool.false_eq_true, if_false] at success
+                    simp only [Bool.false_eq_true, ite_false] at success
                     cases hfallback :
                         (stats.resultLevel.isAlwaysZero ||
                           stats.resultLevel.geq sortResult.sortLevel!) with
@@ -686,7 +686,7 @@ theorem exists_of_run
                         contradiction
                     | true =>
                         rw [hfallback] at success
-                        simp only [Bool.true_eq_false, Bool.not_true, if_false,
+                        simp only [Bool.true_eq_false, Bool.not_true, ite_false,
                           ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
                           Except.bind, Except.pure] at success
                         exact finish (.fallback hstruct hfallback) success
@@ -817,7 +817,7 @@ theorem buildExecution_ok_of_run
               contradiction
             next heq2 =>
               rw [heq2] at success
-              simp only [Except.bind, if_true, ReaderT.pure, Pure.pure,
+              simp only [Except.bind, ite_true, ReaderT.pure, Pure.pure,
                 ReaderT.bind, Bind.bind, Except.pure] at success
               obtain ⟨tail, htail⟩ := ih success
               rw [htail]
@@ -852,7 +852,7 @@ theorem buildExecution_ok_of_run
               intro restSuccess
               cases isUnsafe with
               | false =>
-                  simp only [Bool.not_false, if_true,
+                  simp only [Bool.not_false, ite_true,
                     ReaderT.bind, Bind.bind] at restSuccess
                   cases hpos : checkPositivity stats domain ctor argIdx
                       context with
@@ -870,7 +870,7 @@ theorem buildExecution_ok_of_run
                       exact ⟨ConstructorPositivityModeTrace.buildExecution_ok_of_run
                         hpmSuccess, ih restSuccess⟩
               | true =>
-                  simp only [Bool.not_true, if_false,
+                  simp only [Bool.not_true, ite_false,
                     ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
                     Except.bind, Except.pure,
                     withLocalDecl_apply] at restSuccess
@@ -884,22 +884,22 @@ theorem buildExecution_ok_of_run
             split
             next hstruct =>
               rw [hstruct] at success
-              simp only [if_true, ReaderT.pure, Pure.pure,
+              simp only [ite_true, ReaderT.pure, Pure.pure,
                 ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success
               obtain ⟨⟨positivity, hpm⟩, tail, htail⟩ := finish success
               rw [hpm, htail]
               exact ⟨_, rfl⟩
             next hstruct =>
               rw [hstruct] at success
-              simp only [Bool.false_eq_true, if_false] at success
+              simp only [Bool.false_eq_true, ite_false] at success
               split
               next hfallback =>
                 rw [hfallback] at success
                 change Except.error _ = Except.ok () at success
                 contradiction
               next hfallback =>
                 rw [hfallback] at success
-                simp only [Bool.true_eq_false, Bool.not_true, if_false,
+                simp only [Bool.true_eq_false, Bool.not_true, ite_false,
                   ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind,
                   Except.bind, Except.pure] at success
                 obtain ⟨⟨positivity, hpm⟩, tail, htail⟩ := finish success
@@ -1157,7 +1157,7 @@ theorem fold_run
       unfold checkConstructorFold
       simp only
       rw [fresh]
-      simp only [Bool.false_eq_true, if_false,
+      simp only [Bool.false_eq_true, ite_false,
         ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure,
         Except.bind, Except.pure]
       rw [closed]
@@ -1193,7 +1193,7 @@ theorem exists_of_fold_run
           contradiction
       | false =>
           rw [hfresh] at success
-          simp only [Bool.false_eq_true, if_false,
+          simp only [Bool.false_eq_true, ite_false,
             ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure,
             Except.bind, Except.pure] at success
           cases hclosed : context.env.checkNoMVarNoFVar
@@ -1261,7 +1261,7 @@ theorem buildExecution_ok_of_fold_run
         contradiction
       next hfresh =>
         rw [hfresh] at success
-        simp only [Bool.false_eq_true, if_false,
+        simp only [Bool.false_eq_true, ite_false,
           ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure,
           Except.bind, Except.pure] at success
         split

Lean4Lean/Std/Basic.lean

@@ -151,7 +151,6 @@ theorem List.idxOf_eq_length_iff [BEq α] [LawfulBEq α]
   | nil => exact iff_of_true rfl not_mem_nil
   | cons b l ih =>
     simp only [length, mem_cons, idxOf_cons]
-    rw [cond_eq_ite]
     split <;> rename_i h <;> simp at h
     · exact iff_of_false (by rintro ⟨⟩) fun H => H <| Or.inl h.symm
     · simp only [Ne.symm h, false_or]