fix

Author: iehality

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/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

Foundation/FirstOrder/Basic/Semantics/Elementary.lean

@@ -220,8 +220,8 @@ lemma modelsTheory [h : M₁ ≡ₑ[L] M₂] {T : Theory L} :
 
 variable (M₁ M₂)
 
-lemma modelsTheory' [M₁ ≡ₑ[L] M₂] (T : Theory L) [M₂ ⊧ₘ* T] :
-    M₁ ⊧ₘ* T := modelsTheory.mpr (inferInstanceAs (M₂ ⊧ₘ* T))
+lemma modelsTheory' [M₁ ≡ₑ[L] M₂] (T : Theory L) [h : M₂ ⊧ₘ* T] :
+    M₁ ⊧ₘ* T := modelsTheory.mpr h
 
 variable {M₁ M₂}
 

Foundation/FirstOrder/Basic/Soundness.lean

@@ -82,9 +82,9 @@ theorem smallSound! : T ⊢ σ → T ⊨ σ := sound!
 
 instance (T : Theory L) : Sound T (Semantics.models (Struc.{v, u} L) T) := ⟨sound!⟩
 
-lemma models_of_subtheory {T U : Theory L} [U ⪯ T] {M : Type*} [Structure L M] [Nonempty M] (hM : M ⊧ₘ* T) : M ⊧ₘ* U :=
+lemma models_of_subtheory {T U : Theory L} [le : U ⪯ T] {M : Type*} [Structure L M] [Nonempty M] (hM : M ⊧ₘ* T) : M ⊧ₘ* U :=
   ⟨ fun {φ} hp ↦ by
-    have : T ⊢ φ := (inferInstanceAs (U ⪯ T)).pbl (Entailment.by_axm _ hp)
+    have : T ⊢ φ := le.pbl (Entailment.by_axm _ hp)
     exact sound! this hM ⟩
 
 lemma consistent_of_satisfiable (h : Semantics.Satisfiable (Struc.{v, u} L) T) : Entailment.Consistent T :=

Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/PeanoMinus.lean

@@ -36,7 +36,9 @@ variable (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T]
 
 open Entailment Entailment.FiniteContext Semiformula
 
-instance : 𝗘𝗤 ⪯ T := WeakerThan.trans inferInstance (inferInstanceAs (𝗣𝗔⁻ ⪯ T))
+instance : 𝗘𝗤 ⪯ T :=
+  have : 𝗣𝗔⁻ ⪯ T := inferInstance
+  WeakerThan.trans inferInstance this
 
 lemma term_add_assoc (t₁ t₂ t₃ : Term V ℒₒᵣ) :
     T.internalize V ⊢ t₁ + (t₂ + t₃) ≐ (t₁ + t₂) + t₃ := by