awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
mp : s(v, w) ∉ (↑p.toPath : G.Walk v w).edges
⊢ s(w, v) ∉ (↑p.toPath : G.Walk v w).edges

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h_1 : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
h : s(v, w) ∈ (↑p.toPath : G.Walk v w).edges
⊢ False

Tactic:
cases hp (Walk.edges_toPath_subset p h)

Premises used: SimpleGraph.Walk.edges_toPath_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ (↑p.toPath : G.Walk v w)).edges

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges

Tactic:
⟨c.adj_of_mem_edges he, ?_⟩

Premises used: And.intro, SimpleGraph.Walk.adj_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
mpr : ∃ (p : G.Walk v w), s(v, w) ∉ p.edges
⊢ G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges

Tactic:
refine ⟨c.adj_of_mem_edges he, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
mpr : ∀ (hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges), False
⊢ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges

Tactic:
by_contra! hb
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
p : G.Walk w v
⊢ s(w, v) ∈ p.edges

Tactic:
simpa [Sym2.eq_swap] using hb p.reverse

Premises used: Sym2.eq_swap, SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ ∀ (p : G.Walk w v), s(w, v) ∈ p.edges

Tactic:
have hb' : ∀ p : G.Walk w v, s(w, v) ∈ p.edges := by
      intro p
      simpa [Sym2.eq_swap] using hb p.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
⊢ v ∈ c.support

Tactic:
have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ False

Tactic:
reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate v hvc) (hc.isTrail.rotate hvc)
      ?_ (Walk.start_mem_support _)

Premises used: SimpleGraph.Walk.start_mem_support, SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux, SimpleGraph.Walk.rotate, SimpleGraph.Walk.IsCircuit.isTrail, SimpleGraph.Walk.IsTrail.rotate, SimpleGraph.Walk.IsCycle.isCircuit
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
mpr : s(w, v) ∈ (c.rotate v hvc).edges
⊢ False

Tactic:
refine reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate v hvc) (hc.isTrail.rotate hvc)
      ?_ (Walk.start_mem_support _)

Premises used: SimpleGraph.Walk.start_mem_support, SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux, SimpleGraph.Walk.rotate, SimpleGraph.Walk.IsCircuit.isTrail, SimpleGraph.Walk.IsTrail.rotate, SimpleGraph.Walk.IsCycle.isCircuit
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
mpr : s(w, v) ∈ c.edges
mpr₁ mpr₂ mpr₃ mpr₄ : s(v, w) ∈ c.edges
⊢ s(w, v) ∈ (c.rotate v hvc).edges

Tactic:
rwa [(c.rotate_edges v hvc).mem_iff, Sym2.eq_swap]

Premises used: List.IsRotated.mem_iff, SimpleGraph.Walk.rotate_edges, Sym2.eq_swap
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
rw rw₁ rw₂ :
  (G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges) ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
mp : (G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges) → ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
mpr mpr₁ :
  (∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges
⊢ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
classical
  rw [reachable_deleteEdges_iff_exists_walk]
  constructor
  · rintro ⟨h, p, hp⟩
    refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩
    · apply Path.cons_isCycle
      rw [Sym2.eq_swap]
      intro h
      cases hp (Walk.edges_toPath_subset p h)
    · simp
  · rintro ⟨u, c, hc, he⟩
    refine ⟨c.adj_of_mem_edges he, ?_⟩
    by_contra! hb
    have hb' : ∀ p : G.Walk w v, s(w, v) ∈ p.edges := by
      intro p
      simpa [Sym2.eq_swap] using hb p.reverse
    have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he
    refine reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate v hvc) (hc.isTrail.rotate hvc)
      ?_ (Walk.start_mem_support _)
    rwa [(c.rotate_edges v hvc).mem_iff, Sym2.eq_swap]

