From 3949a40ed334d895980411c190c83c32b7695ffd Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Fri, 16 Oct 2026 13:53:29 +0000
Subject: [PATCH 1/3] perf(Incompleteness): factor sequence and frame proofs

---
 .../Arithmetization/Basic/IOpen.lean          |  1 -
 .../Arithmetization/Basic/Ind.lean            |  1 -
 .../Arithmetization/ISigmaOne/HFS/Seq.lean    | 16 +++++++++++++--
 .../ISigmaOne/Metamath/Proof/Derivation.lean  |  1 -
 .../ISigmaOne/Metamath/Term/Functions.lean    |  1 -
 .../Foundation/FirstOrder/Arith/Theory.lean   | 20 +++----------------
 .../Foundation/Modal/Entailment/K5.lean       |  4 ----
 .../Modal/Kripke/Hilbert/GL/Tree.lean         |  1 -
 .../Kripke/Hilbert/Grz/Completeness.lean      | 11 ++++++----
 .../Foundation/Modal/Logic/WellKnown.lean     |  2 --
 .../Foundation/Vorspiel/Order.lean            |  1 -
 11 files changed, 24 insertions(+), 35 deletions(-)

diff --git a/LeanPool/Incompleteness/Arithmetization/Basic/IOpen.lean b/LeanPool/Incompleteness/Arithmetization/Basic/IOpen.lean
index 5a12871dd6..95fae1ba9f 100644
--- a/LeanPool/Incompleteness/Arithmetization/Basic/IOpen.lean
+++ b/LeanPool/Incompleteness/Arithmetization/Basic/IOpen.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.Incompleteness.Arithmetization.Basic.Ind
 public import LeanPool.Incompleteness.Arithmetization.Basic.PeanoMinus
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 
 /-! # IOpen -/
diff --git a/LeanPool/Incompleteness/Arithmetization/Basic/Ind.lean b/LeanPool/Incompleteness/Arithmetization/Basic/Ind.lean
index 6ea5e1f4d3..740bf2bc44 100644
--- a/LeanPool/Incompleteness/Arithmetization/Basic/Ind.lean
+++ b/LeanPool/Incompleteness/Arithmetization/Basic/Ind.lean
@@ -9,7 +9,6 @@ public import LeanPool.Incompleteness.Arithmetization.Definability.Boldface
 import LeanPool.Incompleteness.Arithmetization.Basic.PeanoMinus
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
 import LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.Corollaries
-import Mathlib.Algebra.Order.Sub.Basic
 
 /-! # Ind -/
 
diff --git a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Seq.lean b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Seq.lean
index d3332a3d10..454cc19e78 100644
--- a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Seq.lean
+++ b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Seq.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Basic
 import LeanPool.Incompleteness.Arithmetization.Definability.Absoluteness
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 
 /-!
 
@@ -432,8 +431,21 @@ section «lp_section_4»
 def _root_.LO.FirstOrder.Arith.mkSeq₁Def : Sg0.Semisentence 2 := .mkSigma
   “s x. !seqConsDef s 0 x” (by simp)
 
+-- Keeping the function abstract prevents conversion from unfolding encoded sequence operations.
+omit [V ⊧ₘ* 𝐈Sg1] in
+private lemma defined_zero_left (f : V → V → V) (φ : Sg0.Semisentence 3)
+    (hφ : Sg0-Function₂ f via φ) :
+    Sg0-Function₁ (fun x ↦ f ∅ x) via
+      (.mkSigma “s x. !φ s 0 x” (by simp)) := by
+  intro v
+  simp only [Fin.isValue, Fin.succ_zero_eq_one, Nat.reduceAdd, Nat.succ_eq_add_one,
+    HierarchySymbol.Semiformula.val_mkSigma, Semiformula.eval_substs, hφ.df.iff,
+    Matrix.vecCons_zero, Semiterm.val_bvar, Matrix.cons_val_one,
+    Semiterm.val_const, Structure.numeral_eq_numeral, ORingStruc.zero_eq_zero]
+  rfl
+
 lemma mkSeq₁_defined : Sg0-Function₁ (fun x : V ↦ !⟦x⟧) via mkSeq₁Def := by
-  intro v; simp [mkSeq₁Def]; rfl
+  simpa only [mkSeq₁Def] using defined_zero_left seqCons seqConsDef seqCons_defined
 
 @[simp] lemma eval_mkSeq₁Def (v) :
     Semiformula.Evalbm V v mkSeq₁Def.val ↔ v 0 = !⟦v 1⟧ := mkSeq₁_defined.df.iff v
diff --git a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Proof/Derivation.lean b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Proof/Derivation.lean
index 30565adb96..01663ae7fd 100644
--- a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Proof/Derivation.lean
+++ b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Proof/Derivation.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Proof.Thy
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Iteration
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 
 /-! # Derivation -/
 
