chore: Update Lean and dependencies on 2026/02/17 (#758)

Co-authored-by: palalansouki <palalansouki@gmail.com>

Author: SnO2WMaN

Foundation.lean

@@ -516,6 +516,7 @@ public import Foundation.Vorspiel.Nat.Matrix
 public import Foundation.Vorspiel.NotationClass
 public import Foundation.Vorspiel.Option
 public import Foundation.Vorspiel.Order
+public import Foundation.Vorspiel.Part
 public import Foundation.Vorspiel.Preorder
 public import Foundation.Vorspiel.Quotient
 public import Foundation.Vorspiel.Rel.Basic

Foundation/FirstOrder/Arithmetic/Definability/Definable.lean

@@ -403,6 +403,7 @@ lemma not (h : Γ.alt-[m].Definable P) :
 lemma impDelta (hp : 𝚫-[m].Definable P) (hq : 𝚫-[m].Definable Q) :
     𝚫-[m].Definable fun x ↦ P x → Q x := (hp.notDelta.or hq).of_iff (by intro x; simp [imp_iff_not_or])
 
+set_option backward.isDefEq.respectTransparency false in
 lemma imp (h₁ : Γ.alt-[m].Definable P) (h₂ : Γ-[m].Definable Q) :
     Γ-[m].Definable (fun v ↦ P v → Q v) := by
   match Γ with

Foundation/FirstOrder/Arithmetic/Exponential/Exp.lean

@@ -775,6 +775,7 @@ lemma exp_even (a : V) : Exp.exp (2 * a) = (Exp.exp a)^2 :=
 @[simp] lemma exp_monotone_le {a b : V} : Exp.exp a ≤ Exp.exp b ↔ a ≤ b :=
   Iff.symm <| Exponential.monotone_le_iff (exponential_exp a) (exponential_exp b)
 
+set_option backward.isDefEq.respectTransparency false in
 lemma nat_cast_exp (n : ℕ) : (Exp.exp n : ℕ) = Exp.exp (n : V) := by
   induction' n with n ih
   · simp

Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean

@@ -16,9 +16,13 @@ section IOpen
 
 variable [V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻]
 
-instance : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻)
+instance : V ⊧ₘ* 𝗣𝗔⁻ :=
+  have : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 := inferInstance
+  models_of_subtheory this
 
-instance : V ⊧ₘ* InductionScheme ℒₒᵣ Semiformula.Open := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻)
+instance : V ⊧ₘ* InductionScheme ℒₒᵣ Semiformula.Open :=
+  have : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 := inferInstance
+  models_of_subtheory this
 
 @[elab_as_elim]
 lemma succ_induction {P : V → Prop}
