fix(Combinatorics/SimpleGraph/Connectivity/Connected): deprecate IsBridge.of_not_reachable

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -369,8 +369,7 @@ lemma isTree_iff_minimal_connected : IsTree G ↔ Minimal Connected G := by
 theorem IsAcyclic.sup_edge_of_not_reachable {u v : V} (hnreach : ¬G.Reachable u v)
     (hacyc : G.IsAcyclic) : (G ⊔ edge u v).IsAcyclic := by
   grind [isAcyclic_iff_forall_edge_isBridge, IsBridge.sup_edge_of_not_reachable,
-    IsBridge.sup_edge_of_not_reachable_of_isBridge,
-    edgeSet_sup, edgeSet_edge, IsBridge.of_not_reachable]
+    IsBridge.sup_edge_of_not_reachable_of_isBridge, edgeSet_sup, edgeSet_edge]
 
 @[deprecated (since := "2026-03-18")]
 alias IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable := IsAcyclic.sup_edge_of_not_reachable

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -752,8 +752,9 @@ def IsBridge (G : SimpleGraph V) (e : Sym2 V) : Prop :=
 theorem isBridge_iff {u v : V} :
     G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G.deleteEdges {s(u, v)}).Reachable u v := Iff.rfl
 
-@[simp] lemma IsBridge.of_not_reachable (huv : ¬ G.Reachable u v) (h : G.Adj u v) :
-    G.IsBridge s(u, v) := ⟨h, fun h ↦ huv <| h.mono <| deleteEdges_le _⟩
+@[deprecated "Use `absurd h.reachable huv` instead." (since := "2026-04-02")]
+lemma IsBridge.of_not_reachable (huv : ¬ G.Reachable u v) (h : G.Adj u v) :
+    G.IsBridge s(u, v) := absurd h.reachable huv
 
 lemma IsBridge.nontrivial {e : Sym2 V} (he : G.IsBridge e) : Nontrivial V := by
   cases e with | h u v; exact ⟨u, v, by rintro rfl; simp [IsBridge] at he⟩