awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ (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)
  (heP : s(x, y) ∉ P.edges), (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
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
⊢ (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)
  (heP : s(x, y) ∈ P.edges), (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
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
⊢ (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)
  (heP : s(x, y) ∈ P.edges) (hyP : y ∈ P.support), (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
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
⊢ (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)
  (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
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
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
⊢ (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)
  (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
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
u v : V
h : ¬G.Reachable u v
⊢ (G ⊔ edge u v).IsBridge s(u, v)
have refine : ¬((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable u v
Tactic: refine isBridge_iff.mpr ⟨.inr ⟨Set.mem_singleton _, mt (· ▸ .rfl) h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
have refine : ∀ ⦃u_1 : V⦄ (p : (G ⊔ edge u v).Walk u_1 u_1), p.IsCycle → e ∉ p.edges
Tactic: refine isBridge_iff_mem_and_forall_cycle_notMem.mpr ⟨edgeSet_mono le_sup_left h'.left, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
have 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
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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ e' ∈ G.edgeSet
have refine : ∀ (h' : e' ∈ (edge u v).edgeSet), G.Reachable u v
Tactic: refine edgeSet_sup .. ▸ Walk.edges_subset_edgeSet _ he' |>.elim id fun h' ↦ h ?_ |>.elim
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ ∃ e ∈ s, e ∈ w.edges
have contrapose! : ∀ (huv : ∀ (e : Sym2 V) (_ : e ∈ s), e ∉ w.edges), (G.deleteEdges s).Reachable u v
Tactic: contrapose! huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
⊢ False
have obtain : ∀ (y : V) (hxy : G.Adj x y), False
Tactic: obtain ⟨y, -, hxy⟩ := adj_of_mem_walk_support w (by rintro ⟨⟩; simp_all) hxw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ False
have refine_1 : ¬(G.deleteEdges {s(y, x)}).Reachable u x
Tactic: refine hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
refine_1 : ¬(G.deleteEdges {s(y, x)}).Reachable u x
⊢ False
have refine_2 : ¬(G.deleteEdges {s(y, x)}).Reachable v x
Tactic: refine hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk u x
⊢ False
have hx₂ : G.Adj x p.penultimate
Tactic: obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk u x
hx₂ : G.Adj x p.penultimate
⊢ False
have hy₂ : ¬p.penultimate = y
Tactic: obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk v x
⊢ False
have hx₂ : G.Adj x p.penultimate
Tactic: obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk v x
hx₂ : G.Adj x p.penultimate
⊢ False
have hy₂ : ¬p.penultimate = y
Tactic: obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
⊢ (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)
have obtain : ∀ (p : G.Walk u v) (hp : p.IsPath),
  (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)
Tactic: obtain ⟨p, hp⟩ := hG.exists_isPath u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)
have val : (induce s G).Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ (induce s G).Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)
have val : ∀ x ∈ p.support, x ∈ s
Tactic: convert! p.induce s _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
w : V
hwp : w ∈ p.support
⊢ w ∈ s
have val : ∀ (hws : w ∉ s), False
Tactic: by_contra hws
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
⊢ k ≤ G.degree u
have by_contra! : ∀ (hh : G.degree u < k), False
Tactic: by_contra! hh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
hh : G.degree u < k
⊢ False
have hh₁ : (G.incidenceSet u).encard < (↑k : ℕ∞)
Tactic: rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
hh : (G.incidenceSet u).encard < (↑k : ℕ∞)
⊢ False
have obtain : ∀ (w : (G.deleteEdges (G.incidenceSet u)).Walk u v), w.IsPath → False
Tactic: obtain ⟨w, _⟩ := h hh |>.exists_isPath
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
⊢ k ≤ G.degree u
have by_contra! : ¬k ≤ G.degree u → False
Tactic: classical
  by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬k ≤ G.degree u → False
⊢ k ≤ G.degree u
have by_contra!₄ : G.degree u < k → False
Tactic: classical
  by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬k ≤ G.degree u → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (hh : G.degree u < k), False
⊢ k ≤ G.degree u
have by_contra!₁₁ : ∀ (hh : (G.incidenceSet u).encard < (↑k : ℕ∞)), False
Tactic: classical
  by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
h : G.IsEdgeReachable k u v
huv : u ≠ v
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬k ≤ G.degree u → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (hh : G.degree u < k), False
by_contra!₁₁ : ∀ (hh : (G.incidenceSet u).encard < (↑k : ℕ∞)), False
⊢ k ≤ G.degree u
have by_contra!₁₂ : ∀ (hh : (G.incidenceSet u).encard < (↑k : ℕ∞)) (w : (G.deleteEdges (G.incidenceSet u)).Walk u v), w.IsPath → False
Tactic: classical
  by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u : V
inst : Fintype (↑(G.neighborSet u) : Type u_1)
inst_1 : Nontrivial V
h : G.IsEdgeConnected k
⊢ k ≤ G.degree u
have obtain : ∀ (v : V) (hv : v ≠ u), k ≤ G.degree u
Tactic: obtain ⟨v, hv⟩ := exists_ne u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
⊢ G.IsEdgeReachable (k + 1) u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
have refine_1 : ∀ (h : G.IsEdgeReachable (k + 1) u v) (e : Sym2 V) (s : Set (Sym2 V)) (hk : s.encard < (↑k : ℕ∞)),
  ((G.deleteEdges {e}).deleteEdges s).Reachable u v
Tactic: refine ⟨fun h e s hk ↦ ?_, fun h s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
refine_1 :
  ∀ (h : G.IsEdgeReachable (k + 1) u v) (e : Sym2 V) (s : Set (Sym2 V)) (hk : s.encard < (↑k : ℕ∞)),
    ((G.deleteEdges {e}).deleteEdges s).Reachable u v
⊢ G.IsEdgeReachable (k + 1) u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
have refine_2 : ∀ (h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v) (s : Set (Sym2 V)) (hs : s.encard < (↑(k + 1) : ℕ∞)),
  (G.deleteEdges s).Reachable u v
Tactic: refine ⟨fun h e s hk ↦ ?_, fun h s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk_1 : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < (↑k : ℕ∞)
⊢ ((G.deleteEdges {e}).deleteEdges s).Reachable u v
have refine_1 : (G.deleteEdges (s ∪ {e})).Reachable u v
Tactic: rw [deleteEdges_deleteEdges, Set.union_comm]