WIP: clean-slate restructure of Möbius file — no Classical anywhere

Drops `attribute [local instance 0] Classical.decRel` and all `open Classical in`
blocks. Restructures helpers to use `Set.Finite.toFinset` (noncomputable, but no
per-graph `Fintype` synthesis required) instead of `edgeFinset`.

The kernel is split into two pieces (degenerate `Icc G G` case and strict
`G < L` case) to avoid `if-then-else` in the signature, which would require
`DecidableEq (SimpleGraph V)`.

Four `sorry`s remain:
* `natCard_edgeSet_eq_add_card_sdiff` — bridge between `Nat.card K.edgeSet` and
  `Nat.card G.edgeSet + #(edgeSetSdiffFinset G K)`.
* `iccEquivPowersetEdgeFinsetSdiff` — `left_inv` / `right_inv`.
* `sum_Icc_neg_one_pow_natCard_edgeSet_of_lt` — alternating-sum collapse via
  `Finset.sum_powerset_neg_one_pow_card`.
* `embeddingCount_eq_sum_signed_copyCount` — main proof.

This commit lands the signature shape (all `Classical`-free) and lets the
proofs follow in subsequent commits.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Inversion.lean

@@ -166,156 +166,95 @@ identity `Finset.sum_powerset_neg_one_pow_card`.
 
 section Mobius
 
-attribute [local instance 0] Classical.decRel
-
-/-- Order-isomorphism between the closed interval `Finset.Icc G K` of graphs and the
-powerset of the edge difference `K.edgeFinset \ G.edgeFinset`, valid when `G ≤ K`.
-
-The forward map sends a graph `G'` with `G ≤ G' ≤ K` to its "extra edges over `G`",
-namely `G'.edgeFinset \ G.edgeFinset`. The inverse sends a subset `S` of "missing edges
-of `G` inside `K`" to the graph whose edge set is `G.edgeFinset ∪ S`, constructed via
-`fromEdgeSet`. -/
-noncomputable def iccEquivPowersetEdgeFinsetSdiff [Fintype V] [DecidableEq V]
-    [DecidableLE (SimpleGraph V)] {G K : SimpleGraph V} (hGK : G ≤ K) :
-    ↥(Finset.Icc G K) ≃ ↥(K.edgeFinset \ G.edgeFinset).powerset where
+variable [Fintype V] [DecidableEq V] [DecidableLE (SimpleGraph V)]
+
+/-! ### Finset of extra edges
+
+Helper construction giving the Finset of edges in `K` but not in `G`, without requiring a
+per-graph `Fintype` instance on the edge sets. Uses `Set.Finite.toFinset` (noncomputable). -/
+
+/-- The set difference of edge sets on a finite vertex type is finite. -/
+lemma edgeSet_sdiff_finite (G K : SimpleGraph V) : (K.edgeSet \ G.edgeSet).Finite :=
+  Set.finite_univ.subset (Set.subset_univ _)
+
+/-- The Finset of edges in `K` but not in `G`. Constructed via `Set.Finite.toFinset`,
+so noncomputable, but requires no per-graph `Fintype` synthesis. -/
+noncomputable def edgeSetSdiffFinset (G K : SimpleGraph V) : Finset (Sym2 V) :=
+  (edgeSet_sdiff_finite G K).toFinset
+
+@[simp] lemma mem_edgeSetSdiffFinset {G K : SimpleGraph V} {e : Sym2 V} :
+    e ∈ edgeSetSdiffFinset G K ↔ e ∈ K.edgeSet ∧ e ∉ G.edgeSet :=
+  Set.Finite.mem_toFinset _
+
+/-- Under `G ≤ K`, `Nat.card K.edgeSet = Nat.card G.edgeSet + #(edgeSetSdiffFinset G K)`. -/
+lemma natCard_edgeSet_eq_add_card_sdiff {G K : SimpleGraph V} (hGK : G ≤ K) :
+    Nat.card K.edgeSet = Nat.card G.edgeSet + #(edgeSetSdiffFinset G K) := by
+  sorry
+
+/-! ### Bijection between Icc and powerset of extra edges -/
+
+/-- Equivalence between the closed interval `Finset.Icc G K` of graphs and the powerset of
+the Finset of edges in `K` not in `G`, when `G ≤ K`.
+
+Forward: `G' ∈ [G, K]` maps to the Finset `edgeSetSdiffFinset G G'.val` (its extra edges
+over `G`, automatically a subset of `edgeSetSdiffFinset G K` since `G' ≤ K`).
+
+Inverse: a subset `S ⊆ edgeSetSdiffFinset G K` maps to `fromEdgeSet (G.edgeSet ∪ ↑S)`. -/
+noncomputable def iccEquivPowersetEdgeFinsetSdiff
+    {G K : SimpleGraph V} (hGK : G ≤ K) :
+    ↥(Finset.Icc G K) ≃ ↥(edgeSetSdiffFinset G K).powerset where
   toFun G' :=
