From 4bde46f9b1014ec194668123d525703e0958b3f3 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 23 Jan 2026 03:47:46 -0500
Subject: [PATCH 1/5] perf: PR for radar testing of Fsub

---
 .../LocallyNameless/Fsub/Reduction.lean           |  4 +---
 .../LocallyNameless/Fsub/Safety.lean              | 12 ++++++------
 .../LocallyNameless/Fsub/Subtype.lean             |  4 ++--
 .../LocallyNameless/Fsub/Typing.lean              |  3 ++-
 .../LocallyNameless/Fsub/WellFormed.lean          | 15 +++------------
 CslibTests/GrindLint.lean                         |  4 ----
 6 files changed, 14 insertions(+), 28 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean
index 69b0ac20..77253934 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean
@@ -45,7 +45,6 @@ variable {t₁ t₂ t₃ : Term Var}
 variable [DecidableEq Var]
 
 /-- Locally closed let bindings have a locally closed body. -/
-@[scoped grind _=_]
 lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by
   constructor <;> intro h <;> cases h
   case mp.let' L t₁_lc h => exact ⟨t₁_lc, L, h⟩
@@ -54,7 +53,6 @@ lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by
     grind [LC.let' <| free_union Var]
 
 /-- Locally closed case bindings have a locally closed bodies. -/
-@[scoped grind _=_]
 lemma body_case : (case t₁ t₂ t₃).LC ↔ t₁.LC ∧ t₂.body ∧ t₃.body := by
   constructor <;> intro h
   case mp => cases h with | case L t₁_lc h₂ h₃ => exact ⟨t₁_lc, ⟨L, h₂⟩, ⟨L, h₃⟩⟩
@@ -115,7 +113,7 @@ lemma Red.lc {t t' : Term Var} (red : t ⭢βᵛ t') : t.LC ∧ t'.LC := by
       grind [
         fresh_exists <| free_union [fv_tm, fv_ty] Var, subst_tm_lc,
         subst_ty_lc, open_tm_subst_tm_intro, open_ty_subst_ty_intro]
-  all_goals grind
+  all_goals grind [body_let, body_case]
 
 end Term
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
index fa3afd88..683b8139 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
@@ -110,11 +110,11 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
     cases ih der with
     | inl _ =>
         exists t₂ ^ᵗᵗ t₁
-        grind
+        grind [body_let]
     | inr red =>
         obtain ⟨t₁', _⟩ := red
         exists t₁'.let' t₂
-        grind
+        grind [body_let]
   case inl der _ ih =>
     cases (ih der) with
     | inl val => grind
@@ -136,20 +136,20 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
     cases ih der with
     | inl val =>
         have ⟨t₁, lr⟩ := der.canonical_form_sum val
-        cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind
+        cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind [body_case]
     | inr red =>
         obtain ⟨t₁', _⟩ := red
         exists t₁'.case t₂ t₃
-        grind
+        grind [body_case]
   case sub => grind
   case abs σ _ τ L _ _=>
     left
     constructor
-    apply LC.abs L <;> grind [cases Env.Wf, cases Term.LC]
+    apply LC.abs L <;> grind [cases Term.LC]
   case tabs L _ _=>
     left
     constructor
-    apply LC.tabs L <;> grind [cases Env.Wf, cases Term.LC]
+    apply LC.tabs L <;> grind [cases Term.LC]
 
 end LambdaCalculus.LocallyNameless.Fsub
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
index e27d7d34..bb0fd870 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
@@ -61,7 +61,7 @@ lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.W
 /-- Subtypes are reflexive when well-formed. -/
 lemma refl (wf_Γ : Γ.Wf) (wf_σ : σ.Wf Γ) : Sub Γ σ σ := by
   induction wf_σ with
-  | all => grind [all (free_union [Context.dom] Var)]
+  | all => grind [all (free_union [Context.dom] Var), Env.Wf.sub, Env.Wf.ty]
   | _ => grind
 
 /-- Weakening of subtypes. -/
@@ -70,7 +70,7 @@ lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ
   induction sub generalizing Γ
   case all =>
     subst eq
-    apply all (free_union [Context.dom] Var) <;> grind
+    apply all (free_union [Context.dom] Var) <;> grind [Env.Wf.sub, Env.Wf.ty]
   all_goals grind [Ty.Wf.weaken, <= sublist_dlookup]
 
 lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 9743f2ab..08177824 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -86,7 +86,8 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
   case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
   case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
   all_goals
-    grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup]
+    grind [Env.Wf.sub, Env.Wf.ty, Wf.weaken, Sub.weaken,
+      Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup]
 
 /-- Weakening of typings (at the front). -/
 lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) :
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
index 34c5172d..13a5a70b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
@@ -49,8 +49,6 @@ inductive Env.Wf : Env Var → Prop
   | sub : Wf Γ → τ.Wf Γ → X ∉ Γ.dom → Wf (⟨X, Binding.sub τ⟩ :: Γ)
   | ty : Wf Γ → τ.Wf Γ → x ∉ Γ.dom → Wf (⟨x, Binding.ty τ⟩ :: Γ)
 
