feat(Combinatorics/SimpleGraph/Inversion): add Möbius inversion between copy counts and induced copy counts

Mathlib.lean

@@ -3623,6 +3623,7 @@ public import Mathlib.Combinatorics.SetFamily.Shadow
 public import Mathlib.Combinatorics.SetFamily.Shatter
 public import Mathlib.Combinatorics.SimpleGraph.Acyclic
 public import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
+public import Mathlib.Combinatorics.SimpleGraph.Automorphism
 public import Mathlib.Combinatorics.SimpleGraph.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Bipartite
 public import Mathlib.Combinatorics.SimpleGraph.Cayley
@@ -3666,6 +3667,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Hasse
 public import Mathlib.Combinatorics.SimpleGraph.IncMatrix
 public import Mathlib.Combinatorics.SimpleGraph.InducedCopy
 public import Mathlib.Combinatorics.SimpleGraph.Init
+public import Mathlib.Combinatorics.SimpleGraph.Inversion
 public import Mathlib.Combinatorics.SimpleGraph.LapMatrix
 public import Mathlib.Combinatorics.SimpleGraph.LineGraph
 public import Mathlib.Combinatorics.SimpleGraph.Maps

Mathlib/Combinatorics/SimpleGraph/Inversion.lean

@@ -0,0 +1,364 @@
+/-
+Copyright (c) 2026 Christoph Spiegel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christoph Spiegel
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Finite
+public import Mathlib.Combinatorics.SimpleGraph.InducedCopy
+public import Mathlib.Data.Nat.Choose.Sum
+public import Mathlib.Data.Set.Card
+
+/-!
+# Möbius inversion between copy counts and induced copy counts
+
+For a guest graph `G : SimpleGraph V` and a host graph `H : SimpleGraph W` with finite
+vertex types, this file establishes the standard summation identity expressing the copy
+count `H.copyCount G` as a sum over supergraphs of `G` (on the same vertex type `V`) of
+induced copy counts `H.embeddingCount G'`, together with its Möbius inverse expressing
+`H.embeddingCount G` as a signed sum of `H.copyCount G'`.
+
+Following the convention from `Mathlib/Combinatorics/SimpleGraph/Copy.lean` and
+`Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean`, counting operations are host-first
+(`H.copyCount G`, `H.embeddingCount G`); types are guest-first (`Copy G H`, `Embedding G H`).
+
+## Main declarations
+
+* `SimpleGraph.Copy.inducedShape` — for `f : Copy G H`, the supergraph of `G` on `V`
+  recording the induced adjacency on the image, transported back via `f.toEmbedding`.
+* `SimpleGraph.Copy.fiberInducedShapeEquiv` — the per-fiber bijection between copies with a
+  prescribed induced shape and graph embeddings of that shape.
+* `SimpleGraph.Copy.equivSigmaEmbedding` — the load-bearing bijection
+  `Copy G H ≃ Σ G' ∈ Icc G ⊤, Embedding G'.val H`.
+* `SimpleGraph.iccEquivPowersetEdgeFinsetSdiff` — for `G ≤ K`, the equivalence
+  `Finset.Icc G K ≃ (K.edgeFinset \ G.edgeFinset).powerset` used to reduce the inner
+  alternating sum to `Finset.sum_powerset_neg_one_pow_card`.
+
+## Main results
+
+* `SimpleGraph.copyCount_eq_sum_embeddingCount` — forward identity:
+  `H.copyCount G = ∑ G' ∈ Icc G ⊤, H.embeddingCount G'`.
+* `SimpleGraph.embeddingCount_eq_sum_signed_copyCount` — Möbius inverse over `ℤ`:
+  `(H.embeddingCount G : ℤ) = (-1) ^ Nat.card G.edgeSet *
+    ∑ G' ∈ Icc G ⊤, (-1) ^ Nat.card G'.edgeSet * (H.copyCount G' : ℤ)`.
+
+## Implementation notes
+
+The forward bijection `Copy.equivSigmaEmbedding` is the only "real" content; the Möbius
+direction reduces to it via the classical alternating-sum identity
+`Finset.sum_powerset_neg_one_pow_card`, reindexed through the order-isomorphism
+`G' ∈ Icc G ⊤ ↔ S ⊆ E(⊤) \ E(G)`.
+
+The Möbius identity is stated in `ℤ` (rather than `ℕ`) because the signs are essential.
+The user-facing form uses `Nat.card G.edgeSet` rather than `#(G'.edgeFinset \ G.edgeFinset)`
+in the sign exponent: equivalent under `G ≤ G'` by parity, but `Nat.card` has no per-graph
+`Fintype` hypothesis, keeping the theorem signature free of `Classical`.
+
+The `LocallyFiniteOrder (SimpleGraph V)` instance consumed by `Finset.Icc G ⊤` comes from
+`SimpleGraph.Finite.instLocallyFiniteOrder`, which requires `[DecidableLE (SimpleGraph V)]`.
+-/
+
+public section
+
+open Finset Function
+
+namespace SimpleGraph
+
+variable {V W : Type*}
+
+/-! ### Induced shape of a copy
+
+The pullback `H.comap f.toEmbedding` records the induced adjacency on the image of a copy
+`f : Copy G H`, transported back to `V`. It is always a supergraph of `G`, and pinning it
+down to a specific supergraph `G'` promotes the copy to an embedding `G' ↪g H`. -/
+
+namespace Copy
+
+variable {G G' : SimpleGraph V} {H : SimpleGraph W}
+
+/-- The pullback of the host graph along the underlying injection of a copy. -/
+def inducedShape (f : Copy G H) : SimpleGraph V :=
+  H.comap f.toEmbedding
+
+@[simp] lemma inducedShape_adj (f : Copy G H) {a b : V} :
+    f.inducedShape.Adj a b ↔ H.Adj (f a) (f b) := Iff.rfl
+
+lemma le_inducedShape (f : Copy G H) : G ≤ f.inducedShape :=
+  fun _ _ => f.toHom.map_adj
+
+/-- A copy with induced shape `G'` promotes to a graph embedding `G' ↪g H`. -/
+@[expose] def toEmbeddingOfInducedShapeEq (f : Copy G H) (h : f.inducedShape = G') :
+    G' ↪g H where
+  toFun := f
+  inj' := f.injective
+  map_rel_iff' {a b} := by
+    change H.Adj (f a) (f b) ↔ G'.Adj a b
+    rw [← h, inducedShape_adj]
+
+@[simp] lemma toEmbeddingOfInducedShapeEq_apply (f : Copy G H) (h : f.inducedShape = G')
+    (v : V) : f.toEmbeddingOfInducedShapeEq h v = f v := rfl
+
+/-- The fiber of `inducedShape` over a supergraph `G' ≥ G` is canonically `Embedding G' H`. -/
+def fiberInducedShapeEquiv (hGG' : G ≤ G') :
+    {f : Copy G H // f.inducedShape = G'} ≃ Embedding G' H where
+  toFun f := f.val.toEmbeddingOfInducedShapeEq f.prop
+  invFun e := ⟨e.toCopy.comp (Copy.ofLE G G' hGG'), by ext a b; simp [inducedShape]⟩
+  left_inv f := by apply Subtype.ext; ext v; simp
+  right_inv e := by apply DFunLike.ext; intro v; simp
+
+end Copy
+
+@[simp] lemma Embedding.inducedShape_toCopy {G : SimpleGraph V} {H : SimpleGraph W}
+    (e : Embedding G H) : e.toCopy.inducedShape = G := by
+  ext a b; rw [Copy.inducedShape_adj]; exact e.map_rel_iff
+
+/-! ### Forward bijection and count identity -/
+
+section Forward
+
+variable {G : SimpleGraph V} {H : SimpleGraph W}
+
+/-- The load-bearing equivalence: a copy of `G` in `H` is the same data as a choice of
+supergraph `G' ∈ Icc G ⊤` (the induced shape) together with a graph embedding
+`G' ↪g H`. This expresses every copy uniquely as an induced copy of some shape `G'`
+between `G` and the complete graph.
+
+The proof goes via the canonical fiber decomposition `Equiv.sigmaFiberEquiv` for the map
+`Copy.inducedShape`. The index `K : SimpleGraph V` is restricted to `Icc G ⊤`, which is
+exactly the set of shapes with nonempty fiber. The per-fiber bijection is
+`Copy.fiberInducedShapeEquiv`. -/
+noncomputable def Copy.equivSigmaEmbedding (G : SimpleGraph V) (H : SimpleGraph W)
+    [Fintype V] [DecidableEq V] [DecidableLE (SimpleGraph V)] :
+    Copy G H ≃ Σ G' : ↥(Finset.Icc G ⊤), Embedding G'.val H :=
+  (Equiv.sigmaFiberEquiv (Copy.inducedShape : Copy G H → SimpleGraph V)).symm.trans <|
+  { toFun := fun ⟨K, f⟩ =>
+      let hGK : G ≤ K := f.prop ▸ f.val.le_inducedShape
+      ⟨⟨K, Finset.mem_Icc.mpr ⟨hGK, le_top⟩⟩,
+       Copy.fiberInducedShapeEquiv hGK f⟩
+    invFun := fun ⟨⟨K, hK⟩, e⟩ =>
+      ⟨K, (Copy.fiberInducedShapeEquiv (Finset.mem_Icc.mp hK).1).symm e⟩
+    left_inv := by
+      rintro ⟨K, f⟩
+      simp
+    right_inv := by
+      rintro ⟨⟨K, hK⟩, e⟩
+      simp only [Equiv.apply_symm_apply] }
+
+/-- Forward identity: every copy of `G` in `H` is an induced copy of some unique
+supergraph `G' ∈ Icc G ⊤` of `G`. -/
+theorem copyCount_eq_sum_embeddingCount [Fintype V] [DecidableEq V]
+    [DecidableLE (SimpleGraph V)] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    H.copyCount G = ∑ G' ∈ Finset.Icc G ⊤, H.embeddingCount G' := by
+  rw [copyCount_eq_nat_card, Nat.card_congr (Copy.equivSigmaEmbedding G H), Nat.card_sigma,
+    ← Finset.sum_attach (Finset.Icc G ⊤) (fun G' => H.embeddingCount G')]
+  refine Finset.sum_congr rfl fun G' _ => ?_
+  exact (embeddingCount_eq_nat_card _ _).symm
+
+end Forward
+
+/-! ### Möbius (signed-sum) inverse
+
+The Möbius inverse to the forward identity, expressing `H.embeddingCount G` as a signed
+sum of `H.copyCount G'` over supergraphs `G' ∈ Icc G ⊤`. The proof reduces, via the
+order-isomorphism `iccEquivPowersetEdgeFinsetSdiff` below, to the alternating-sum
+identity `Finset.sum_powerset_neg_one_pow_card`.
+-/
+
+section Mobius
+
+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). -/
+
+omit [Fintype V] [DecidableEq V] [DecidableLE (SimpleGraph V)] in
+/-- The set difference of edge sets on a finite vertex type is finite. -/
+lemma edgeSet_sdiff_finite [Finite V] (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
+
+omit [DecidableEq V] [DecidableLE (SimpleGraph V)] in
+@[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 _
+
+omit [DecidableEq V] [DecidableLE (SimpleGraph V)] in
+/-- 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
+  rw [Nat.card_coe_set_eq, Nat.card_coe_set_eq,
+      show #(edgeSetSdiffFinset G K) = (K.edgeSet \ G.edgeSet).ncard from
+        (Set.ncard_eq_toFinset_card _ (edgeSet_sdiff_finite G K)).symm,
+      add_comm]
+  exact (Set.ncard_sdiff_add_ncard_of_subset (edgeSet_subset_edgeSet.mpr hGK)).symm
+
+/-! ### 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' :=
+    ⟨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.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 hab, hab.ne⟩
+      · rw [fromEdgeSet_le]
+        rintro e ⟨heGS | heGS, _⟩
+        · exact edgeSet_subset_edgeSet.mpr hGK heGS
+        · exact (hSK e (Finset.mem_coe.mp heGS)).1⟩
+  left_inv := by
+    rintro ⟨G', hG'⟩
+    have hGG' : G ≤ G' := (Finset.mem_Icc.mp hG').1
+    apply Subtype.ext
+    ext a b
+    rw [fromEdgeSet_adj]
+    simp only [Set.mem_union, Finset.mem_coe, mem_edgeSetSdiffFinset]
+    refine ⟨fun ⟨h, _⟩ => h.elim (edgeSet_subset_edgeSet.mpr 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 : ∀ e ∈ S, e ∈ K.edgeSet ∧ e ∉ G.edgeSet := fun e he => by
+      have := Finset.mem_powerset.mp hS he
+      rwa [mem_edgeSetSdiffFinset] at this
+    apply Subtype.ext
+    apply Finset.ext
+    intro e
+    rw [mem_edgeSetSdiffFinset, edgeSet_fromEdgeSet, Set.mem_sdiff, Set.mem_union]
+    refine ⟨?_, fun heS => ?_⟩
+    · rintro ⟨⟨h | h, _⟩, heG⟩
+      · exact absurd h heG
+      · exact Finset.mem_coe.mp h
+    · have ⟨heK, heG⟩ := hSK e heS
+      exact ⟨⟨.inr (Finset.mem_coe.mpr heS), fun hd =>
+        K.not_isDiag_of_mem_edgeSet heK hd⟩, heG⟩
+
+/-! ### 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.
+Reindexes via `iccEquivPowersetEdgeFinsetSdiff`, factors out the `(-1)^Nat.card G.edgeSet`
+constant via the cardinality bridge, then collapses via `Finset.sum_powerset_neg_one_pow_card`
+(which is zero on a non-empty powerset). -/
+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
+  have hGL' : G ≤ L := hGL.le
+  -- Reindex the sum via `iccEquiv` and factor out `(-1)^Nat.card G.edgeSet`.
+  have key : ∑ K' ∈ Finset.Icc G L, (-1 : ℤ) ^ Nat.card K'.edgeSet
+      = (-1 : ℤ) ^ Nat.card G.edgeSet *
+          ∑ S ∈ (edgeSetSdiffFinset G L).powerset, (-1 : ℤ) ^ #S := by
+    rw [Finset.mul_sum,
+        ← Finset.sum_attach (Finset.Icc G L)
+          (fun K' => (-1 : ℤ) ^ Nat.card K'.edgeSet),
+        ← Finset.sum_attach (edgeSetSdiffFinset G L).powerset
+          (fun S => (-1 : ℤ) ^ Nat.card G.edgeSet * (-1 : ℤ) ^ #S)]
+    refine Finset.sum_equiv (iccEquivPowersetEdgeFinsetSdiff hGL')
+      (fun _ => by simp) ?_
+    intro K' _
+    have hGK' : G ≤ K'.val := (Finset.mem_Icc.mp K'.prop).1
+    rw [natCard_edgeSet_eq_add_card_sdiff hGK', pow_add]
+    rfl
+  rw [key, Finset.sum_powerset_neg_one_pow_card, if_neg, mul_zero]
+  -- Remaining goal: `edgeSetSdiffFinset G L ≠ ∅`, which would imply `L ≤ G`.
+  intro hempty
+  have hLsubG : L.edgeSet ⊆ G.edgeSet :=
+    Set.sdiff_eq_empty.mp ((edgeSet_sdiff_finite G L).toFinset_eq_empty.mp hempty)
+  exact absurd (le_antisymm (edgeSet_subset_edgeSet.mp hLsubG) hGL') hGL.ne'
+
+/-! ### 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`.
+
+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
+  symm
+  calc (-1 : ℤ) ^ Nat.card G.edgeSet *
+          ∑ G' ∈ Finset.Icc G ⊤,
+            (-1 : ℤ) ^ Nat.card G'.edgeSet * (H.copyCount G' : ℤ)
+      -- Substitute the forward identity into each `copyCount G'`.
+      = (-1 : ℤ) ^ Nat.card G.edgeSet *
+          ∑ G' ∈ Finset.Icc G ⊤, ∑ L ∈ Finset.Icc G' ⊤,
+            (-1 : ℤ) ^ Nat.card G'.edgeSet * (H.embeddingCount L : ℤ) := by
+        simp_rw [copyCount_eq_sum_embeddingCount, Nat.cast_sum, Finset.mul_sum]
+      -- Distribute `(-1)^Nat.card G.edgeSet` into the double sum.
+    _ = ∑ G' ∈ Finset.Icc G ⊤, ∑ L ∈ Finset.Icc G' ⊤,
+            (-1 : ℤ) ^ Nat.card G.edgeSet *
+              ((-1 : ℤ) ^ Nat.card G'.edgeSet * (H.embeddingCount L : ℤ)) := by
+        rw [Finset.mul_sum]
+        refine Finset.sum_congr rfl fun G' _ => ?_
+        rw [Finset.mul_sum]
+      -- Swap the order of summation over the triangle `G ≤ G' ≤ L ≤ ⊤`.
+    _ = ∑ L ∈ Finset.Icc G ⊤, ∑ G' ∈ Finset.Icc G L,
+            (-1 : ℤ) ^ Nat.card G.edgeSet *
+              ((-1 : ℤ) ^ Nat.card G'.edgeSet * (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 each inner sum.
+    _ = ∑ L ∈ Finset.Icc G ⊤, (H.embeddingCount L : ℤ) *
+          ((-1 : ℤ) ^ Nat.card G.edgeSet *
+            ∑ G' ∈ Finset.Icc G L, (-1 : ℤ) ^ Nat.card G'.edgeSet) := by
+        refine Finset.sum_congr rfl fun L _ => ?_
+        rw [Finset.mul_sum, Finset.mul_sum]
+        refine Finset.sum_congr rfl fun G' _ => ?_
+        ring
+      -- Isolate the `L = G` term: all others vanish via the strict-`G < L` kernel.
+    _ = (H.embeddingCount G : ℤ) := by
+        rw [Finset.sum_eq_single G]
+        · rw [sum_Icc_self_neg_one_pow_natCard_edgeSet, ← pow_add,
+              Even.neg_one_pow ⟨_, rfl⟩, mul_one]
+        · intro L hL hLG
+          rcases eq_or_lt_of_le (Finset.mem_Icc.mp hL).1 with rfl | hGL
+          · exact absurd rfl hLG
+          · rw [sum_Icc_neg_one_pow_natCard_edgeSet_of_lt hGL, mul_zero, mul_zero]
+        · intro hG
+          exact absurd (Finset.mem_Icc.mpr ⟨le_refl _, le_top⟩) hG
+
+end Mobius
+
+end SimpleGraph