feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems + golfing (leanprover-community#30640)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -357,108 +357,88 @@ lemma isTree_iff_minimal_connected : IsTree G ↔ Minimal Connected G := by
   simp only [edges_map, Hom.coe_ofLE, Sym2.map_id, List.map_id_fun, id_eq] at this
   simp [this, p.adj_of_mem_edges]
 
-set_option backward.isDefEq.respectTransparency false in
-/--
-Adding an edge to an acyclic graph preserves acyclicity if the endpoints are not reachable.
--/
+/-- Connecting two unreachable vertices by an edge preserves acyclicity. -/
+theorem IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable {u v : V} (hnreach : ¬G.Reachable u v)
+    (hacyc : G.IsAcyclic) : (G ⊔ fromEdgeSet {s(u, v)}).IsAcyclic := by
+  grind [isAcyclic_iff_forall_edge_isBridge, IsBridge.sup_fromEdgeSet_of_not_reachable,
+    edgeSet_sup, IsBridge.sup_fromEdgeSet_of_not_reachable_of_isBridge, edgeSet_fromEdgeSet]
+
 theorem isAcyclic_add_edge_iff_of_not_reachable (x y : V) (hxy : ¬ G.Reachable x y) :
-    (G ⊔ fromEdgeSet {s(x, y)}).IsAcyclic ↔ IsAcyclic G := by
-  refine ⟨fun h ↦ h.anti le_sup_left, fun hG ↦ ?_⟩
-  have x_ne_y : x ≠ y := fun c => (c ▸ hxy) (Reachable.refl y)
-  have h_add_remove : (G ⊔ fromEdgeSet {s(x, y)}) \ fromEdgeSet {s(x, y)} = G := by
-    simpa using fun h => hxy h.reachable
-  have h_bridge : (G ⊔ fromEdgeSet {s(x, y)}).IsBridge s(x, y) := by
-    simpa [isBridge_iff, x_ne_y, h_add_remove]
-  rw [isBridge_iff_adj_and_forall_cycle_notMem] at h_bridge
-  intro u c hc
-  let c' : G.Walk u u := Walk.transfer c G (fun e he ↦ by
-    have eneq : e ≠ s(x, y) := fun h => h_bridge.2 c hc (h ▸ he)
-    simpa [eneq] using Walk.edges_subset_edgeSet c he)
-  exact hG c' (Walk.IsCycle.transfer (qc := hc) ..)
+    (G ⊔ fromEdgeSet {s(x, y)}).IsAcyclic ↔ IsAcyclic G :=
+  ⟨.anti le_sup_left, .isAcyclic_sup_fromEdgeSet_of_not_reachable hxy⟩
+
+/-- Adding an edge results in an acyclic graph iff the original graph was acyclic and
+the edge connects vertices that previously had no path between them. -/
+theorem isAcyclic_sup_fromEdgeSet_iff {u v : V} :
+    (G ⊔ fromEdgeSet {s(u, v)}).IsAcyclic ↔
+      G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v) := by
+  by_cases huv : u = v
+  · grind [sup_eq_left, fromEdgeSet_le, Sym2.mem_diagSet, Sym2.mk_isDiag_iff]
+  by_cases hadj : G.Adj u v
+  · grind [sup_eq_left, fromEdgeSet_le, mem_edgeSet]
+  refine ⟨?_, fun ⟨hacyc, hreach⟩ ↦ hacyc.isAcyclic_sup_fromEdgeSet_of_not_reachable <| by grind⟩
+  refine fun hacyc ↦ ⟨hacyc.anti le_sup_left, fun hreach ↦ False.elim ?_⟩
+  have := isAcyclic_iff_forall_edge_isBridge.mp (e := s(u, v)) hacyc <| by simp [huv]
+  refine isBridge_iff.mp this |>.right <| hreach.mono <| Eq.le <| Eq.symm ?_
+  rw [sup_sdiff_right_self]
+  exact deleteEdges_eq_self.mpr <| Set.disjoint_singleton_right.mpr hadj
 
 /--
 The reachability relation of a maximal acyclic subgraph agrees with that of the larger graph.
 -/
 lemma reachable_eq_of_maximal_isAcyclic (F : SimpleGraph V)
-    (h : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) F) : F.Reachable = G.Reachable := by
-  obtain ⟨hF : F ≤ G, hF' : F.IsAcyclic⟩ := h.prop
-  replace h : ∀ {H : SimpleGraph V}, H ≤ G ∧ H.IsAcyclic → F ≤ H → H ≤ F := h.le_of_ge
+    (h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F) : F.Reachable = G.Reachable := by
   ext u v