@@ -768,7 +772,8 @@ end IOpen
 lemma polynomial_induction [V ⊧ₘ* 𝗣𝗔⁻] (Γ m) [V ⊧ₘ* 𝗜𝗡𝗗 Γ m]
     {P : V → Prop} (hP : Γ-[m]-Predicate P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x := by
-  haveI : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  have : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 := models_of_subtheory this
   intro x; induction x using InductionOnHierarchy.order_induction
   · exact Γ
   · exact m

Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean

@@ -490,7 +490,7 @@ scoped instance : CovariantClass M M (· + ·) (· ≤ ·) := ⟨by intro; simp
 scoped instance : CovariantClass M M (Function.swap (· * ·)) (· ≤ ·) := ⟨by intro; exact mul_le_mul_right⟩
 
 @[simp] lemma one_lt_mul_self_iff {a : M} : 1 < a * a ↔ 1 < a :=
-  ⟨(fun h ↦ by push_neg at h ⊢; exact mul_le_one' h h).mtr, fun h ↦ one_lt_mul'' h h⟩
+  ⟨(fun h ↦ by push Not at h ⊢; exact mul_le_one' h h).mtr, fun h ↦ one_lt_mul'' h h⟩
 
 @[simp] lemma opos_lt_sq_pos_iff {a : M} : 0 < a^2 ↔ 0 < a := by simp [sq, pos_iff_ne_zero]
 

Foundation/FirstOrder/Arithmetic/Q/Basic.lean

@@ -152,7 +152,7 @@ lemma zero_mul_one : (0 : M) * 1 = 0 := calc
 @[simp]
 lemma not_le_zero {a : M} : ¬a < 0 := by
   apply Arithmetic.lt_def.not.mpr;
-  push_neg;
+  push Not;
   intro b;
   calc
     a + (b + 1) = (a + b) + 1 := Arithmetic.add_succ _ _

Foundation/FirstOrder/Arithmetic/R0/Basic.lean

@@ -136,7 +136,8 @@ lemma bold_sigma_one_completeness' {n} {σ : Semisentence ℒₒᵣ n} (hσ : Hi
   simpa [Empty.eq_elim] using bold_sigma_one_completeness (M := M) (φ := σ) hσ (f := Empty.elim) (e := e) h
 
 instance consistent : Entailment.Consistent 𝗥₀ :=
-  Sound.consistent_of_satisfiable ⟨_, inferInstanceAs (ℕ ⊧ₘ* 𝗥₀)⟩
+  let : ℕ ⊧ₘ* 𝗥₀ := inferInstance
+  Sound.consistent_of_satisfiable ⟨_, this⟩
 
 end model
 

Foundation/FirstOrder/Arithmetic/Schemata.lean

@@ -66,9 +66,13 @@ lemma ISigma_subset_mono {s₁ s₂} (h : s₁ ≤ s₂) : 𝗜𝚺 s₁ ⊆ 
 lemma ISigma_weakerThan_of_le {s₁ s₂} (h : s₁ ≤ s₂) : 𝗜𝚺 s₁ ⪯ 𝗜𝚺 s₂ :=
   Entailment.WeakerThan.ofSubset (ISigma_subset_mono h)
 
-instance : 𝗘𝗤 ⪯ 𝗜𝗡𝗗 Γ n := Entailment.WeakerThan.trans (inferInstanceAs (𝗘𝗤 ⪯ 𝗣𝗔⁻)) inferInstance
+instance : 𝗘𝗤 ⪯ 𝗜𝗡𝗗 Γ n :=
+  have : 𝗘𝗤 ⪯ 𝗣𝗔⁻ := inferInstance
+  Entailment.WeakerThan.trans this inferInstance
 
-instance : 𝗘𝗤 ⪯ 𝗜𝗢𝗽𝗲𝗻 := Entailment.WeakerThan.trans (inferInstanceAs (𝗘𝗤 ⪯ 𝗣𝗔⁻)) inferInstance
+instance : 𝗘𝗤 ⪯ 𝗜𝗢𝗽𝗲𝗻 :=
+  have : 𝗘𝗤 ⪯ 𝗣𝗔⁻ := inferInstance
+  Entailment.WeakerThan.trans this inferInstance
 
 instance : 𝗜𝗢𝗽𝗲𝗻 ⪯ 𝗜𝗡𝗗 Γ n :=
   Entailment.WeakerThan.ofSubset <| Set.union_subset_union_right _  <| InductionScheme_subset Arithmetic.Hierarchy.of_open
@@ -126,11 +130,14 @@ section
 
 variable (Γ : Polarity) (m : ℕ) [V ⊧ₘ* 𝗜𝗡𝗗 Γ m]
 
-instance : V ⊧ₘ* InductionScheme ℒₒᵣ (Hierarchy Γ m) := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+instance : V ⊧ₘ* InductionScheme ℒₒᵣ (Hierarchy Γ m) :=
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  models_of_subtheory this
 
 lemma succ_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x :=
-  haveI : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  have : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory this
   InductionScheme.succ_induction (P := P) (C := Hierarchy Γ m) (by
     rcases hP with ⟨φ, hp⟩
     haveI : Inhabited V := Classical.inhabited_of_nonempty'
@@ -140,7 +147,8 @@ lemma succ_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P)
 
 lemma order_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P)
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x := by
-  haveI : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  have : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory this
   suffices ∀ x, ∀ y < x, P y by
     intro x; exact this (x + 1) x (by simp only [lt_add_iff_pos_right, lt_one_iff_eq_zero])
   intro x; induction x using succ_induction
@@ -158,7 +166,8 @@ lemma order_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P)
 
 private lemma neg_succ_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P)
     (nzero : ¬P 0) (nsucc : ∀ x, ¬P x → ¬P (x + 1)) : ∀ x, ¬P x := by
-  haveI : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  have : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory this
   by_contra A
   have : ∃ x, P x := by simpa using A
   rcases this with ⟨a, ha⟩
@@ -202,12 +211,14 @@ instance models_InductionScheme_alt : V ⊧ₘ* InductionScheme ℒₒᵣ (Arith
       (by intro x; simp [←Matrix.fun_eq_vec_one, Semiformula.eval_rewriteMap]))
 
 instance models_alt : V ⊧ₘ* 𝗜𝗡𝗗 Γ.alt m := by
-  haveI : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  have : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory this
   simp only [InductionOnHierarchy, ModelsTheory.add_iff]; constructor <;> infer_instance
 
 lemma least_number {P : V → Prop} (hP : Γ-[m].DefinablePred P)
     {x} (h : P x) : ∃ y, P y ∧ ∀ z < y, ¬P z := by
-  haveI : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗡𝗗 Γ m)
+  have : V ⊧ₘ* 𝗜𝗡𝗗 Γ m := inferInstance
+  have : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory this
   by_contra A
   have A : ∀ z, P z → ∃ w < z, P w := by simpa using A
   have : ∀ z, ∀ w < z, ¬P w := by
@@ -338,13 +349,17 @@ lemma ISigma0.least_number [V ⊧ₘ* 𝗜𝚺₀] {P : V → Prop} (hP : 𝚺
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x :=
   InductionOnHierarchy.order_induction_sigma Γ 1 hP ind
 
-instance [V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻] : V ⊧ₘ* 𝗣𝗔⁻ := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻)
+instance [V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻] : V ⊧ₘ* 𝗣𝗔⁻ :=
+  have : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 := inferInstance
+  models_of_subtheory this
 