Premises used: SimpleGraph.reachable_deleteEdges_iff_exists_walk, Sym2.eq_swap, SimpleGraph.Path.cons_isCycle
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
rw : G.Adj v w → (¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges)
⊢ G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
rw [isBridge_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, SimpleGraph.isBridge_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
contrapose! : (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
⊢ ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
rw : (G.deleteEdges {s(v, w)}).Reachable v w ↔ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w
⊢ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
rw [← adj_and_reachable_delete_edges_iff_exists_cycle]

Premises used: SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G.deleteEdges {s(v, w)}).Reachable v w ↔ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w

Tactic:
simp only [h, true_and]

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
⊢ G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges

Tactic:
Sym2.ind (fun _ _ => isBridge_iff_adj_and_forall_cycle_notMem) e

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : ¬G.IsBridge s(x, y)
⊢ G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y

Tactic:
simp only [isBridge_iff, not_and, not_not] at h

Premises used: Classical.not_not, SimpleGraph.isBridge_iff, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
inl : ∀ (hxy : ¬G.Adj x y), (G.deleteEdges {s(x, y)}).Connected
inr : ∀ (hxy : G.Adj x y), (G.deleteEdges {s(x, y)}).Connected
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
obtain hxy | hxy := em' <| G.Adj x y

Premises used: SimpleGraph.Adj, em'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ Disjoint G (fromEdgeSet {s(x, y)})

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
inl : (G \ fromEdgeSet {s(x, y)}).Connected
inl₁ inl₂ inl₃ inl₄ : G.Connected
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
rwa [deleteEdges, Disjoint.sdiff_eq_left (by simpa)]

Premises used: SimpleGraph.deleteEdges, Disjoint.sdiff_eq_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
(connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
inr : ∀ (w : V), (G.deleteEdges {s(x, y)}).Reachable x w
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
inr : ∀ (P : G.Walk w x) (hP : P.IsPath), (G.deleteEdges {s(x, y)}).Reachable x w
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
obtain ⟨P, hP⟩ := hG.exists_isPath w x

Premises used: SimpleGraph.Connected.exists_isPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
inr : ∀ (heP : s(x, y) ∉ P.edges), (G.deleteEdges {s(x, y)}).Reachable x w
inr₁ : ∀ (heP : s(x, y) ∈ P.edges), (G.deleteEdges {s(x, y)}).Reachable x w
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
obtain heP | heP := em' <| s(x, y) ∈ P.edges

Premises used: em', SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ ∀ e ∈ P.edges, e ∉ {s(x, y)}

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
exact ⟨(P.toDeleteEdges {s(x, y)} (by grind)).reverse⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
⊢ y ∈ P.support

Tactic:
have hyP := P.snd_mem_support_of_mem_edges heP
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
⊢ x ∉ (P.takeUntil y hyP).support

Tactic:
have hxP₁ := Walk.endpoint_notMem_support_takeUntil hP hyP hxy.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
⊢ s(x, y) ∉ P₁.edges

Tactic:
have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
heP₁ : s(x, y) ∉ P₁.edges
⊢ ∀ e ∈ P₁.edges, e ∉ {s(x, y)}

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
heP₁ : s(x, y) ∉ P₁.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by grind)⟩)

Premises used: SimpleGraph.Reachable.symm, Sym2.mk, SimpleGraph.Reachable.trans, Nonempty.intro, SimpleGraph.Walk.toDeleteEdges, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : ¬G.IsBridge s(x, y)
simp : ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y), (G.deleteEdges {s(x, y)}).Connected
inl :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : ¬G.Adj x y), (G.deleteEdges {s(x, y)}).Connected
inr inr₁ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y), (G.deleteEdges {s(x, y)}).Connected
inr₂ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V),
    (G.deleteEdges {s(x, y)}).Reachable x w
inr₃ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V) (P : G.Walk w x)
    (hP : P.IsPath), (G.deleteEdges {s(x, y)}).Reachable x w
inr₄ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V) (P : G.Walk w x) (hP : P.IsPath)
    (heP : s(x, y) ∉ P.edges), (G.deleteEdges {s(x, y)}).Reachable x w
inr₅ inr₆ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V) (P : G.Walk w x) (hP : P.IsPath)
    (heP : s(x, y) ∈ P.edges), (G.deleteEdges {s(x, y)}).Reachable x w
