diff --git a/Foundation/IntProp/Heyting/Semantics.lean b/Foundation/IntProp/Heyting/Semantics.lean
index f5d1746f..6d5d8b4e 100644
--- a/Foundation/IntProp/Heyting/Semantics.lean
+++ b/Foundation/IntProp/Heyting/Semantics.lean
@@ -87,7 +87,10 @@ instance : Semantics.And (HeytingSemantics α) := ⟨fun {ℍ φ ψ} ↦ by simp
 @[simp] lemma val_iff {φ ψ : Formula α} : ℍ ⊧ φ ⭤ ψ ↔ (ℍ ⊧ₕ φ) = (ℍ ⊧ₕ ψ) := by
   simp [LogicalConnective.iff, antisymm_iff]
 
-lemma val_not (φ : Formula α) : ℍ ⊧ ∼φ ↔ (ℍ ⊧ₕ φ) = ⊥ := by simp [val_def]; rw [←HeytingAlgebra.himp_bot, himp_eq_top_iff, le_bot_iff]; rfl
+lemma val_not (φ : Formula α) : ℍ ⊧ ∼φ ↔ (ℍ ⊧ₕ φ) = ⊥ := by
+  simp only [val_def, Formula.hVal_neg];
+  rw [←HeytingAlgebra.himp_bot, himp_eq_top_iff, le_bot_iff];
+  rfl
 
 @[simp] lemma val_or (φ ψ : Formula α) : ℍ ⊧ φ ⋎ ψ ↔ (ℍ ⊧ₕ φ) ⊔ (ℍ ⊧ₕ ψ) = ⊤ := by
   simp [val_def]; rfl
@@ -96,8 +99,6 @@ def mod (H : Hilbert α) : Set (HeytingSemantics α) := Semantics.models (Heytin
 
 variable {H : Hilbert α}
 
-instance [H.IncludeEFQ] : System.Intuitionistic H where
-
 lemma mod_models_iff {φ : Formula α} :
     mod.{_,w} H ⊧ φ ↔ ∀ ℍ : HeytingSemantics.{_,w} α, ℍ ⊧* H.axioms → ℍ ⊧ φ := by
   simp [mod, Semantics.models, Semantics.set_models_iff]
@@ -136,17 +137,16 @@ def lindenbaum : HeytingSemantics α where
   valAtom a := ⟦.atom a⟧
 
 lemma lindenbaum_val_eq : (lindenbaum H ⊧ₕ φ) = ⟦φ⟧ := by
-  induction φ using Formula.rec' <;> try simp [top_def, bot_def]
-  case hatom => rfl
-  case hverum => rfl
-  case hfalsum => rfl
-  case hand ihp ihq => simp [ihp, ihq]; rw [inf_def]
-  case hor ihp ihq => simp [ihp, ihq]; rw [sup_def]
-  case himp ihp ihq => simp [ihp, ihq]; rw [himp_def]
-  case hneg ih => simp [ih]; rw [compl_def]
+  induction φ using Formula.rec' with
+  | hand _ _ ihp ihq => simp only [hVal_and, ihp, ihq]; rw [inf_def];
+  | hor _ _ ihp ihq => simp only [hVal_or, ihp, ihq]; rw [sup_def];
+  | himp _ _ ihp ihq => simp only [hVal_imply, ihp, ihq]; rw [himp_def];
+  | hneg _ ih => simp only [hVal_not, ih]; rw [compl_def];
+  | _ => rfl
 
 variable {H}
 
+omit [System.Consistent H] in
 lemma lindenbaum_complete_iff [System.Consistent H] {φ : Formula α} : lindenbaum H ⊧ φ ↔ H ⊢! φ := by
   simp [val_def', lindenbaum_val_eq, provable_iff_eq_top]
 
diff --git a/Foundation/Logic/LindenbaumAlgebra.lean b/Foundation/Logic/LindenbaumAlgebra.lean
index 77a3992f..c45a32d8 100644
--- a/Foundation/Logic/LindenbaumAlgebra.lean
+++ b/Foundation/Logic/LindenbaumAlgebra.lean
@@ -136,7 +136,7 @@ lemma provable_iff_eq_top {φ : F} : 𝓢 ⊢! φ ↔ (⟦φ⟧ : LindenbaumAlge
   simp [top_def, provable_iff_provablyEquivalent_verum]; rfl
 
 lemma inconsistent_iff_trivial : Inconsistent 𝓢 ↔ (∀ φ : LindenbaumAlgebra 𝓢, φ = ⊤) := by
-  simp [Inconsistent, provable_iff_eq_top]
+  simp only [Inconsistent, provable_iff_eq_top]
   constructor
   · intro h φ;
     induction φ using Quotient.ind
@@ -145,7 +145,7 @@ lemma inconsistent_iff_trivial : Inconsistent 𝓢 ↔ (∀ φ : LindenbaumAlgeb
 
 lemma consistent_iff_nontrivial : Consistent 𝓢 ↔ Nontrivial (LindenbaumAlgebra 𝓢) := by
   apply not_iff_not.mp
-  simp [not_consistent_iff_inconsistent, nontrivial_iff, inconsistent_iff_trivial]
+  simp only [not_consistent_iff_inconsistent, inconsistent_iff_trivial, nontrivial_iff, ne_eq, not_exists, not_not]
   constructor
   · intro h φ ψ; simp [h]
   · intro h φ; exact h φ ⊤
@@ -167,7 +167,7 @@ instance LindenbaumAlgebra.heyting [DecidableEq F] : HeytingAlgebra (LindenbaumA
     exact efq!
   himp_bot φ := by
     induction' φ using Quotient.ind with φ
-    simp [bot_def, himp_def, compl_def]
+    simp only [bot_def, himp_def, compl_def, Quotient.eq]
     exact iff_comm! ⨀ neg_equiv!
 
 end intuitionistic
@@ -184,7 +184,7 @@ instance LindenbaumAlgebra.boolean [DecidableEq F] : BooleanAlgebra (LindenbaumA
     simp only [compl_def, inf_def, bot_def, le_def, intro_bot_of_and!]
   top_le_sup_compl φ := by
     induction' φ using Quotient.ind with φ
-    simp [compl_def, sup_def, top_def, le_def]
+    simp only [top_def, compl_def, sup_def, le_def]
     apply imply₁'! lem!
   le_top φ := by
     induction' φ using Quotient.ind with φ
@@ -198,7 +198,7 @@ instance LindenbaumAlgebra.boolean [DecidableEq F] : BooleanAlgebra (LindenbaumA
     induction' φ using Quotient.ind with φ
     induction' ψ using Quotient.ind with ψ
     rw [sup_comm]
-    simp [himp_def, compl_def, sup_def]
+    simp only [himp_def, compl_def, sup_def, Quotient.eq]
     exact imply_iff_not_or!
 
 end classical