diff --git a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean
index 08de8262a7..67d8b298e9 100644
--- a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean
+++ b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean
@@ -7,7 +7,6 @@ module
 
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Term.Basic
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 
 /-! # Functions -/
diff --git a/LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Theory.lean b/LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Theory.lean
index f5165c257d..3d28062cdd 100644
--- a/LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Theory.lean
+++ b/LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Theory.lean
@@ -232,23 +232,9 @@ example (a b : ℕ) : Set.Finite {a, b} := by simp only [Set.finite_singleton, S
     ext φ; constructor
     · rintro ⟨⟩
       case equal => left; assumption
-      case addZero => tauto
-      case addAssoc => tauto
-      case addComm => tauto
-      case addEqOfLt => tauto
-      case zeroLe => tauto
-      case zeroLtOne => tauto
-      case oneLeOfZeroLt => tauto
-      case addLtAdd => tauto
-      case mulZero => tauto
-      case mulOne => tauto
-      case mulAssoc => tauto
-      case mulComm => tauto
-      case mulLtMul => tauto
-      case distr => tauto
-      case ltIrrefl => tauto
-      case ltTrans => tauto
-      case ltTri => tauto
+      all_goals
+        right
+        simp only [Set.mem_insert_iff, Set.mem_singleton_iff, or_true, true_or]
     · rintro (h | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
       | rfl | rfl | rfl)
       · exact PeanoMinus.equal _ h
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Entailment/K5.lean b/LeanPool/Incompleteness/Foundation/Modal/Entailment/K5.lean
index c9c22e195a..336a8cfdfe 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Entailment/K5.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Entailment/K5.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.Incompleteness.Foundation.Modal.Entailment.K
 
-import Mathlib.Data.Finset.Attr
-import Mathlib.Tactic.Bound.Init
-import Mathlib.Tactic.Finiteness.Attr
-import Mathlib.Tactic.SetLike
 
 /-! # K5 -/
 
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Tree.lean b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Tree.lean
index 626523d7fe..7d46def922 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Tree.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Tree.lean
@@ -9,7 +9,6 @@ public import LeanPool.Incompleteness.Foundation.Modal.Kripke.Tree
 public import LeanPool.Incompleteness.Foundation.Modal.Hilbert.WellKnown
 public import LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomL
 import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Completeness
-import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Soundness
 
 /-! # Tree -/
 
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean
index 8e883f6d51..557f948fc6 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean
@@ -93,10 +93,13 @@ lemma reflexive : Std.Refl (miniCanonicalFrame φ).Rel :=
 lemma transitive : IsTrans (miniCanonicalFrame φ).World (miniCanonicalFrame φ).Rel := by
   constructor
   rintro X Y Z ⟨RXY₁, RXY₂⟩ ⟨RYZ₁, RYZ₂⟩;
-  constructor;
-  · simp_all
-  · intro h;
-    simp_all
+  constructor
+  · intro χ hχ hX
+    exact RYZ₁ χ hχ (RXY₁ χ hχ hX)
+  · intro h
+    have hXY : X = Y := RXY₂ fun χ hχ hY ↦ h χ hχ (RYZ₁ χ hχ hY)
+    have hYZ : Y = Z := RYZ₂ fun χ hχ hZ ↦ RXY₁ χ hχ (h χ hχ hZ)
+    exact hXY.trans hYZ
 
 lemma antisymm : Std.Antisymm (miniCanonicalFrame φ).Rel := by
   constructor
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Logic/WellKnown.lean b/LeanPool/Incompleteness/Foundation/Modal/Logic/WellKnown.lean
index c484f574a1..3512a630fd 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Logic/WellKnown.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Logic/WellKnown.lean
@@ -29,10 +29,8 @@ public import LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomGrz
 public import LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomL
 public import LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomVer
 import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Completeness
-import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Soundness
 import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Unnecessitation
 import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Grz.Completeness
-import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Grz.Soundness
 import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Ver
 
 /-! # WellKnown -/
diff --git a/LeanPool/Incompleteness/Foundation/Vorspiel/Order.lean b/LeanPool/Incompleteness/Foundation/Vorspiel/Order.lean
index 119548eef5..06f27a84f3 100644
--- a/LeanPool/Incompleteness/Foundation/Vorspiel/Order.lean
+++ b/LeanPool/Incompleteness/Foundation/Vorspiel/Order.lean
@@ -8,7 +8,6 @@ module
 public import Aesop.BuiltinRules
 public import Mathlib.Order.Heyting.Basic
 public import Mathlib.Tactic.ToAdditive
-import Mathlib.Algebra.GroupWithZero.Nat
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Data.Finset.Attr
 import Mathlib.Tactic.Bound.Init

From 89b42910e584d7c7e67be0aa385ac25e616ec972 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Fri, 16 Oct 2026 14:38:55 +0000
Subject: [PATCH 2/3] perf(Incompleteness): reuse formula and frame proof
 lemmas

---
 LeanPool/Incompleteness/Arith/D1.lean         |  5 ++-
 .../ISigmaOne/Metamath/Formula/Basic.lean     | 42 ++++++++++---------
 .../FirstOrder/Completeness/SubLanguage.lean  | 29 +------------
 .../Foundation/Modal/Kripke/Completeness.lean |  8 ++--
 .../Modal/Kripke/Hilbert/GL/Completeness.lean | 24 +++++++----
 5 files changed, 46 insertions(+), 62 deletions(-)

diff --git a/LeanPool/Incompleteness/Arith/D1.lean b/LeanPool/Incompleteness/Arith/D1.lean
index 6cc0cec64c..4e099d58c8 100644
--- a/LeanPool/Incompleteness/Arith/D1.lean
+++ b/LeanPool/Incompleteness/Arith/D1.lean
@@ -154,7 +154,10 @@ lemma quote_derivation_def
 
 @[simp] lemma fstidx_quote
     {Γ : Finset (SyntacticFormula L)} (d : T ⊢₂ Γ) : fstIdx (⌜d⌝ : V) = ⌜Γ⌝ := by
-  induction d <;> simp [quote_derivation_def, codeIn]
+  induction d <;>
+    simp only [quote_derivation_def, codeIn, fstIdx_axL, fstIdx_root, fstIdx_verumIntro,
+      fstIdx_andIntro, fstIdx_orIntro, fstIdx_allIntro, fstIdx_exIntro, fstIdx_wkRule,
+      fstIdx_shiftRule, fstIdx_cutRule]
 
 end Derivation2
 
diff --git a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean
index afbd63d396..ba84f836c1 100644
--- a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean
+++ b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean
@@ -1273,19 +1273,21 @@ lemma uformula_result_induction {P : V → V → V → Prop} (hP : Sg1-Relation
   rcases hp.case with
     (⟨k, r, v, hkr, hv, rfl⟩ | ⟨k, r, v, hkr, hv, rfl⟩ | rfl | rfl | ⟨p₁, p₂, hp₁, hp₂,
       rfl⟩ | ⟨p₁, p₂, hp₁, hp₂, rfl⟩ | ⟨p₁, hp₁, rfl⟩ | ⟨p₁, hp₁, rfl⟩)
-  · simpa [hkr, hv] using hRel param k r v hkr hv
-  · simpa [hkr, hv] using hNRel param k r v hkr hv
-  · simpa using hverum param
-  · simpa using hfalsum param
-  · simpa [c.result_and hp₁ hp₂] using
-      hand param p₁ p₂ hp₁ hp₂ (ih p₁ (by simp) param (by simp [f]) hp₁) (ih p₂ (by simp) param (by
-        simp [f]) hp₂)
-  · simpa [c.result_or hp₁ hp₂] using
-      hor param p₁ p₂ hp₁ hp₂ (ih p₁ (by simp) param (by simp [f]) hp₁) (ih p₂ (by simp) param (by
-        simp [f]) hp₂)
-  · simpa [c.result_all hp₁] using
+  · simpa only [c.result_rel hkr hv] using hRel param k r v hkr hv
+  · simpa only [c.result_nrel hkr hv] using hNRel param k r v hkr hv
+  · simpa only [c.result_verum] using hverum param
+  · simpa only [c.result_falsum] using hfalsum param
+  · simpa only [c.result_and hp₁ hp₂] using
+      hand param p₁ p₂ hp₁ hp₂
+        (ih p₁ (by simp) param (by simp [f]) hp₁)
+        (ih p₂ (by simp) param (by simp [f]) hp₂)
+  · simpa only [c.result_or hp₁ hp₂] using
+      hor param p₁ p₂ hp₁ hp₂
+        (ih p₁ (by simp) param (by simp [f]) hp₁)
+        (ih p₂ (by simp) param (by simp [f]) hp₂)
+  · simpa only [c.result_all hp₁] using
       hall param p₁ hp₁ (ih p₁ (by simp) (c.allChanges param) (by simp [f]) hp₁)
-  · simpa [c.result_ex hp₁] using
+  · simpa only [c.result_ex hp₁] using
       hex param p₁ hp₁ (ih p₁ (by simp) (c.exChanges param) (by simp [f]) hp₁)
 
 
@@ -1715,22 +1717,22 @@ lemma semiformula_result_induction {P : V → V → V → V → Prop} (hP : Sg1-
   rcases Language.IsSemiformula.case_iff.mp hp with
     (⟨k, R, v, hR, hv, rfl⟩ | ⟨k, R, v, hR, hv, rfl⟩ | rfl | rfl | ⟨p₁, p₂, h₁, h₂, rfl⟩ | ⟨p₁,
       p₂, h₁, h₂, rfl⟩ | ⟨p₁, h₁, rfl⟩ | ⟨p₁, h₁, rfl⟩)
-  · simpa [hR, hv.isUTerm] using hRel n param k R v hR hv
-  · simpa [hR, hv.isUTerm] using hNRel n param k R v hR hv
-  · simpa using hverum n param
-  · simpa using hfalsum n param
-  · simpa [h₁.isUFormula, h₂.isUFormula] using
+  · simpa only [c.result_rel hR hv.isUTerm] using hRel n param k R v hR hv
+  · simpa only [c.result_nrel hR hv.isUTerm] using hNRel n param k R v hR hv
+  · simpa only [c.result_verum] using hverum n param
+  · simpa only [c.result_falsum] using hfalsum n param
+  · simpa only [c.result_and h₁.isUFormula h₂.isUFormula] using
       hand n param p₁ p₂ h₁ h₂
         (ih p₁ (by simp) param (by simp [f]) n (by simp [g]) h₁)
         (ih p₂ (by simp) param (by simp [f]) n (by simp [g]) h₂)
-  · simpa [h₁.isUFormula, h₂.isUFormula] using
+  · simpa only [c.result_or h₁.isUFormula h₂.isUFormula] using
       hor n param p₁ p₂ h₁ h₂
         (ih p₁ (by simp) param (by simp [f]) n (by simp [g]) h₁)
         (ih p₂ (by simp) param (by simp [f]) n (by simp [g]) h₂)
-  · simpa [h₁.isUFormula] using
+  · simpa only [c.result_all h₁.isUFormula] using
       hall n param p₁ h₁
         (ih p₁ (by simp) (c.allChanges param) (by simp [f]) (n + 1) (by simp [g]) h₁)
-  · simpa [h₁.isUFormula] using
+  · simpa only [c.result_ex h₁.isUFormula] using
       hex n param p₁ h₁
         (ih p₁ (by simp) (c.exChanges param) (by simp [f]) (n + 1) (by simp [g]) h₁)
 
diff --git a/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean b/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean
index 9465151249..447d96df3b 100644
--- a/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean
+++ b/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean
@@ -84,21 +84,7 @@ def toSubLanguage' (pf : ∀ k, L.Func k → Prop) (pr : ∀ k, L.Rel k → Prop
     | bvar x => rfl
     | fvar x => rfl
     | func f v ih =>
-      have hv : (fun i => (toSubLanguage' pf pr (v i)
-          (fun k' f' h' => h k' f' (lang_func_ss f v i h'))).lMap L.ofSubLanguage) = v := by
-        funext i
-        exact ih i _
-      calc
-        (toSubLanguage' pf pr (func f v) h).lMap L.ofSubLanguage =
-            func ((L.ofSubLanguage).func ⟨f, h _ f (lang_func f v)⟩)
-              (fun i => (toSubLanguage' pf pr (v i)
-                (fun k' f' h' => h k' f' (lang_func_ss f v i h'))).lMap
-                  L.ofSubLanguage) := rfl
-        _ = func f (fun i => (toSubLanguage' pf pr (v i)
-              (fun k' f' h' => h k' f' (lang_func_ss f v i h'))).lMap
-                L.ofSubLanguage) := by
-          rfl
-        _ = func f v := congrArg (func f) hv
+      exact congrArg (func f) (funext fun i ↦ ih i _)
 
 end Semiterm
 
@@ -188,18 +174,7 @@ def toSubLanguage' (pf : ∀ k, L.Func k → Prop) (pr : ∀ k, L.Rel k → Prop
         (fun k f h => hf k f (langFunc_rel_ss r v i h))).lMap L.ofSubLanguage) = v := by
       funext i
       exact Semiterm.lMap_toSubLanguage' pf pr (v i) _