-instance [V ⊧ₘ* 𝗜𝚺₀] : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 := models_of_subtheory <| inferInstanceAs (V ⊧ₘ* 𝗜𝚺₀)
+instance [V ⊧ₘ* 𝗜𝚺₀] : V ⊧ₘ* 𝗜𝗢𝗽𝗲𝗻 :=
+  have : V ⊧ₘ* 𝗜𝚺₀ := inferInstance
+  models_of_subtheory this
 
 instance [V ⊧ₘ* 𝗜𝚺₁] : V ⊧ₘ* 𝗜𝚺₀ := inferInstance
 
-def mod_ISigma_of_le {n₁ n₂} (h : n₁ ≤ n₂) [V ⊧ₘ* 𝗜𝚺 n₂] : V ⊧ₘ* 𝗜𝚺 n₁ :=
+abbrev mod_ISigma_of_le {n₁ n₂} (h : n₁ ≤ n₂) [V ⊧ₘ* 𝗜𝚺 n₂] : V ⊧ₘ* 𝗜𝚺 n₁ :=
   ModelsTheory.of_ss inferInstance (ISigma_subset_mono h)
 
 end models
@@ -381,15 +396,19 @@ instance : Entailment.Consistent 𝗣𝗔 := 𝗣𝗔.consistent_of_sound (Eq 
 instance : 𝗣𝗔 ⪯ 𝗧𝗔 := inferInstance
 
 instance (T : ArithmeticTheory) [𝗣𝗔⁻ ⪯ T] : 𝗥₀ ⪯ T :=
-  Entailment.WeakerThan.trans (inferInstanceAs (𝗥₀ ⪯ 𝗣𝗔⁻)) inferInstance
+  have : 𝗥₀ ⪯ 𝗣𝗔⁻ := inferInstance
+  Entailment.WeakerThan.trans this inferInstance
 
 instance (T : ArithmeticTheory) [𝗜𝚺₀ ⪯ T] : 𝗣𝗔⁻ ⪯ T :=
-  Entailment.WeakerThan.trans (inferInstanceAs (𝗣𝗔⁻ ⪯ 𝗜𝚺₀)) inferInstance
+  have : 𝗣𝗔⁻ ⪯ 𝗜𝚺₀ := inferInstance
+  Entailment.WeakerThan.trans this inferInstance
 
 instance (T : ArithmeticTheory) [𝗜𝚺₁ ⪯ T] : 𝗣𝗔⁻ ⪯ T :=
-  Entailment.WeakerThan.trans (inferInstanceAs (𝗣𝗔⁻ ⪯ 𝗜𝚺₁)) inferInstance
+  have : 𝗣𝗔⁻ ⪯ 𝗜𝚺₁ := inferInstance
+  Entailment.WeakerThan.trans this inferInstance
 
 instance (T : ArithmeticTheory) [𝗣𝗔 ⪯ T] : 𝗣𝗔⁻ ⪯ T :=
-  Entailment.WeakerThan.trans (inferInstanceAs (𝗣𝗔⁻ ⪯ 𝗣𝗔)) inferInstance
+  have : 𝗣𝗔⁻ ⪯ 𝗣𝗔 := inferInstance
+  Entailment.WeakerThan.trans this inferInstance
 
 end LO.FirstOrder.Arithmetic

Foundation/FirstOrder/Basic/Calculus.lean

@@ -640,7 +640,8 @@ def unprovable_univCl_iff {φ : SyntacticFormula L} :
     (𝓢 : Theory L) ⊬ φ.univCl ↔ 𝓢 ⊬ φ := provable_univCl_iff.not
 
 instance (𝓢 𝓣 : Schema L) [𝓢 ⪯ 𝓣] : 𝓢.toTheory ⪯ 𝓣.toTheory :=
-  ⟨fun _ b ↦ coe_provable_iff_provable_coe.mpr <| (inferInstanceAs (𝓢 ⪯ 𝓣)).pbl (coe_provable_iff_provable_coe.mp b)⟩
+  let le : 𝓢 ⪯ 𝓣 := inferInstance
+  ⟨fun _ b ↦ coe_provable_iff_provable_coe.mpr <| le.pbl (coe_provable_iff_provable_coe.mp b)⟩
 
 @[simp] lemma coe_consistent_iff :
     Consistent (𝓢 : Theory L) ↔ Consistent 𝓢 := calc

Foundation/FirstOrder/Basic/Eq.lean

@@ -225,6 +225,7 @@ lemma elementaryEquiv : QuotEq L M ≡ₑ[L] M := ⟨models_iff⟩
 
 variable {L M}
 
+set_option backward.isDefEq.respectTransparency false in
 lemma rel_eq (a b : QuotEq L M) : (@Semiformula.Operator.Eq.eq L _).val (M := QuotEq L M) ![a, b] ↔ a = b := by
   induction' a using Quotient.ind with a
   induction' b using Quotient.ind with b