-attribute [scoped grind! .] Env.Wf.sub Env.Wf.ty
-
 variable {Γ Δ Θ : Env Var} {σ τ τ' γ δ : Ty Var}
 
 open scoped Context in
@@ -98,14 +96,7 @@ lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨
   generalize eq : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ) = Θ at wf
   induction wf generalizing Γ with
   | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons]
-  | _ =>
-    #adaptation_note
-    /--
-    Moving from `nightly-2025-09-15` to `nightly-2025-10-19`,
-    I've had to remove the `append_assoc` lemma from grind;
-    without this `grind` is exploding. This requires further investigation.
-    -/
-    grind [sublist_dlookup, -append_assoc]
+  | _ => grind [sublist_dlookup]
 
 lemma narrow_cons (wf : σ.Wf (⟨X, Binding.sub τ⟩ :: Δ)) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) :
     σ.Wf (⟨X, Binding.sub τ'⟩ :: Δ) := by
@@ -167,11 +158,11 @@ open Context List Binding
 lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) :
     Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
   induction Γ <;> cases wf_env <;>
-  grind [Ty.Wf.narrow, eq_nil_of_append_eq_nil, cases Env.Wf]
+  grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.narrow]
 
 /-- A context remains well-formed under strengthening. -/
 lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by
-  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen]
+  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen, Env.Wf.sub, Env.Wf.ty]
 
 variable [HasFresh Var] in
 /-- A context remains well-formed under substitution (of a well-formed type). -/
diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean
index 6eb56e31..33a4e2ed 100644
--- a/CslibTests/GrindLint.lean
+++ b/CslibTests/GrindLint.lean
@@ -59,8 +59,6 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.arrow
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.sum
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.trans_tvar
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.body_case
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.body_let
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_tm_body
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.app
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.inl
@@ -69,8 +67,6 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.tapp
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_subst
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.sub
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty
 
 #guard_msgs in
 #grind_lint check (min := 20) in Cslib

From b6c57208e52eb96822c60fb8e7a736788ec975ef Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 23 Jan 2026 04:01:24 -0500
Subject: [PATCH 2/5] out back -append_assoc

---
 .../LocallyNameless/Fsub/WellFormed.lean            | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
index 13a5a70b..aae28f88 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
@@ -96,7 +96,14 @@ lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨
   generalize eq : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ) = Θ at wf
   induction wf generalizing Γ with
   | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons]