-    calc
-      lMap L.ofSubLanguage (toSubLanguage' pf pr (nrel r v) hf hr) =
-          nrel (L.ofSubLanguage.rel
-            ⟨r, hr _ r (by simp only [langRel, Finset.mem_singleton])⟩)
-            (fun i => ((v i).toSubLanguage' pf pr
-              (fun k f h => hf k f (langFunc_rel_ss r v i h))).lMap
-                L.ofSubLanguage) := rfl
-      _ = nrel r (fun i => ((v i).toSubLanguage' pf pr
-            (fun k f h => hf k f (langFunc_rel_ss r v i h))).lMap
-              L.ofSubLanguage) := by
-        rfl
-      _ = nrel r v := congrArg (nrel r) hv
+    exact congrArg (nrel r) hv
   case hall φ ih =>
     calc
       lMap L.ofSubLanguage (toSubLanguage' pf pr (∀' φ) hf hr) =
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Completeness.lean b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Completeness.lean
index ef421ea063..7195e52e5d 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Completeness.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Completeness.lean
@@ -37,7 +37,7 @@ namespace canonicalFrame
 
 variable {Ω₁ Ω₂ : (canonicalFrame 𝓢).World}
 
-@[simp] lemma rel_def_box : Ω₁ ≺ Ω₂ ↔ ∀ {φ}, □φ ∈ Ω₁ → φ ∈ Ω₂ := by simp [Frame.Rel']; aesop;
+@[simp] lemma rel_def_box : Ω₁ ≺ Ω₂ ↔ ∀ {φ}, □φ ∈ Ω₁ → φ ∈ Ω₂ := Iff.rfl
 
 lemma multirel_def_multibox : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, □^[n]φ ∈ Ω₁.1 → φ ∈ Ω₂.1 := by
   induction n generalizing Ω₁ Ω₂ with
@@ -91,10 +91,8 @@ lemma multirel_def_multibox : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, □^[n]φ ∈ Ω
         apply hΩ;
         simp_all;
 
-lemma multirel_def_multibox' : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, φ ∈ (□''⁻¹^[n]Ω₁.1) → φ ∈ Ω₂.1 := by
-  constructor;
-  · intro h φ hp; exact multirel_def_multibox.mp h hp;
-  · intro h; apply multirel_def_multibox.mpr; assumption;
+lemma multirel_def_multibox' : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, φ ∈ (□''⁻¹^[n]Ω₁.1) → φ ∈ Ω₂.1 :=
+  multirel_def_multibox
 
 lemma multirel_def_multidia : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, (φ ∈ Ω₂.1 → ◇^[n]φ ∈ Ω₁.1) :=
   Iff.trans multirel_def_multibox multibox_multidia
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean
index 0116af096b..ca9aa7e4d8 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean
@@ -42,15 +42,16 @@ namespace miniCanonicalFrame
 
 lemma is_irreflexive : Std.Irrefl (miniCanonicalFrame φ).Rel := by
   constructor
-  simp_all
+  rintro X ⟨_, χ, _, hnot, hmem⟩
+  exact hnot hmem
 
 lemma is_transitive : IsTrans (miniCanonicalFrame φ).World (miniCanonicalFrame φ).Rel := by
   constructor
-  rintro X Y Z ⟨RXY, ⟨χ, _, _, _⟩⟩ ⟨RYZ, _⟩;
-  constructor;
-  · simp_all
-  · use χ;
-    simp_all
+  rintro X Y Z ⟨RXY, ⟨χ, hχ, hnot, hmem⟩⟩ ⟨RYZ, _⟩
+  constructor
+  · intro ψ hψ hX
+    exact RYZ ψ hψ (RXY ψ hψ hX).2
+  · exact ⟨χ, hχ, hnot, (RYZ χ hχ hmem).2⟩
 
 end miniCanonicalFrame
 
@@ -174,9 +175,14 @@ lemma truthlemma {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformu
       push Not;
       use Y;
       constructor;
-      · constructor;
-        · aesop;
-        · aesop;
+      · constructor
+        · intro χ hχ hBox
+          have hprebox : χ ∈ X.1.prebox := by
+            change □χ ∈ X.1 at hBox
+            simpa only [Finset.eq_prebox_premultibox_one, Finset.mem_preimage,
+              Function.iterate_one] using hBox
+          exact ⟨hY₁.1.1 hprebox, hY₁.1.2 (Finset.mem_image.mpr ⟨χ, hprebox, rfl⟩)⟩
+        · exact ⟨ψ, q_sub, h, hY₁.2 (Finset.mem_insert_self _ _)⟩
       · apply ih ?_ |>.not.mpr;
         · apply iff_mem_compl (subformulas.mem_box q_sub) |>.not.mpr;
           push Not;

From 967e8fa8ed450a86a87702a9d7ceeca81a6d80e0 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Fri, 16 Oct 2026 15:50:10 +0000
Subject: [PATCH 3/3] perf(Incompleteness): reuse congruence and boxed-list
 inclusion

---
 .../FirstOrder/Completeness/SubLanguage.lean  |  8 +++-
 .../Modal/Kripke/Hilbert/GL/Completeness.lean | 46 +++++++++---------
 .../Kripke/Hilbert/Grz/Completeness.lean      |  5 +-
 .../Foundation/Modal/LogicSymbol.lean         | 16 +++++++
 .../Modal/MaximalConsistentSet.lean           | 48 +++++++------------
 .../Foundation/Modal/Subformulas.lean         | 14 ++++--
 6 files changed, 73 insertions(+), 64 deletions(-)

diff --git a/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean b/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean
index 447d96df3b..f60cad6117 100644
--- a/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean
+++ b/LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean
@@ -185,7 +185,13 @@ def toSubLanguage' (pf : ∀ k, L.Func k → Prop) (pr : ∀ k, L.Rel k → Prop
       lMap L.ofSubLanguage (toSubLanguage' pf pr (∃' φ) hf hr) =
           ∃' lMap L.ofSubLanguage (toSubLanguage' pf pr φ hf hr) := rfl
       _ = ∃' φ := congrArg Semiformula.ex (ih hf hr)
