feat(Combinatorics/SimpleGraphs): various path and edge lemmas (#22034)

Adds a number of miscellaneous lemmas, mostly on paths and edges, in preparation for Tutte's theorem.



Co-authored-by: Pim Otte <otte.pim@gmail.com>

Author: pimotte

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

@@ -145,6 +145,10 @@ theorem mem_verts_toSubgraph (p : G.Walk u v) : w ∈ p.toSubgraph.verts ↔ w 
       ⟨by rintro (rfl | h) <;> simp [*], by simp (config := { contextual := true })⟩
     simp [ih, or_assoc, this]
 
+lemma not_nil_of_adj_toSubgraph {u v} {x : V} {p : G.Walk u v} (hadj : p.toSubgraph.Adj w x) :
+    ¬p.Nil := by
+  cases p <;> simp_all
+
 lemma start_mem_verts_toSubgraph (p : G.Walk u v) : u ∈ p.toSubgraph.verts := by
   simp [mem_verts_toSubgraph]
 
@@ -185,6 +189,13 @@ theorem toSubgraph_rotate [DecidableEq V] (c : G.Walk v v) (h : u ∈ c.support)
 theorem toSubgraph_map (f : G →g G') (p : G.Walk u v) :
     (p.map f).toSubgraph = p.toSubgraph.map f := by induction p <;> simp [*, Subgraph.map_sup]
 
+lemma adj_toSubgraph_mapLe {G' : SimpleGraph V} {w x : V} {p : G.Walk u v} (h : G ≤ G') :
+    (p.mapLe h).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x := by
+  simp only [toSubgraph_map, Subgraph.map_adj]
+  nth_rewrite 1 [← Hom.mapSpanningSubgraphs_apply h w, ← Hom.mapSpanningSubgraphs_apply h x]
+  rw [Relation.map_apply_apply (Hom.mapSpanningSubgraphs_injective h)
+    (Hom.mapSpanningSubgraphs_injective h)]
+
 @[simp]
 theorem finite_neighborSet_toSubgraph (p : G.Walk u v) : (p.toSubgraph.neighborSet w).Finite := by
   induction p with
@@ -370,6 +381,17 @@ lemma ncard_neighborSet_toSubgraph_eq_two {u v} {p : G.Walk u u} (hpc : p.IsCycl
   rw [← hi.1, hpc.neighborSet_toSubgraph_internal he.1 (by omega)]
   exact Set.ncard_pair (hpc.getVert_sub_one_neq_getVert_add_one (by omega))
 
+lemma exists_isCycle_snd_verts_eq {p : G.Walk v v} (h : p.IsCycle) (hadj : p.toSubgraph.Adj v w) :
+    ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts := by
+  have : w ∈ p.toSubgraph.neighborSet v := hadj
+  rw [h.neighborSet_toSubgraph_endpoint] at this
+  simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at this
+  obtain hl | hr := this
+  · exact ⟨p, ⟨h, hl.symm, rfl⟩⟩
+  · use p.reverse
+    rw [penultimate, ← getVert_reverse] at hr
+    exact ⟨h.reverse, hr.symm, by rw [toSubgraph_reverse _]⟩
+
 end IsCycle
 
 end Walk

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -272,6 +272,13 @@ def mapSpanningSubgraphs {G G' : SimpleGraph V} (h : G ≤ G') : G →g G' where
   toFun x := x
   map_rel' ha := h ha
 
+lemma mapSpanningSubgraphs_inj {G G' : SimpleGraph V} {v w : V} (h : G ≤ G') :
+    mapSpanningSubgraphs h v = mapSpanningSubgraphs h w ↔ v = w := by simp
+
+lemma mapSpanningSubgraphs_injective {G G' : SimpleGraph V} (h : G ≤ G') :
+    Injective (mapSpanningSubgraphs h) :=
+  fun v w hvw ↦ by simpa [mapSpanningSubgraphs_apply] using hvw
+
 theorem mapEdgeSet.injective (hinj : Function.Injective f) : Function.Injective f.mapEdgeSet := by
   rintro ⟨e₁, h₁⟩ ⟨e₂, h₂⟩
   dsimp [Hom.mapEdgeSet]

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -6,6 +6,7 @@ Authors: Alena Gusakov, Arthur Paulino, Kyle Miller, Pim Otte
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
 import Mathlib.Combinatorics.SimpleGraph.DegreeSum
+import Mathlib.Combinatorics.SimpleGraph.Operations
 import Mathlib.Data.Fintype.Order
 import Mathlib.Data.Set.Functor
 
@@ -89,6 +90,16 @@ lemma IsMatching.map_ofLE (h : M.IsMatching) (hGG' : G ≤ G') :
   use w
   simpa using hv' ▸ hw
 
+lemma IsMatching.not_adj_left_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huv : v ≠ w)
+    (hadj : M.Adj u v) : ¬M.Adj u w := by
+  intro hadj'
+  obtain ⟨x, hx⟩ := hM (M.edge_vert hadj)
+  exact huv (hx.2 _ hadj ▸ (hx.2 _ hadj').symm)
+
+lemma IsMatching.not_adj_right_of_ne {M : Subgraph G} {u v w : V} (hM : M.IsMatching) (huw : u ≠ w)
+    (hadj : M.Adj u v) : ¬M.Adj w v  :=
+  fun hadj' ↦ hM.not_adj_left_of_ne huw hadj.symm hadj'.symm
+
 lemma IsMatching.sup (hM : M.IsMatching) (hM' : M'.IsMatching)
     (hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching := by
   intro v hv
@@ -354,6 +365,35 @@ lemma IsCycles.induce_supp (c : G.ConnectedComponent) (h : G.IsCycles) :
   ext w'
   simp only [mem_neighborSet, c.adj_spanningCoe_induce_supp, hw, true_and]
 
+lemma Walk.IsCycle.isCycles_spanningCoe_toSubgraph {u : V} {p : G.Walk u u} (hpc : p.IsCycle) :
+    p.toSubgraph.spanningCoe.IsCycles := by
+  intro v hv
+  apply hpc.ncard_neighborSet_toSubgraph_eq_two
+  obtain ⟨_, hw⟩ := hv
+  exact p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw
+
+lemma Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {u v} {p : G.Walk u v} (hp : p.IsPath)
+    (h : u ≠ v) (hs : s(v, u) ∉ p.edges) : (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles := by
+  let c := (p.mapLe (OrderTop.le_top G)).cons (by simp [h.symm] : (completeGraph V).Adj v u)
+  have : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe := by
+    ext w x
+    simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
+      Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]
+    aesop
+  exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs])
+
+lemma Walk.IsCycle.adj_toSubgraph_iff_of_isCycles [LocallyFinite G] {u} {p : G.Walk u u}
+    (hp : p.IsCycle) (hcyc : G.IsCycles) (hv : v ∈ p.toSubgraph.verts) :
+    ∀ w, p.toSubgraph.Adj v w ↔ G.Adj v w := by
+  refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Inhabited _).default (Set.toFinite _)
+  apply Classical.inhabited_of_nonempty
+  rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
+      ← Set.cast_ncard (finite_neighborSet_toSubgraph p), hcyc
+        (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
+          Set.nonempty_of_ncard_ne_zero <| by simp [Set.Nonempty.mono,
+          hp.ncard_neighborSet_toSubgraph_eq_two (by aesop), Set.nonempty_of_ncard_ne_zero]),
+      hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)]
+
 open scoped symmDiff
 
 lemma Subgraph.IsPerfectMatching.symmDiff_isCycles
