Proof.expand_onlyAtomicAxioms

Author: chenson2018

Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean

@@ -123,6 +123,18 @@ private lemma Proof.expand_onlyAtomicAxioms_dual {a : Proposition Atom} :
 open Proposition Proof in
 /-- η-expansion is correct: the proof returned by η-expansion contains only atomic axioms. -/
 theorem Proof.expand_onlyAtomicAxioms (a : Proposition Atom) : a.expand.onlyAtomicAxioms := by
-  induction a <;> grind [onlyAtomicAxioms_rwConclusion]
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+  induction a with
+  | one =>
+    rw [←dual_involution .one]
+    apply expand_onlyAtomicAxioms_dual
+    simp [expand, onlyAtomicAxioms, dual]
+  | zero =>
+    rw [←dual_involution .zero]
+    apply expand_onlyAtomicAxioms_dual
+    simp [expand, onlyAtomicAxioms, dual]
+  | top | bot => simp [expand, onlyAtomicAxioms]
+  | _ => grind
 
 end Cslib.CLL