awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
⊢ False
have hpq' : s(v, w) ∈ pwv.reverse.edges
Tactic: have hpq' := hb pwv.reverse
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.reverse.edges
⊢ False
have hpq'₁ : s(v, w) ∈ pwv.edges
Tactic: rw [Walk.edges_reverse, List.mem_reverse] at hpq'
Cleared hypotheses: hpq'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
hw₁ : w ∈ (c.takeUntil v ⋯).support
hv₁ : v ∈ c.support
⊢ False
have hc₁ : let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
let pvu := c.dropUntil v hv₁;
((pvu.append puw).edges ++ pwv.edges).Nodup
Tactic: rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc
Cleared hypotheses: hc, he, hw, hv, puw, pwv, pvu, this, hbq, hpq'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ 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
have 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
Tactic: rw [reachable_deleteEdges_iff_exists_walk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
have mp : (Walk.cons sorry (↑p.toPath : G.Walk v w)).IsCycle
Tactic: refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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 : (Walk.cons ⋯ (↑p.toPath : G.Walk v w)).IsCycle
⊢ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
have mp₁ : s(v, w) ∈ (Walk.cons sorry (↑p.toPath : G.Walk v w)).edges
Tactic: refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (Walk.cons ⋯ (↑p.toPath : G.Walk v w)).IsCycle
have mp : s(w, v) ∉ (↑p.toPath : G.Walk v w).edges
Tactic: apply Path.cons_isCycle
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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(w, v) ∉ (↑p.toPath : G.Walk v w).edges
have mp : s(v, w) ∉ (↑p.toPath : G.Walk v w).edges
Tactic: rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
have mpr : ∃ (p : G.Walk v w), s(v, w) ∉ p.edges
Tactic: refine ⟨c.adj_of_mem_edges he, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges
have mpr : ∀ (hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges), False
Tactic: by_contra! hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
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
⊢ False
have hb' : ∀ (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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
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
⊢ False
have hvc : v ∈ c.support
Tactic: have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
have mpr : s(w, v) ∈ (c.rotate v hvc).edges
Tactic: refine reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate v hvc) (hc.isTrail.rotate hvc)
      ?_ (Walk.start_mem_support _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ s(w, v) ∈ (c.rotate v hvc).edges
have mpr : s(w, v) ∈ c.edges
Tactic: rwa [(c.rotate_edges v hvc).mem_iff, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
have 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)
Tactic: rw [isBridge_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : 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
have contrapose! : (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : 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
have rw : (G.deleteEdges {s(v, w)}).Reachable v w ↔ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w
Tactic: rw [← adj_and_reachable_delete_edges_iff_exists_cycle]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).Connected
have h₁ : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y
Tactic: simp only [isBridge_iff, not_and, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Connected
have inl : ∀ (hxy : ¬G.Adj x y), (G.deleteEdges {s(x, y)}).Connected
Tactic: obtain hxy | hxy := em' <| G.Adj x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Connected
have inr : ∀ (hxy : G.Adj x y), (G.deleteEdges {s(x, y)}).Connected
Tactic: obtain hxy | hxy := em' <| G.Adj x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
have inl : (G \ fromEdgeSet {s(x, y)}).Connected
Tactic: rwa [deleteEdges, Disjoint.sdiff_eq_left (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
have inr : ∀ (w : V), (G.deleteEdges {s(x, y)}).Reachable x w
Tactic: refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
have inr : ∀ (P : G.Walk w x) (hP : P.IsPath), (G.deleteEdges {s(x, y)}).Reachable x w
Tactic: obtain ⟨P, hP⟩ := hG.exists_isPath w x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
have inr : ∀ (heP : s(x, y) ∉ P.edges), (G.deleteEdges {s(x, y)}).Reachable x w
Tactic: obtain heP | heP := em' <| s(x, y) ∈ P.edges
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
have inr₁ : ∀ (heP : s(x, y) ∈ P.edges), (G.deleteEdges {s(x, y)}).Reachable x w
Tactic: obtain heP | heP := em' <| s(x, y) ∈ P.edges
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
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
have hyP : y ∈ P.support
Tactic: have hyP := P.snd_mem_support_of_mem_edges heP
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
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
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
have hxP₁ : x ∉ (P.takeUntil y hyP).support
Tactic: have hxP₁ := Walk.endpoint_notMem_support_takeUntil hP hyP hxy.ne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
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
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
have heP₁ : s(x, y) ∉ P₁.edges
Tactic: have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).Connected
have simp : ∀ (h : G.Adj x y → (G.deleteEdges {s(x, y)}).Reachable x y), (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)⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Connected
have 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
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)⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Connected
have 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
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)⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Connected
have 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
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)⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.deleteEdges {s(x, y)}).Connected
have 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
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)⟩)
Cleared hypotheses: h