inr₇ inr₈ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V) (P : G.Walk w x) (hP : P.IsPath)
    (heP : s(x, y) ∈ P.edges) (hyP : y ∈ P.support), (G.deleteEdges {s(x, y)}).Reachable x w
inr₉ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V) (P : G.Walk w x) (hP : P.IsPath)
    (heP : s(x, y) ∈ P.edges) (hyP : y ∈ P.support) (hxP₁ : x ∉ (P.takeUntil y hyP).support),
    (G.deleteEdges {s(x, y)}).Reachable x w
inr₁₀ :
  ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y) (hxy : G.Adj x y) (w : V) (P : G.Walk w x) (hP : P.IsPath)
    (heP : s(x, y) ∈ P.edges) (hyP : y ∈ P.support),
    let P₁ := P.takeUntil y hyP;
    ∀ (hxP₁ : x ∉ (P.takeUntil y hyP).support) (heP₁ : s(x, y) ∉ P₁.edges), (G.deleteEdges {s(x, y)}).Reachable x w
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
classical
  simp only [isBridge_iff, not_and, not_not] at h
  obtain hxy | hxy := em' <| G.Adj x y
  · rwa [deleteEdges, Disjoint.sdiff_eq_left (by simpa)]
  refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩
  obtain ⟨P, hP⟩ := hG.exists_isPath w x
  obtain heP | heP := em' <| s(x, y) ∈ P.edges
  · exact ⟨(P.toDeleteEdges {s(x, y)} (by grind)).reverse⟩
  have hyP := P.snd_mem_support_of_mem_edges heP
  let P₁ := P.takeUntil y hyP
  have hxP₁ := Walk.endpoint_notMem_support_takeUntil hP hyP hxy.ne
  have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h
  exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by grind)⟩)

Premises used: SimpleGraph.deleteEdges, Iff.mpr, Classical.not_not, SimpleGraph.Adj, SimpleGraph.isBridge_iff, Disjoint.sdiff_eq_left, Exists.intro, not_and, em', SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
e : Sym2 V
hle : G ≤ G'
h : e ∈ G.edgeSet
h' : G'.IsBridge e
⊢ G.IsBridge e

Tactic:
isBridge_iff_mem_and_forall_cycle_notMem.mpr ⟨h, fun _ p hp hpe ↦
    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)⟩

Premises used: Iff.mpr, SimpleGraph.Walk.edges_mapLe_eq_edges, Eq.rec, SimpleGraph.Walk.IsCycle.mapLe, And.right, SimpleGraph.Walk.mapLe, And.intro, Iff.mp, Eq.symm, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ (G ⊔ edge u v).IsBridge s(u, v)