-  all_goals simp_all [toSubLanguage']
+  all_goals simp only [toSubLanguage']
+  case hverum => rfl
+  case hfalsum => rfl
+  case hand φ ψ ihp ihq =>
+    exact congrArg₂ Semiformula.and (ihp _ _) (ihq _ _)
+  case hor φ ψ ihp ihq =>
+    exact congrArg₂ Semiformula.or (ihp _ _) (ihq _ _)
 
 /-- Imported declaration from the Incompleteness formalization. -/
 noncomputable def languageFuncIndexed (φ : Semiformula L μ n) (k) : Finset (L.Func k) :=
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean
index ca9aa7e4d8..7b83f291ab 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean
@@ -65,24 +65,21 @@ abbrev miniCanonicalModel (φ : Formula ℕ) : Kripke.Model where
 lemma truthlemma_lemma1
   {X : ComplementClosedConsistentFinset Hilbert.GL φ.subformulas} (hq : □ψ ∈ φ.subformulas)
   : ((X.1.prebox ∪ X.1.prebox.modalBox) ∪ {□ψ, -ψ}) ⊆ φ.subformulas⁻ := by
-  intro χ hr;
-  replace hr : χ = □ψ ∨ χ = -ψ ∨ □χ ∈ X ∨ (∃ a, □a ∈ X ∧ □a = χ) := by simp at hr; tauto;
-  rcases hr with (rfl | rfl | hp | ⟨χ, hr, rfl⟩);
-  · apply Finset.mem_union.mpr;
-    tauto;
-  · apply Finset.mem_union.mpr;
-    right;
-    apply Finset.mem_image.mpr;
-    use ψ;
-    constructor;
-    · exact subformulas.mem_box hq;
-    · tauto;
-  · have := X.closed.subset hp;
-    have := FormulaFinset.complementary_mem_box (by apply subformulas.mem_imp₁) this;
-    apply Finset.mem_union.mpr;
-    left;
-    exact subformulas.mem_box this;
-  · exact X.closed.subset hr;
+  intro χ hr
+  simp only [Finset.mem_union, Finset.mem_insert, Finset.mem_singleton] at hr
+  rcases hr with (hprebox | hbox) | rfl | rfl
+  · have hp : □χ ∈ X.1 := by
+      simpa only [Finset.eq_prebox_premultibox_one, Finset.mem_preimage,
+        Function.iterate_one] using hprebox
+    have := X.closed.subset hp
+    have := FormulaFinset.complementary_mem_box (by apply subformulas.mem_imp₁) this
+    exact Finset.mem_union_left _ (subformulas.mem_box this)
+  · obtain ⟨χ, hχ, rfl⟩ := Finset.mem_image.mp hbox
+    apply X.closed.subset
+    simpa only [Finset.eq_prebox_premultibox_one, Finset.mem_preimage,
+      Function.iterate_one] using hχ
+  · exact Finset.mem_union_left _ hq
+  · exact Finset.mem_union_right _ (Finset.mem_image.mpr ⟨ψ, subformulas.mem_box hq, rfl⟩)
 
 
 lemma truthlemma_lemma2
@@ -93,14 +90,14 @@ lemma truthlemma_lemma2
   apply FormulaFinset.intro_union_consistent;
   rintro Γ₁ Γ₂ ⟨hΓ₁, hΓ₂⟩;
   replace hΓ₂ : ∀ χ ∈ Γ₂, χ = □ψ ∨ χ = -ψ := by
-    simp_all
+    simpa only [Finset.mem_insert, Finset.mem_singleton] using hΓ₂
   by_contra hC;
   have : Γ₁ ⊢[_]! ⋀Γ₂ ==> ⊥ := provable_iff.mpr <| and_imply_iff_imply_imply'!.mp hC;
   have : Γ₁ ⊢[_]! (□ψ ⋏ -ψ) ==> ⊥ := imp_trans''! (by
     suffices Γ₁ ⊢[Hilbert.GL]! ⋀[□ψ, -ψ] ==> ⋀Γ₂ by
-      simp_all
-    apply conjconj_subset!;
-    simpa using hΓ₂;
+      simpa only [List.conj₂_doubleton] using this
+    apply conjconj_subset!
+    simpa only [List.mem_cons, List.not_mem_nil, or_false] using hΓ₂
   ) this;
   have : Γ₁ ⊢[_]! □ψ ==> -ψ ==> ⊥ := and_imply_iff_imply_imply'!.mp this;
   have : Γ₁ ⊢[Hilbert.GL]! □ψ ==> ψ := by
@@ -113,8 +110,9 @@ lemma truthlemma_lemma2
   have : _ ⊢! ⋀□'Γ₁ ==> □ψ := provable_iff.mp this;
   have : _ ⊢! ⋀□'(X.1.prebox ∪ X.1.prebox.modalBox |>.toList) ==> □ψ :=
     imp_trans''! (conjconj_subset! (by
-    simp_all
-  )) this;
+      intro χ hχ
+      exact List.box_subset_mono (fun {ψ} hψ ↦ Finset.mem_toList.mpr (hΓ₁ ψ hψ)) hχ
+    )) this;
   have : _ ⊢! ⋀□'(X.1.prebox.toList) ==> □ψ := imp_trans''! (conjconj_provable! (by
     suffices ∀ χ, (□χ ∈ X ∨ ∃ χ', □χ' ∈ X ∧ □χ' =
       χ) → (□'^[1](Finset.premultibox 1 X).toList) ⊢[Hilbert.GL]! □χ by simpa;
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean
index 557f948fc6..017ef8052f 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/Grz/Completeness.lean
@@ -169,8 +169,9 @@ lemma truthlemma_lemma2
     have : (Hilbert.Grz) ⊢! ⋀□'Γ₁ ==> □ψ := imp_trans''! collect_box_conj! this;
     have : (Hilbert.Grz) ⊢! ⋀□'(X.1.prebox.modalBox |>.toList) ==> □ψ :=
       imp_trans''! (conjconj_subset! (by
-      simp_all
-    )) this;
+        intro χ hχ
+        exact List.box_subset_mono (fun {ψ} hψ ↦ Finset.mem_toList.mpr (hΓ₁ ψ hψ)) hχ
+      )) this;
     have : (Hilbert.Grz) ⊢! ⋀□'(X.1.prebox.toList) ==> □ψ := imp_trans''! (conjconj_provable! (by
       intro ψ hq;
       simp only [Finset.eq_prebox_premultibox_one, Finset.eq_box_multibox_one,
diff --git a/LeanPool/Incompleteness/Foundation/Modal/LogicSymbol.lean b/LeanPool/Incompleteness/Foundation/Modal/LogicSymbol.lean
index 40b29311b6..2ba7bc32f4 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/LogicSymbol.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/LogicSymbol.lean
@@ -571,3 +571,19 @@ end «lp_section_9»
 end List
 
 end «lp_section_1»
+
+namespace List
+
+/-- Applying the iterated box operation preserves inclusion of lists. -/
+lemma multibox_subset_mono {F : Type*} [DecidableEq F] [LO.Box F] {n : ℕ} {l₁ l₂ : List F}
+    (h : l₁ ⊆ l₂) : □'^[n]l₁ ⊆ □'^[n]l₂ := by
+  intro φ hφ
+  obtain ⟨ψ, hψ, rfl⟩ := Finset.mem_image.mp (Finset.mem_toList.mp hφ)
+  apply Finset.mem_toList.mpr
+  exact Finset.mem_image.mpr ⟨ψ, List.mem_toFinset.mpr (h (List.mem_toFinset.mp hψ)), rfl⟩
+
+/-- Applying the box operation preserves inclusion of lists. -/
+lemma box_subset_mono {F : Type*} [DecidableEq F] [LO.Box F] {l₁ l₂ : List F}
+    (h : l₁ ⊆ l₂) : □'l₁ ⊆ □'l₂ := multibox_subset_mono h
+
+end List
diff --git a/LeanPool/Incompleteness/Foundation/Modal/MaximalConsistentSet.lean b/LeanPool/Incompleteness/Foundation/Modal/MaximalConsistentSet.lean
index 4120119fb2..4387734a91 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/MaximalConsistentSet.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/MaximalConsistentSet.lean
@@ -275,22 +275,20 @@ lemma intro_triunion_consistent
   let Γ₂ := (Γ₁₂.filter (· ∈ T₂));
   apply unprovable_imp_trans''! (φ := ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃);
   · exact imp_trans''! (and₂'! <| and_assoc!) <| by
-      apply and_replace_left!;
-      apply imply_left_conj_concat!.mp;
-        apply conjconj_subset!;
-        intro φ hp;
-        simp only [List.mem_append, List.mem_filter, decide_eq_true_eq, Γ₁, Γ₂];
-        simp_all
-  · apply h;
-    refine ⟨?_, ?_, h₃⟩;
-    · intro φ hp;
-      rcases h₁₂ φ (List.mem_of_mem_filter hp) with (_ | _)
-      · assumption;
-      · simpa using List.of_mem_filter hp;
-    · intro φ hp;
-      rcases h₁₂ φ (List.mem_of_mem_filter hp) with (_ | _)
-      · have := List.of_mem_filter hp; simp_all
-      · assumption;
+      apply and_replace_left!
+      apply imply_left_conj_concat!.mp
+      apply conjconj_subset!
+      intro φ hp
+      simp only [List.mem_append, List.mem_filter, decide_eq_true_eq, Γ₁, Γ₂]
+      rcases h₁₂ φ hp with hφ | hφ
+      · exact Or.inl ⟨hp, hφ⟩
+      · exact Or.inr ⟨hp, hφ⟩
+  · apply h
+    refine ⟨?_, ?_, h₃⟩
+    · intro φ hp
+      simpa only [decide_eq_true_eq] using List.of_mem_filter hp
+    · intro φ hp
+      simpa only [decide_eq_true_eq] using List.of_mem_filter hp
 
 omit [DecidableEq α] in
 omit [Entailment.Classical 𝓢] in
@@ -619,22 +617,8 @@ lemma mem_dia_dual : ◇φ ∈ Ω ↔ (∼(□(∼φ)) ∈ Ω) := by classical
 omit [DecidableEq α] in
 lemma iff_mem_multidia : (◇^[n]φ ∈ Ω) ↔ (∃ Ω' :
     MaximalConsistentSet 𝓢, (□''⁻¹^[n]Ω.1 ⊆ Ω'.1) ∧ (φ ∈ Ω'.1)) := by classical
-  constructor;
-  · intro h;
-    have := mem_multidia_dual.mp h;
-    have := iff_mem_neg.mp this;
-    have := iff_mem_multibox.not.mp this;
-    push Not at this;
-    simp_all
-  · rintro ⟨Ω', h₁, h₂⟩;
-    apply mem_multidia_dual.mpr;
-    apply iff_mem_neg.mpr;
-    apply iff_mem_multibox.not.mpr;
-    push Not;
-    use Ω';
-    constructor;
-    · exact h₁;
-    · exact iff_mem_neg.mp <| iff_mem_negneg.mpr h₂;
+  simp only [mem_multidia_dual, iff_mem_neg, iff_mem_multibox, not_forall, not_not, exists_prop]
+  rfl
 omit [DecidableEq α] in
 lemma iff_mem_dia : (◇φ ∈ Ω) ↔ (∃ Ω' :
     MaximalConsistentSet 𝓢, (□''⁻¹Ω.1 ⊆ Ω'.1) ∧ (φ ∈ Ω'.1)) :=
diff --git a/LeanPool/Incompleteness/Foundation/Modal/Subformulas.lean b/LeanPool/Incompleteness/Foundation/Modal/Subformulas.lean
index de26304443..061d84628a 100644
--- a/LeanPool/Incompleteness/Foundation/Modal/Subformulas.lean
+++ b/LeanPool/Incompleteness/Foundation/Modal/Subformulas.lean
@@ -44,12 +44,15 @@ lemma mem_imp (h : (ψ ==> χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas ∧ 
   | himp φ₁ φ₂ ihp₁ ihp₂ =>
     simp only [subformulas, Finset.mem_insert, Finset.mem_union] at h ⊢
     rcases h with h_eq | h₁ | h₂
-    · simp_all
-    · simp_all
-    · simp_all
+    · cases h_eq
+      exact ⟨Or.inr (Or.inl mem_self), Or.inr (Or.inr mem_self)⟩
+    · exact ⟨Or.inr (Or.inl (ihp₁ h₁).1), Or.inr (Or.inl (ihp₁ h₁).2)⟩
+    · exact ⟨Or.inr (Or.inr (ihp₂ h₂).1), Or.inr (Or.inr (ihp₂ h₂).2)⟩
   | hbox _ ihp =>
     simp only [subformulas, Finset.mem_insert] at h ⊢
-    simp_all
+    rcases h with h_eq | h_sub
+    · cases h_eq
+    · exact ⟨Or.inr (ihp h_sub).1, Or.inr (ihp h_sub).2⟩
 
 lemma mem_imp₁ (h : (ψ ==> χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas := mem_imp h |>.1
 
@@ -72,7 +75,8 @@ lemma mem_box (h : □ψ ∈ φ.subformulas) : ψ ∈ φ.subformulas := by
   | hbox _ ihp =>
     simp only [subformulas, Finset.mem_insert] at h ⊢
     rcases h with h_eq | h_sub
-    · simp_all
+    · cases h_eq
+      exact Or.inr mem_self
     · exact Or.inr (ihp h_sub)
 
 -- TODO: add tactic like `subformulas`.