Fix simp regressions in ModalCompanion/Basic after deps update

Version bump broke three proofs that relied on simp computing
`2 * (n + 1)` and `Finset.filterMap` over a singleton:

- `negRepeat_succ_rw`: factor out `negRepeat_neg` and rewrite the
  multiplication explicitly before unfolding `negRepeat`.
- `notForces_double_negRepeat`: rewrite `2 * (n + 1)` to `2 * n + 1 + 1`
  so `simp [negRepeat]` can unfold the two negations.
- `modal_companion_VFSer`: add `star_singleton_dni` proving
  `{∼∼⊤}.star = {∼□∼□⊤}` via `ext`, and rewrite with it (plus
  `Finset.singleton_union`) instead of unfolding `Axioms.star`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: SnO2WMaN

VeryWeakSubintuitionistic/ModalCompanion/Basic.lean

@@ -164,9 +164,14 @@ def negRepeat : ℕ → Formula α → Formula α
 
 notation "∼^[" n "]" A => negRepeat n A
 
-lemma negRepeat_succ_rw {n : ℕ} : (∼^[2 * (n + 1)]A) = ∼(∼^[2 * n](∼A)) := by
+lemma negRepeat_neg {n : ℕ} : (∼^[n](∼A)) = ∼(∼^[n]A) := by
   induction n <;> simp_all [negRepeat];
 
+lemma negRepeat_succ_rw {n : ℕ} : (∼^[2 * (n + 1)]A) = ∼(∼^[2 * n](∼A)) := by
+  rw [negRepeat_neg];
+  rw [show 2 * (n + 1) = 2 * n + 1 + 1 by omega];
+  simp [negRepeat];
+
 end Modal.Formula
 
 
@@ -202,6 +207,7 @@ lemma notForces_double_negRepeat {M : Model κ α} {x : M.World} : (x ⊩ (∼^[
   | zero => grind;
   | succ n ih =>
     apply Iff.trans ?_ ih;
+    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by omega];
     simp [Modal.Formula.negRepeat];
     grind;
 
@@ -296,14 +302,19 @@ theorem modal_companion_VF {A : Formula α} {N : Finset ℕ} : List.TFAE [
   have : Fact (∀ B ∈ (∅ : Axioms α), B.IsClosedNegativeAxiom) := ⟨by grind⟩;
   simpa [Axioms.star] using modal_companion (Λ := ∅);
 
+omit [DecidableEq α] in
+private lemma star_singleton_dni : ({ (∼∼⊤ : Formula α) } : Axioms α).star = { (∼□∼□⊤ : Modal.Formula α) } := by
+  ext B;
+  simp [Axioms.star, Formula.corsi, eq_comm];
+
 /-- Corollary 6.13 -/
 theorem modal_companion_VFSer {A : Formula α} {N : Finset ℕ} : List.TFAE [
   ({(∼∼⊤ : Formula α)}) ⊢ⱽ A,
   ({(∼□∼□⊤ : Modal.Formula α)}) ⊢ᴺ A.corsi,
   (insert (∼□∼□⊤ : Modal.Formula α) (N.image (λ n => ∼□(∼^[2 * n]⊥)))) ⊢ᴺ A.corsi
 ] := by
   have : Fact (∀ B ∈ ({ (∼∼⊤ : Formula α) } : Axioms α), B.IsClosedNegativeAxiom) := ⟨by grind⟩;
-  simpa [Axioms.star] using modal_companion (Λ := { (∼∼⊤ : Formula α) });
+  simpa [star_singleton_dni, Finset.singleton_union] using modal_companion (Λ := { (∼∼⊤ : Formula α) });
 
 
 end