@@ -490,6 +530,35 @@ def IsAlternating (G G' : SimpleGraph V) :=
 lemma IsAlternating.mono {G'' : SimpleGraph V} (halt : G.IsAlternating G') (h : G'' ≤ G) :
     G''.IsAlternating G' := fun _ _ _ hww' hvw hvw' ↦ halt hww' (h hvw) (h hvw')
 
+lemma IsAlternating.spanningCoe (halt : G.IsAlternating G') (H : Subgraph G)  :
+    H.spanningCoe.IsAlternating G' := by
+  intro v w w' hww' hvw hvv'
+  simp only [Subgraph.spanningCoe_adj] at hvw hvv'
+  exact halt hww' hvw.adj_sub hvv'.adj_sub
+
+lemma IsAlternating.sup_edge {u x : V} (halt : G.IsAlternating G') (hnadj : ¬G'.Adj u x)
+    (hu' : ∀ u', u' ≠ u → G.Adj x u' → G'.Adj x u')
+    (hx' : ∀ x', x' ≠ x → G.Adj x' u → G'.Adj x' u) : (G ⊔ edge u x).IsAlternating G' := by
+  by_cases hadj : G.Adj u x
+  · rwa [sup_edge_of_adj G hadj]
+  intro v w w' hww' hvw hvv'
+  simp only [sup_adj, edge_adj] at hvw hvv'
+  obtain hl | hr := hvw <;> obtain h1 | h2 := hvv'
+  · exact halt hww' hl h1
+  · rw [G'.adj_congr_of_sym2 (by aesop : s(v, w') = s(u, x))]
+    simp only [hnadj, not_false_eq_true, iff_true]
+    rcases h2.1 with ⟨h2l1, h2l2⟩ | ⟨h2r1,h2r2⟩
+    · subst h2l1 h2l2
+      exact (hx' _ hww' hl.symm).symm
+    · aesop
+  · rw [G'.adj_congr_of_sym2 (by aesop : s(v, w) = s(u, x))]
+    simp only [hnadj, false_iff, not_not]
+    rcases hr.1 with ⟨hrl1, hrl2⟩ | ⟨hrr1, hrr2⟩
+    · subst hrl1 hrl2
+      exact (hx' _ hww'.symm h1.symm).symm
+    · aesop
+  · aesop
+
 lemma IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatching)
     (hG' : G'.IsAlternating M.spanningCoe) (hG'cyc : G'.IsCycles) :
     (⊤ : Subgraph (M.spanningCoe ∆ G')).IsPerfectMatching := by

Mathlib/Combinatorics/SimpleGraph/Operations.lean

@@ -148,6 +148,11 @@ def edge : SimpleGraph V := fromEdgeSet {s(s, t)}
 lemma edge_adj (v w : V) : (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w := by
   rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]
 
+lemma adj_edge {v w : V} : (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w := by
+  simp only [edge_adj, ne_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk,
+    and_congr_left_iff]
+  tauto
+
 lemma edge_comm : edge s t = edge t s := by
   rw [edge, edge, Sym2.eq_swap]
 
@@ -175,6 +180,15 @@ lemma sup_edge_of_adj (h : G.Adj s t) : G ⊔ edge s t = G := by
   rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edge_edgeSet_of_ne h.ne, Set.singleton_subset_iff,
     mem_edgeSet]
 
+lemma disjoint_edge {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v := by
+  by_cases h : u = v
+  · subst h
+    simp [edge_self_eq_bot]
+  simp [← disjoint_edgeSet, edge_edgeSet_of_ne h]
+
+lemma sdiff_edge {u v : V} (h : ¬G.Adj u v) : G \ edge u v = G := by
+  simp [disjoint_edge, h]
+
 theorem Subgraph.spanningCoe_sup_edge_le {H : Subgraph (G ⊔ edge s t)} (h : ¬ H.Adj s t) :
     H.spanningCoe ≤ G := by
   intro v w hvw

Mathlib/Combinatorics/SimpleGraph/Path.lean

@@ -304,6 +304,44 @@ lemma IsPath.getVert_injOn {p : G.Walk u v} (hp : p.IsPath) :
         (by omega : (m - 1) ≤ p.length) hnm
       omega
 
+lemma IsPath.getVert_eq_start_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
+    p.getVert i = u ↔ i = 0 := by
+  refine ⟨?_, by aesop⟩
+  intro h
+  by_cases hi : i = 0
+  · exact hi
+  · apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
+    simp [h]
+
+lemma IsPath.getVert_eq_end_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
+    p.getVert i = w ↔ i = p.length := by
+  have := hp.reverse.getVert_eq_start_iff (by omega : p.reverse.length - i ≤ p.reverse.length)
+  simp only [length_reverse, getVert_reverse,
+    show p.length - (p.length - i) = i from by omega] at this
+  rw [this]
+  omega
+
+lemma IsPath.getVert_injOn_iff (p : G.Walk u v) : Set.InjOn p.getVert {i | i ≤ p.length} ↔
+    p.IsPath := by
+  refine ⟨?_, fun a => a.getVert_injOn⟩
+  induction p with
+  | nil => simp
+  | cons h q ih =>
+    intro hinj
+    rw [cons_isPath_iff]
+    refine ⟨ih (by
+      intro n hn m hm hnm
+      simp only [Set.mem_setOf_eq] at hn hm
+      have := hinj (by rw [length_cons]; omega : n + 1 ≤ (q.cons h).length)
+          (by rw [length_cons]; omega : m + 1 ≤ (q.cons h).length)
+          (by simpa [getVert_cons] using hnm)
+      omega), fun h' => ?_⟩
+    obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
+    have := hinj (by rw [length_cons]; omega : (n + 1) ≤ (q.cons h).length)
+      (by omega : 0 ≤ (q.cons h).length) (show (q.cons h).getVert (n + 1) = (q.cons h).getVert 0
+        from by rwa [getVert_cons _ _ (by omega : n + 1 ≠ 0), getVert_zero])
+    omega
+
 /-! ### About cycles -/
 
 -- TODO: These results could possibly be less laborious with a periodic function getCycleVert