-  refine ⟨fun h ↦ h.mono hF, ?_⟩
-  contrapose! h
-  obtain ⟨⟨p : G.Walk u v⟩, h : ¬ F.Reachable u v⟩ := h
-  let s : Set V := F.connectedComponentMk u
-  have hus : u ∈ s := ConnectedComponent.connectedComponentMk_mem
-  have hvs : v ∉ s := h ∘ (F.connectedComponentMk u).reachable_of_mem_supp hus
-  obtain ⟨⟨⟨u', v'⟩, huv : G.Adj u' v'⟩, -, hu : u' ∈ s, hv : v' ∉ s⟩ :=
-    p.exists_boundary_dart s hus hvs
-  suffices (F ⊔ fromEdgeSet {s(u', v')}).IsAcyclic by
-    refine ⟨F ⊔ fromEdgeSet {s(u', v')}, ⟨?_, this⟩, le_sup_left, ?_⟩
-    · have : G.Adj v' u' := G.symm huv
-      simp only [sup_le_iff, le_iff_adj, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq,
-        Sym2.rel_iff'] at hF ⊢
-      grind
-    · rw [le_iff_adj]
-      push_neg
-      refine ⟨u', v', ?_, fun hc ↦ ?_⟩
-      · simpa using Or.inr huv.ne
-      · have := (F.connectedComponentMk u).mem_supp_congr_adj hc
-        grind
-  suffices ¬ F.Reachable u' v' by rwa [isAcyclic_add_edge_iff_of_not_reachable u' v' this]
-  suffices F.connectedComponentMk u' = s by
-    rw [← ConnectedComponent.eq]
-    exact fun hc ↦ (hc ▸ this ▸ hv) ConnectedComponent.connectedComponentMk_mem
-  simp_rw [s, SetLike.coe, ConnectedComponent.supp_inj, ← ConnectedComponent.mem_supp_iff]
-  grind
+  refine ⟨.mono h.prop.left, fun ⟨p⟩ ↦ ?_⟩
+  by_contra
+  let s : F.ConnectedComponent := .mk _ u
+  have : v ∉ s := this ∘ s.reachable_of_mem_supp rfl
+  have : ∃ d ∈ p.darts, d.fst ∈ s ∧ d.snd ∉ s := p.exists_boundary_dart s rfl this
+  rcases this with ⟨⟨⟨u', v'⟩, huv⟩, _, hu, hv⟩
+  have : ¬F.Reachable v' u' := mt ConnectedComponent.sound <| s.mem_supp_iff u' |>.mp hu ▸ hv
+  suffices F ⊔ fromEdgeSet {s(v', u')} ≤ F by
+    grind [Adj.reachable, sup_le_iff, le_iff_adj, fromEdgeSet_adj]
+  refine h.le_of_ge ⟨?_, h.prop.right.isAcyclic_sup_fromEdgeSet_of_not_reachable this⟩ le_sup_left
+  grind [Maximal, sup_le, le_iff_adj, fromEdgeSet_adj, huv.symm]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- A subgraph is maximal acyclic iff its reachability relation agrees with the larger graph. -/
-theorem maximal_isAcyclic_iff_reachable_eq {F : SimpleGraph V} (hF : F ≤ G) (hF' : F.IsAcyclic) :
-    Maximal (fun H => H ≤ G ∧ H.IsAcyclic) F ↔ F.Reachable = G.Reachable := by
-  refine ⟨reachable_eq_of_maximal_isAcyclic F, fun h => ?_⟩
-  by_contra!
-  obtain ⟨F', hF'⟩ := exists_gt_of_not_maximal (P := fun H => H ≤ G ∧ H.IsAcyclic) ⟨hF, hF'⟩ this
-  obtain ⟨e, he⟩ := Set.exists_of_ssubset <| edgeSet_strict_mono hF'.1
-  have : (F ⊔ fromEdgeSet {e}).IsAcyclic := by
-    apply hF'.2.2.anti
-    refine sup_le_iff.mpr ⟨by grind, ?_⟩
-    rw [← F'.fromEdgeSet_edgeSet]
-    grind [fromEdgeSet_mono]
-  have F_sdiff_eq : (F ⊔ fromEdgeSet {e}) \ fromEdgeSet {e} = F := by
-    simpa using he.2
+theorem maximal_isAcyclic_iff_reachable_eq {F : SimpleGraph V} (hle : F ≤ G) (hF : F.IsAcyclic) :
+    Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F ↔ F.Reachable = G.Reachable := by
+  refine ⟨reachable_eq_of_maximal_isAcyclic F, fun h ↦ ?_⟩
+  by_contra
+  have ⟨H, hFH, hHG, hH⟩ := exists_gt_of_not_maximal ⟨hle, hF⟩ this
+  have ⟨e, heH, heF⟩ := Set.exists_of_ssubset <| edgeSet_strict_mono hFH
   have h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e := by
-    apply isAcyclic_iff_forall_edge_isBridge.mp this
-    simp [F'.not_isDiag_of_mem_edgeSet he.1]
-  simp only [IsBridge, F_sdiff_eq] at h_bridge
+    refine isAcyclic_iff_forall_edge_isBridge.mp ?_ <| by simp [H.not_isDiag_of_mem_edgeSet heH]
+    exact hH.anti <| sup_le_iff.mpr ⟨hFH.le, H.fromEdgeSet_le.mpr <| by grind⟩
+  have : (F ⊔ fromEdgeSet {e}) \ fromEdgeSet {e} = F := by simpa using heF
   cases e
-  case h u v =>
-    simp only [Sym2.lift_mk] at h_bridge
-    suffices G.Reachable u v by exact (h ▸ h_bridge.2) this
-    apply Reachable.mono hF'.2.1
-    apply Adj.reachable
-    simpa using he.1
+  rw [isBridge_iff, this, h] at h_bridge
+  exact h_bridge.right <| hHG heH |>.reachable
 
 /-- A subgraph of a connected graph is maximal acyclic iff it is a tree. -/
 theorem Connected.maximal_le_isAcyclic_iff_isTree {T : SimpleGraph V} (hG : G.Connected)
-    (hT : T ≤ G) : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree := by
-  have : Nonempty V := hG.nonempty
+    (hT : T ≤ G) : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree := by
+  have := hG.nonempty
   refine ⟨fun h ↦ ⟨⟨fun u v ↦ ?_⟩, h.1.2⟩, fun hT' ↦ ?_⟩
-  · rw [G.reachable_eq_of_maximal_isAcyclic T h]
-    exact hG.preconnected u v
-  · rw [maximal_isAcyclic_iff_reachable_eq hT hT'.IsAcyclic]
-    replace hT' : T.Reachable = ⊤ := by
-      rw [← preconnected_iff_reachable_eq_top]
-      exact hT'.isConnected.preconnected
-    replace hG : G.Reachable = ⊤ := by
-      rw [← preconnected_iff_reachable_eq_top]
-      exact hG.preconnected
-    rw [hT', hG]
+  · exact G.reachable_eq_of_maximal_isAcyclic T h ▸ hG.preconnected u v
+  · rw [maximal_isAcyclic_iff_reachable_eq hT hT'.IsAcyclic,
+      T.preconnected_iff_reachable_eq_top.mp hT'.isConnected.preconnected,
+      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]
 
 @[simp]
 theorem maximal_isAcyclic_iff_isTree [Nonempty V] {T : SimpleGraph V} :
     Maximal IsAcyclic T ↔ T.IsTree := by
   simp [← connected_top.maximal_le_isAcyclic_iff_isTree le_top]
 
+/-- A maximally acyclic graph is a tree. This is similar to `maximal_isAcyclic_iff_isTree` except
+with `Nonempty V` as part of the iff rather than an assumption. -/
+theorem isTree_iff_maximal_isAcyclic : G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G := by
+  refine ⟨fun h ↦ ?_, fun ⟨_, h⟩ ↦ G.maximal_isAcyclic_iff_isTree.mp h⟩
+  have := h.isConnected.nonempty
+  exact ⟨this, G.maximal_isAcyclic_iff_isTree.mpr h⟩
+
 /-- Every acyclic subgraph can be extended to a spanning forest. -/
 theorem exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic {H : SimpleGraph V} (hH_le : H ≤ G)
     (hH_isAcyclic : H.IsAcyclic) :

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -844,6 +844,22 @@ theorem IsBridge.anti_of_mem_edgeSet {G' : SimpleGraph V} {e : Sym2 V} (hle : G
     isBridge_iff_mem_and_forall_cycle_notMem.mp h' |>.right
       (p.mapLe hle) (Walk.IsCycle.mapLe hle hp) (p.edges_mapLe_eq_edges hle ▸ hpe)⟩
 
+/-- Connecting two unreachable vertices by an edge creates a bridge. -/
+theorem IsBridge.sup_fromEdgeSet_of_not_reachable {u v : V} (h : ¬G.Reachable u v) :
+    (G ⊔ fromEdgeSet {s(u, v)}).IsBridge s(u, v) := by
+  refine isBridge_iff.mpr ⟨.inr ⟨Set.mem_singleton _, mt (· ▸ .rfl) h⟩, ?_⟩
+  exact fun h' ↦ h <| .mono (sdiff_le_iff'.mpr <| refl _) h'
+
+/-- Connecting two unreachable vertices by an edge preserves existing bridges. -/
+theorem IsBridge.sup_fromEdgeSet_of_not_reachable_of_isBridge {u v : V} {e : Sym2 V}
+    (h : ¬G.Reachable u v) (h' : G.IsBridge e) : (G ⊔ fromEdgeSet {s(u, v)}).IsBridge e := by
+  refine isBridge_iff_mem_and_forall_cycle_notMem.mpr ⟨edgeSet_mono le_sup_left h'.left, ?_⟩
+  refine fun _ p hp hpe ↦ isBridge_iff_mem_and_forall_cycle_notMem.mp h' |>.right
+    (p.transfer G fun e' he' ↦ ?_) (hp.transfer _) (Walk.edges_transfer p _ ▸ hpe)
+  refine edgeSet_sup .. ▸ Walk.edges_subset_edgeSet _ he' |>.elim id fun h' ↦ h ?_ |>.elim
+  exact .mono (sdiff_le_iff'.mpr <| refl _) <|
+    adj_and_reachable_delete_edges_iff_exists_cycle.mpr (by grind [edgeSet_fromEdgeSet]) |>.right
+
 end BridgeEdges
 
 /-!