-    ⟨G'.val.edgeFinset \ G.edgeFinset, by
-      simp only [Finset.mem_powerset]
-      exact Finset.sdiff_subset_sdiff (edgeFinset_mono (Finset.mem_Icc.mp G'.prop).2)
-        Finset.Subset.rfl⟩
+    ⟨edgeSetSdiffFinset G G'.val, by
+      rw [Finset.mem_powerset]
+      intro e he
+      rw [mem_edgeSetSdiffFinset] at he ⊢
+      exact ⟨edgeSet_subset_edgeSet.mpr (Finset.mem_Icc.mp G'.prop).2 he.1, he.2⟩⟩
   invFun S :=
-    ⟨fromEdgeSet ((G.edgeFinset : Set (Sym2 V)) ∪ S.val), by
-      have hSK : S.val ⊆ K.edgeFinset \ G.edgeFinset := Finset.mem_powerset.mp S.prop
+    ⟨fromEdgeSet (G.edgeSet ∪ ↑S.val), by
+      have hSK : ∀ e ∈ S.val, e ∈ K.edgeSet ∧ e ∉ G.edgeSet := fun e he => by
+        have := Finset.mem_powerset.mp S.prop he
+        rwa [mem_edgeSetSdiffFinset] at this
       refine Finset.mem_Icc.mpr ⟨fun a b hab => ?_, ?_⟩
-      · exact (fromEdgeSet_adj _).mpr ⟨.inl (mem_coe.mpr <| mem_edgeFinset.mpr hab), hab.ne⟩
+      · exact (fromEdgeSet_adj _).mpr ⟨.inl hab, hab.ne⟩
       · rw [fromEdgeSet_le]
         rintro e ⟨heGS | heGS, _⟩
-        · exact edgeSet_subset_edgeSet.mpr hGK (mem_edgeFinset.mp heGS)
-        · exact mem_edgeFinset.mp (Finset.mem_sdiff.mp (hSK heGS)).1⟩
-  left_inv := by
-    rintro ⟨G', hG'⟩
-    have hGG' : G ≤ G' := (Finset.mem_Icc.mp hG').1
-    apply Subtype.ext
-    ext a b
-    simp only [fromEdgeSet_adj, Set.mem_union, mem_coe, mem_edgeFinset, Finset.coe_sdiff,
-      Set.mem_diff]
-    refine ⟨fun ⟨h, _⟩ => h.elim (hGG' ·) (·.1), fun h => ⟨?_, h.ne⟩⟩
-    by_cases hG : G.Adj a b
-    · exact .inl hG
-    · exact .inr ⟨h, hG⟩
-  right_inv := by
-    rintro ⟨S, hS⟩
-    have hSK : S ⊆ K.edgeFinset \ G.edgeFinset := Finset.mem_powerset.mp hS
-    apply Subtype.ext
-    ext e
-    simp only [Finset.mem_sdiff, mem_edgeFinset, edgeSet_fromEdgeSet, Set.mem_diff,
-      Set.mem_union, mem_coe]
-    refine ⟨?_, fun heS => ?_⟩
-    · rintro ⟨⟨h | h, _⟩, heG⟩
-      · exact absurd h heG
-      · exact h
-    · have heKsd := Finset.mem_sdiff.mp (hSK heS)
-      refine ⟨⟨.inr heS, fun hd =>
-        K.not_isDiag_of_mem_edgeSet (mem_edgeFinset.mp heKsd.1) hd⟩, ?_⟩
-      exact fun heG => heKsd.2 (mem_edgeFinset.mpr heG)
-
-/-- The combinatorial kernel of Möbius inversion at the graph level: the alternating sum of
-`(-1) ^ #(K' \ G)` over `K'` in a closed interval `[G, L]` collapses to `1` when `L = G` and
-`0` otherwise. Reindexes via `iccEquivPowersetEdgeFinsetSdiff` to
-`Finset.sum_powerset_neg_one_pow_card`. -/
-private theorem sum_Icc_neg_one_pow_card_edgeFinset_sdiff_eq_ite
-    [Fintype V] [DecidableEq V] [DecidableLE (SimpleGraph V)]
-    {G L : SimpleGraph V} (hGL : G ≤ L) :
-    ∑ K' ∈ Finset.Icc G L, (-1 : ℤ) ^ #(K'.edgeFinset \ G.edgeFinset)
-      = if L = G then 1 else 0 := by
-  have key : ∑ K' ∈ Finset.Icc G L, (-1 : ℤ) ^ #(K'.edgeFinset \ G.edgeFinset)
-      = ∑ S ∈ (L.edgeFinset \ G.edgeFinset).powerset, (-1 : ℤ) ^ #S := by
-    rw [← Finset.sum_attach (Finset.Icc G L)
-          (fun K' => (-1 : ℤ) ^ #(K'.edgeFinset \ G.edgeFinset)),
-        ← Finset.sum_attach (L.edgeFinset \ G.edgeFinset).powerset
-          (fun S => (-1 : ℤ) ^ #S)]
-    exact Finset.sum_equiv (iccEquivPowersetEdgeFinsetSdiff hGL)
-      (fun _ => by simp) (fun _ _ => rfl)
-  rw [key, Finset.sum_powerset_neg_one_pow_card]
-  obtain rfl | hLG := eq_or_ne L G
-  · simp
-  · rw [if_neg, if_neg hLG]
-    intro hempty
-    apply hLG
-    have hsub : L ≤ G := by
-      simpa [Finset.sdiff_eq_empty_iff_subset, edgeFinset_subset_edgeFinset] using hempty
-    exact le_antisymm hsub hGL
-
-/-- Auxiliary form of the Möbius inverse with sign `(-1) ^ #(G'.edgeFinset \ G.edgeFinset)`.
-The user-facing version `embeddingCount_eq_sum_signed_copyCount` factors the sign through
-`Nat.card G.edgeSet * Nat.card G'.edgeSet`, eliminating per-graph `Fintype` hypotheses from
-the signature. -/
-private theorem embeddingCount_eq_sum_signed_copyCount_aux [Fintype V] [DecidableEq V]
-    [DecidableLE (SimpleGraph V)] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    (H.embeddingCount G : ℤ) =
-      ∑ G' ∈ Finset.Icc G ⊤,
-        (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset) * (H.copyCount G' : ℤ) := by
-  symm
-  calc ∑ G' ∈ Finset.Icc G ⊤,
-          (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset) * (H.copyCount G' : ℤ)
-      -- Substitute the forward identity into each summand.
-      = ∑ G' ∈ Finset.Icc G ⊤, ∑ L ∈ Finset.Icc G' ⊤,
-          (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset) * (H.embeddingCount L : ℤ) := by
-        simp_rw [copyCount_eq_sum_embeddingCount, Nat.cast_sum, Finset.mul_sum]
-      -- Swap the order of summation over the triangle `G ≤ G' ≤ L ≤ ⊤`.
-    _ = ∑ L ∈ Finset.Icc G ⊤, ∑ G' ∈ Finset.Icc G L,
-          (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset) * (H.embeddingCount L : ℤ) := by
-        rw [Finset.sum_comm' (s := Finset.Icc G (⊤ : SimpleGraph V))
-            (t := fun G' => Finset.Icc G' ⊤)
-            (s' := fun L => Finset.Icc G L) (t' := Finset.Icc G (⊤ : SimpleGraph V))
-            (h := fun G' L => by
-              simp only [Finset.mem_Icc]
-              exact ⟨fun ⟨⟨hGG', _⟩, hG'L, _⟩ => ⟨⟨hGG', hG'L⟩, hGG'.trans hG'L, le_top⟩,
-                     fun ⟨⟨hGG', hG'L⟩, _⟩ => ⟨⟨hGG', le_top⟩, hG'L, le_top⟩⟩)]
-      -- Factor `H.embeddingCount L` out of the inner sum.
-    _ = ∑ L ∈ Finset.Icc G ⊤, (H.embeddingCount L : ℤ) *
-          ∑ G' ∈ Finset.Icc G L, (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset) := by
-        simp_rw [mul_comm ((-1 : ℤ) ^ _) ((H.embeddingCount _ : ℤ)), ← Finset.mul_sum]
-      -- Inner sum collapses to `δ_{L = G}` by the kernel lemma.
-    _ = ∑ L ∈ Finset.Icc G ⊤, (H.embeddingCount L : ℤ) * (if L = G then 1 else 0) := by
-        refine Finset.sum_congr rfl fun L hL => ?_
-        rw [sum_Icc_neg_one_pow_card_edgeFinset_sdiff_eq_ite (Finset.mem_Icc.mp hL).1]
-      -- Only the `L = G` term survives.
-    _ = (H.embeddingCount G : ℤ) := by
-        simp_rw [mul_ite, mul_one, mul_zero]
-        rw [Finset.sum_ite_eq' (Finset.Icc G ⊤) G fun L => (H.embeddingCount L : ℤ),
-            if_pos (Finset.mem_Icc.mpr ⟨le_refl _, le_top⟩)]
-
-/-- Sign factorization: under `G ≤ G'`, the parity of `#(G'.edgeFinset \ G.edgeFinset)`
-equals the sum of the parities of `Nat.card G.edgeSet` and `Nat.card G'.edgeSet`. -/
-private lemma neg_one_pow_card_edgeFinset_sdiff [Fintype V] [DecidableEq V]
-    {G G' : SimpleGraph V} (hGG' : G ≤ G') :
-    (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset)
-      = (-1 : ℤ) ^ Nat.card G.edgeSet * (-1 : ℤ) ^ Nat.card G'.edgeSet := by
-  rw [show Nat.card G.edgeSet = #G.edgeFinset from
-        Nat.card_eq_fintype_card.trans G.card_edgeSet,
-      show Nat.card G'.edgeSet = #G'.edgeFinset from
-        Nat.card_eq_fintype_card.trans G'.card_edgeSet,
-      show #G'.edgeFinset = #G.edgeFinset + #(G'.edgeFinset \ G.edgeFinset) by
-        have := Finset.card_sdiff_add_card_eq_card (edgeFinset_mono hGG'); omega,
-      pow_add, ← mul_assoc, ← pow_add,
-      show (-1 : ℤ) ^ (#G.edgeFinset + #G.edgeFinset) = 1 from Even.neg_one_pow ⟨_, rfl⟩,
-      one_mul]
+        · exact edgeSet_subset_edgeSet.mpr hGK heGS
+        · exact (hSK e (Finset.mem_coe.mp heGS)).1⟩
+  left_inv := by sorry
+  right_inv := by sorry
+
+/-! ### Combinatorial kernel
+
+Split into two pieces, avoiding `if-then-else` (which would require `DecidableEq` on
+`SimpleGraph V`). Consumers case-split on `G = L vs G < L` via `eq_or_lt_of_le`. -/
+
+/-- Degenerate case: the alternating sum over a singleton interval. -/
+lemma sum_Icc_self_neg_one_pow_natCard_edgeSet (G : SimpleGraph V) :
+    ∑ K' ∈ Finset.Icc G G, (-1 : ℤ) ^ Nat.card K'.edgeSet
+      = (-1 : ℤ) ^ Nat.card G.edgeSet := by
+  rw [Finset.Icc_self, Finset.sum_singleton]
+
+/-- Strictly-larger case: the alternating sum over `Icc G L` with `G < L` is zero. -/
+lemma sum_Icc_neg_one_pow_natCard_edgeSet_of_lt
+    {G L : SimpleGraph V} (hGL : G < L) :
+    ∑ K' ∈ Finset.Icc G L, (-1 : ℤ) ^ Nat.card K'.edgeSet = 0 := by
+  sorry
+
+/-! ### Main Möbius identity -/
 
 /-- The Möbius (signed-sum) inverse to `copyCount_eq_sum_embeddingCount`. The induced copy
 count is expressed as a signed sum of copy counts over supergraphs `G' ∈ Icc G ⊤`, with the
-sign factored as `(-1) ^ Nat.card G.edgeSet * (-1) ^ Nat.card G'.edgeSet` — equivalently
-`(-1) ^ #(G'.edgeFinset \ G.edgeFinset)`, but stated via `Nat.card` so no per-graph
-`Fintype` hypothesis on the edge sets appears in the signature. -/
-theorem embeddingCount_eq_sum_signed_copyCount [Fintype V] [DecidableEq V]
-    [DecidableLE (SimpleGraph V)] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W) :
+sign factored as `(-1)^Nat.card G.edgeSet * (-1)^Nat.card G'.edgeSet`.
+
+The `Nat.card` form keeps the signature free of per-graph `Fintype` synthesis on edge sets
+(and hence free of `Classical`). -/
+theorem embeddingCount_eq_sum_signed_copyCount [Finite W]
+    (G : SimpleGraph V) (H : SimpleGraph W) :
     (H.embeddingCount G : ℤ) =
       (-1 : ℤ) ^ Nat.card G.edgeSet *
         ∑ G' ∈ Finset.Icc G ⊤,
           (-1 : ℤ) ^ Nat.card G'.edgeSet * (H.copyCount G' : ℤ) := by
-  rw [embeddingCount_eq_sum_signed_copyCount_aux, Finset.mul_sum]
-  refine Finset.sum_congr rfl fun G' hG' => ?_
-  rw [neg_one_pow_card_edgeFinset_sdiff (Finset.mem_Icc.mp hG').1, mul_assoc]
+  sorry
 
 end Mobius