Tactic:
isBridge_iff.mpr ⟨.inr ⟨Set.mem_singleton _, mt (· ▸ .rfl) h⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_singleton, mt, SimpleGraph.isBridge_iff, And.intro, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
refine : ¬((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable u v
⊢ (G ⊔ edge u v).IsBridge s(u, v)

Tactic:
refine isBridge_iff.mpr ⟨.inr ⟨Set.mem_singleton _, mt (· ▸ .rfl) h⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ ¬((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable u v

Tactic:
fun h' ↦ h <| .mono (sdiff_le_iff'.mpr <| refl _) h'

Premises used: Iff.mpr, sdiff_le_iff', SimpleGraph.edge, Max.max, SimpleGraph.Reachable.mono, refl, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ ¬((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable u v

Tactic:
exact fun h' ↦ h <| .mono (sdiff_le_iff'.mpr <| refl _) h'

Premises used: Iff.mpr, sdiff_le_iff', Max.max, SimpleGraph.Reachable.mono, refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h' : G.IsBridge e
⊢ (G ⊔ edge u v).IsBridge e

Tactic:
isBridge_iff_mem_and_forall_cycle_notMem.mpr ⟨edgeSet_mono le_sup_left h'.left, ?_⟩

Premises used: Iff.mpr, le_sup_left, And.left, SimpleGraph.edgeSet_mono, And.intro, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h' : G.IsBridge e
refine : ∀ ⦃u_1 : V⦄ (p : (G ⊔ edge u v).Walk u_1 u_1), p.IsCycle → e ∉ p.edges
⊢ (G ⊔ edge u v).IsBridge e

Tactic:
refine isBridge_iff_mem_and_forall_cycle_notMem.mpr ⟨edgeSet_mono le_sup_left h'.left, ?_⟩

Premises used: Iff.mpr, le_sup_left, And.left, SimpleGraph.edgeSet_mono, And.intro, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h' : G.IsBridge e
⊢ ∀ ⦃u_1 : V⦄ (p : (G ⊔ edge u v).Walk u_1 u_1), p.IsCycle → e ∉ p.edges

Tactic:
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)

Premises used: SimpleGraph.Walk.IsCycle.transfer, And.right, Iff.mp, SimpleGraph.Walk.transfer, Not, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h' : G.IsBridge e
refine :
  ∀ (x : V) (p : (G ⊔ edge u v).Walk x x) (hp : p.IsCycle) (hpe : e ∈ p.edges) (e' : Sym2 V) (he' : e' ∈ p.edges),
    e' ∈ G.edgeSet
⊢ ∀ ⦃u_1 : V⦄ (p : (G ⊔ edge u v).Walk u_1 u_1), p.IsCycle → e ∉ p.edges

Tactic:
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)

Premises used: And.right, Iff.mp, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h' : G.IsBridge e
x : V
p : (G ⊔ edge u v).Walk x x
hp : p.IsCycle
hpe : e ∈ p.edges
e' : Sym2 V
he' : e' ∈ p.edges
refine : ∀ (h' : e' ∈ (edge u v).edgeSet), G.Reachable u v
⊢ e' ∈ G.edgeSet

Tactic:
refine edgeSet_sup .. ▸ Walk.edges_subset_edgeSet _ he' |>.elim id fun h' ↦ h ?_ |>.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h'_1 : G.IsBridge e
x : V
p : (G ⊔ edge u v).Walk x x
hp : p.IsCycle
hpe : e ∈ p.edges
e' : Sym2 V
he' : e' ∈ p.edges
h' : e' ∈ (edge u v).edgeSet
⊢ p.IsCycle ∧ s(u, v) ∈ p.edges

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
h'_1 : G.IsBridge e
x : V
p : (G ⊔ edge u v).Walk x x
hp : p.IsCycle
hpe : e ∈ p.edges
e' : Sym2 V
he' : e' ∈ p.edges
h' : e' ∈ (edge u v).edgeSet
⊢ G.Reachable u v

Tactic:
exact .mono (sdiff_le_iff'.mpr le_rfl) <|
    adj_and_reachable_delete_edges_iff_exists_cycle.mpr ⟨_, p, by simp_all⟩ |>.right

Premises used: Iff.mpr, SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, And.right, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
s : Set (Sym2 V)
huv : ¬(G.deleteEdges s).Reachable u v
contrapose! : ∀ (huv : ∀ (e : Sym2 V) (_ : e ∈ s), e ∉ w.edges), (G.deleteEdges s).Reachable u v
⊢ ∃ e ∈ s, e ∈ w.edges

Tactic:
contrapose! huv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
s : Set (Sym2 V)
huv : ∀ (e : Sym2 V) (_ : e ∈ s), e ∉ w.edges
⊢ (G.deleteEdges s).Reachable u v

Tactic:
⟨w.toDeleteEdges _ fun _ ↦ imp_not_comm.1 <| huv _⟩

Premises used: Nonempty.intro, imp_not_comm, SimpleGraph.Walk.toDeleteEdges, Iff.mp, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
s : Set (Sym2 V)
huv : ∀ (e : Sym2 V) (_ : e ∈ s), e ∉ w.edges
⊢ (G.deleteEdges s).Reachable u v

Tactic:
exact ⟨w.toDeleteEdges _ fun _ ↦ imp_not_comm.1 <| huv _⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
e : Sym2 V
huv : ¬(G.deleteEdges {e}).Reachable u v
⊢ e ∈ w.edges

Tactic:
simpa using w.exists_mem_edges_of_not_reachable_deleteEdges huv

Premises used: SimpleGraph.Walk.exists_mem_edges_of_not_reachable_deleteEdges