-  | _ => grind [sublist_dlookup]
+  | _ =>
+    #adaptation_note
+    /--
+    Moving from `nightly-2025-09-15` to `nightly-2025-10-19`,
+    I've had to remove the `append_assoc` lemma from grind;
+    without this `grind` is exploding. This requires further investigation.
+    -/
+    grind [sublist_dlookup, -append_assoc]
 
 lemma narrow_cons (wf : σ.Wf (⟨X, Binding.sub τ⟩ :: Δ)) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) :
     σ.Wf (⟨X, Binding.sub τ'⟩ :: Δ) := by
@@ -158,11 +165,11 @@ open Context List Binding
 lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) :
     Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
   induction Γ <;> cases wf_env <;>
-  grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.narrow]
+  grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.narrow, eq_nil_of_append_eq_nil, cases Env.Wf]
 
 /-- A context remains well-formed under strengthening. -/
 lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by
-  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen, Env.Wf.sub, Env.Wf.ty]
+  induction Γ <;> cases wf <;> grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.strengthen]
 
 variable [HasFresh Var] in
 /-- A context remains well-formed under substitution (of a well-formed type). -/

From 4ab525249a894fc4a3649308dfa291abb64ca876 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 23 Jan 2026 04:10:15 -0500
Subject: [PATCH 3/5] rm some cases

---
 .../Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean | 2 +-
 .../LambdaCalculus/LocallyNameless/Fsub/Subtype.lean          | 4 ++--
 .../LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean       | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
index 683b8139..b1ca7b1a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
@@ -68,7 +68,7 @@ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing
     case case_inr der _ _ =>
       have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub
       grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm]
-  all_goals grind [cases Red]
+  all_goals grind
 
 /-- Any typable term either has a reduction step or is a value. -/
 lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
index bb0fd870..3e5c7d3b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
@@ -55,7 +55,7 @@ variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var}
 @[grind →]
 lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by
   induction sub with
-  | all => grind [Wf.all (free_union Var), Wf.narrow_cons, cases Env.Wf, cases LC]
+  | all => grind [Wf.all (free_union Var), Wf.narrow_cons]
   | _ => grind
 
 /-- Subtypes are reflexive when well-formed. -/
@@ -109,7 +109,7 @@ lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by
   case top => cases sub₁ <;> cases sub₂ <;> grind
   case var X =>
     generalize eq : fvar X = γ at sub₁
-    induction sub₁ <;> grind [cases Sub]
+    induction sub₁ <;> grind
   case arrow σ' τ' _ _ _ _ =>
     generalize eq : σ'.arrow τ' = γ at sub₁
     induction sub₁ <;> grind [cases Sub]
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
index aae28f88..e7276be4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
@@ -165,7 +165,7 @@ open Context List Binding
 lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) :
     Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
   induction Γ <;> cases wf_env <;>
-  grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.narrow, eq_nil_of_append_eq_nil, cases Env.Wf]
+  grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.narrow]
 
 /-- A context remains well-formed under strengthening. -/
 lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by

From dee05e5f3c745b629fdc49cf5c0dd35ff9f8c7bc Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 23 Jan 2026 04:15:45 -0500
Subject: [PATCH 4/5] rm a rule

---
 .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean          | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 08177824..bc63f25a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -85,9 +85,8 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
   case' tabs => apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
   case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
   case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
-  all_goals
-    grind [Env.Wf.sub, Env.Wf.ty, Wf.weaken, Sub.weaken,
-      Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup]
+  all_goals grind 
+    [Env.Wf.sub, Env.Wf.ty, Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, <= sublist_dlookup]
 
 /-- Weakening of typings (at the front). -/
 lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) :

From 7afc30323ca27777cf36820ff53f6bb742d3fac2 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 23 Jan 2026 04:22:34 -0500
Subject: [PATCH 5/5] lint

---
 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index bc63f25a..e5038bda 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -85,7 +85,7 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
   case' tabs => apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
   case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
   case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
-  all_goals grind 
+  all_goals grind
     [Env.Wf.sub, Env.Wf.ty, Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, <= sublist_dlookup]
 
 /-- Weakening of typings (at the front). -/