awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (s ∪ {e})).Reachable u v
have refine_1 : (s ∪ {e}).encard < (↑(k + 1) : ℕ∞)
Tactic: apply h
-- 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 : ℕ∞)
⊢ (s ∪ {e}).encard < (↑(k + 1) : ℕ∞)
have refine_1 : s.encard + 1 < (↑(k + 1) : ℕ∞)
Tactic: grw [Set.encard_union_le, Set.encard_singleton]
-- 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
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
have refine_2 : ∀ (hs : Set.encard.{u_1} (α := Sym2 V) ∅ < (↑(k + 1) : ℕ∞)), (G.deleteEdges ∅).Reachable u v
Tactic: obtain rfl | ⟨e, he⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: 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
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < (↑(k + 1) : ℕ∞)
refine_2 : ∀ (hs : Set.encard.{u_1} (α := Sym2 V) ∅ < (↑(k + 1) : ℕ∞)), (G.deleteEdges ∅).Reachable u v
⊢ (G.deleteEdges s).Reachable u v
have refine_2₁ : ∀ (e : Sym2 V) (he : e ∈ s), (G.deleteEdges s).Reachable u v
Tactic: obtain rfl | ⟨e, he⟩ := s.eq_empty_or_nonempty
-- 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
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < (↑(k + 1) : ℕ∞)
e : Sym2 V
he : e ∈ s
⊢ (G.deleteEdges s).Reachable u v
have refine_2 : ((G.deleteEdges {e}).deleteEdges (s \ {e})).Reachable u v
Tactic: rw [← Set.insert_diff_self_of_mem he, Set.insert_eq, ← deleteEdges_deleteEdges]
-- 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
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < (↑(k + 1) : ℕ∞)
e : Sym2 V
he : e ∈ s
⊢ ((G.deleteEdges {e}).deleteEdges (s \ {e})).Reachable u v
have refine_2 : (s \ {e}).encard + 1 < HAdd.hAdd (α := ℕ∞) (↑k : ℕ∞) 1
Tactic: refine h e <| ENat.add_lt_add_iff_right ENat.one_ne_top |>.mp ?_
-- 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
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < (↑(k + 1) : ℕ∞)
e : Sym2 V
he : e ∈ s
⊢ (s \ {e}).encard + 1 < HAdd.hAdd (α := ℕ∞) (↑k : ℕ∞) 1
have refine_2 : s.encard < HAdd.hAdd (α := ℕ∞) (↑k : ℕ∞) 1
Tactic: rwa [Set.encard_diff_singleton_add_one he]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
have refine_1 : ∀ (h : G.IsBridge s(u, v)) (hc : G.IsEdgeReachable 2 u v), False
Tactic: refine ⟨fun h ↦ ⟨h.left, fun hc ↦ ?_⟩, fun ⟨hadj, hc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.IsBridge s(u, v)) (hc : G.IsEdgeReachable 2 u v), False
⊢ G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
have refine_2 : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v → ∀ (hadj : G.Adj u v) (hc : ¬G.IsEdgeReachable 2 u v), G.IsBridge s(u, v)
Tactic: refine ⟨fun h ↦ ⟨h.left, fun hc ↦ ?_⟩, fun ⟨hadj, hc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
⊢ G.IsBridge s(u, v)
have refine_2 : ∀ (hr : (G.deleteEdges {s(u, v)}).Reachable u v) (s : Set (Sym2 V)) (hs₂ : s.encard < (↑2 : ℕ∞)),
  (G.deleteEdges s).Reachable u v
Tactic: refine isBridge_iff.mpr ⟨hadj, fun hr ↦ hc fun s hs₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable u v
s : Set (Sym2 V)
hs₂ : s.encard < (↑2 : ℕ∞)
⊢ (G.deleteEdges s).Reachable u v
have pos : ∀ (hs₁ : s.encard ≠ (↑1 : ℕ∞)), (G.deleteEdges s).Reachable u v
Tactic: by_cases! hs₁ : s.encard ≠ (1 : ℕ)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable u v
s : Set (Sym2 V)
hs₂ : s.encard < (↑2 : ℕ∞)
pos : ∀ (hs₁ : s.encard ≠ (↑1 : ℕ∞)), (G.deleteEdges s).Reachable u v
⊢ (G.deleteEdges s).Reachable u v
have neg : ∀ (hs₁ : s.encard = (↑1 : ℕ∞)), (G.deleteEdges s).Reachable u v
Tactic: by_cases! hs₁ : s.encard ≠ (1 : ℕ)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable u v
s : Set (Sym2 V)
hs₂ : s.encard < (↑2 : ℕ∞)
hs₁ : s.encard ≠ (↑1 : ℕ∞)
⊢ (G.deleteEdges s).Reachable u v
have pos : s.encard < (↑1 : ℕ∞)
Tactic: apply G.isEdgeReachable_one.mpr hadj.reachable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable u v
s : Set (Sym2 V)
hs₂ : s.encard < (↑2 : ℕ∞)
hs₁ : s.encard = (↑1 : ℕ∞)
⊢ (G.deleteEdges s).Reachable u v
have neg : ∀ (x : Sym2 V) (hs₂ : Set.encard (α := Sym2 V) {x} < (↑2 : ℕ∞)) (hs₁ : Set.encard (α := Sym2 V) {x} = (↑1 : ℕ∞)),
  (G.deleteEdges {x}).Reachable u v
Tactic: obtain ⟨x, rfl⟩ := Set.encard_eq_one (s := s).mp hs₁
Cleared hypotheses: s, hs₂, hs₁
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable u v
x : Sym2 V
hs₂ : Set.encard (α := Sym2 V) {x} < (↑2 : ℕ∞)
hs₁ : Set.encard (α := Sym2 V) {x} = (↑1 : ℕ∞)
⊢ (G.deleteEdges {x}).Reachable u v
have pos : ∀ (hx : s(u, v) = x), (G.deleteEdges {x}).Reachable u v
Tactic: by_cases hx : s(u, v) = x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v
hadj : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable u v
x : Sym2 V
hs₂ : Set.encard (α := Sym2 V) {x} < (↑2 : ℕ∞)
hs₁ : Set.encard (α := Sym2 V) {x} = (↑1 : ℕ∞)
pos : ∀ (hx : s(u, v) = x), (G.deleteEdges {x}).Reachable u v
⊢ (G.deleteEdges {x}).Reachable u v
have neg : ∀ (hx : ¬s(u, v) = x), (G.deleteEdges {x}).Reachable u v
Tactic: by_cases hx : s(u, v) = x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
⊢ ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w
have obtain : ∀ (w : G.Walk u v) (hw : w.IsPath), ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w
Tactic: obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
⊢ ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w
have this : G.Adj u w.snd
Tactic: have : G.Adj u w.snd := Walk.adj_snd (by grind [Walk.not_nil_of_ne])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
⊢ ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w
have refine : ∀ (s : Set (Sym2 V)) (hs : s.encard < (↑2 : ℕ∞)), (G.deleteEdges s).Reachable u w.snd
Tactic: refine ⟨w.snd, this, fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < (↑2 : ℕ∞)
⊢ (G.deleteEdges s).Reachable u w.snd
have pos : ∀ (h' : s = {s(u, w.snd)}), (G.deleteEdges s).Reachable u w.snd
Tactic: by_cases! h' : s = {s(u, w.snd)}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < (↑2 : ℕ∞)
pos : ∀ (h' : s = {s(u, w.snd)}), (G.deleteEdges s).Reachable u w.snd
⊢ (G.deleteEdges s).Reachable u w.snd
have neg : ∀ (h' : s ≠ {s(u, w.snd)}), (G.deleteEdges s).Reachable u w.snd
Tactic: by_cases! h' : s = {s(u, w.snd)}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < (↑2 : ℕ∞)
h' : s = {s(u, w.snd)}
⊢ (G.deleteEdges s).Reachable u w.snd
have pos : ∀ (hs : Set.encard (α := Sym2 V) {s(u, w.snd)} < (↑2 : ℕ∞)), (G.deleteEdges {s(u, w.snd)}).Reachable u w.snd
Tactic: subst h'
Cleared hypotheses: s, hs, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
hs : Set.encard (α := Sym2 V) {s(u, w.snd)} < (↑2 : ℕ∞)
⊢ (G.deleteEdges {s(u, w.snd)}).Reachable u w.snd
have pos : ∀ (hh : s(u, w.snd) ∈ w.tail.edges), False
Tactic: refine Reachable.trans (h hs) <| w.tail.toDeleteEdge _ (fun hh ↦ ?_) |>.reachable.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
hs : Set.encard (α := Sym2 V) {s(u, w.snd)} < (↑2 : ℕ∞)
hh : s(u, w.snd) ∈ w.tail.edges
⊢ False
have this₁ : u = w.tail.snd
Tactic: have := hw.tail.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hh)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this_1 : G.Adj u w.snd
hs : Set.encard (α := Sym2 V) {s(u, w.snd)} < (↑2 : ℕ∞)
hh : s(u, w.snd) ∈ w.tail.edges
this : u = w.tail.snd
⊢ False
have this₁ : u = w.getVert 2
Tactic: simp only [Walk.getVert_tail, Nat.reduceAdd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < (↑2 : ℕ∞)
h' : s ≠ {s(u, w.snd)}
⊢ (G.deleteEdges s).Reachable u w.snd
have neg : s(u, w.snd) ∉ s
Tactic: refine Walk.reachable <| Walk.cons (deleteEdges_adj.mpr ⟨this, ?_⟩) Walk.nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < (↑2 : ℕ∞)
h' : s ≠ {s(u, w.snd)}
⊢ s(u, w.snd) ∉ s
have neg : ∀ (h' : s(u, w.snd) ∈ s), s = {s(u, w.snd)}
Tactic: contrapose h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < (↑2 : ℕ∞)
h' : s(u, w.snd) ∈ s
⊢ s = {s(u, w.snd)}
have neg : s.Subsingleton
Tactic: refine (Set.subsingleton_iff_singleton h').mp ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : x ∈ w.support
⊢ G.IsEdgeReachable 2 u x
have contrapose : ∀ (huy : ¬G.IsEdgeReachable 2 u x), x ∉ w.support
Tactic: contrapose huy
Cleared hypotheses: huy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
⊢ x ∉ w.support
have obtain : ∀ (e : Sym2 V) (he : ¬(G.deleteEdges {e}).Reachable u x), x ∉ w.support
Tactic: obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
e : Sym2 V
he : ¬(G.deleteEdges {e}).Reachable u x
⊢ x ∉ w.support
have he' : ¬(G.deleteEdges {e}).Reachable v x
Tactic: have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : x ∈ w.support
⊢ G.IsEdgeReachable 2 u x
have contrapose : ∀ (huy : x ∈ w.support), G.IsEdgeReachable 2 u x
Tactic: classical
  contrapose huy
  obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
  have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
  exact fun hy ↦ hw.disjoint_edges_takeUntil_dropUntil hy
    ((w.takeUntil x _).mem_edges_of_not_reachable_deleteEdges he)
    (by simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he')
Cleared hypotheses: huy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : x ∈ w.support
contrapose contrapose₁ : ∀ (huy : x ∈ w.support), G.IsEdgeReachable 2 u x
⊢ G.IsEdgeReachable 2 u x
have contrapose₂ : ¬G.IsEdgeReachable 2 u x → x ∉ w.support
Tactic: classical
  contrapose huy
  obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
  have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
  exact fun hy ↦ hw.disjoint_edges_takeUntil_dropUntil hy
    ((w.takeUntil x _).mem_edges_of_not_reachable_deleteEdges he)
    (by simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he')
Cleared hypotheses: huy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : x ∈ w.support
contrapose contrapose₁ : ∀ (huy : x ∈ w.support), G.IsEdgeReachable 2 u x
contrapose₂ contrapose₃ contrapose₄ : ∀ (huy : ¬G.IsEdgeReachable 2 u x), x ∉ w.support
⊢ G.IsEdgeReachable 2 u x
have contrapose₅ : ∀ (huy : ¬G.IsEdgeReachable 2 u x) (e : Sym2 V) (he : ¬(G.deleteEdges {e}).Reachable u x), x ∉ w.support
Tactic: classical
  contrapose huy
  obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
  have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
  exact fun hy ↦ hw.disjoint_edges_takeUntil_dropUntil hy
    ((w.takeUntil x _).mem_edges_of_not_reachable_deleteEdges he)
    (by simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he')
Cleared hypotheses: huy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : x ∈ w.support
contrapose contrapose₁ : ∀ (huy : x ∈ w.support), G.IsEdgeReachable 2 u x
contrapose₂ contrapose₃ contrapose₄ : ∀ (huy : ¬G.IsEdgeReachable 2 u x), x ∉ w.support
contrapose₅ : ∀ (huy : ¬G.IsEdgeReachable 2 u x) (e : Sym2 V) (he : ¬(G.deleteEdges {e}).Reachable u x), x ∉ w.support
⊢ G.IsEdgeReachable 2 u x
have contrapose₆ : ∀ (huy : ¬G.IsEdgeReachable 2 u x) (e : Sym2 V) (he : ¬(G.deleteEdges {e}).Reachable u x)
  (he' : ¬(G.deleteEdges {e}).Reachable v x), x ∉ w.support
Tactic: classical
  contrapose huy
  obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
  have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
  exact fun hy ↦ hw.disjoint_edges_takeUntil_dropUntil hy
    ((w.takeUntil x _).mem_edges_of_not_reachable_deleteEdges he)
    (by simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he')
Cleared hypotheses: huy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v ↔ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
have mp : G.Reachable u v → ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
mp : G.Reachable u v → ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
⊢ G.Reachable u v ↔ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
have mpr : (∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty) → G.Reachable u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
⊢ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
have mp : ∀ (p : G.Path u v), ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
Tactic: refine r.elim_path fun p => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
have mp : (↑p : G.Walk u v) ∈ G.finsetWalkLength (↑(⟨(↑p : G.Walk u v).length, sorry⟩ : Fin (Fintype.card V)) : ℕ) u v
Tactic: refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Connected
have rw : G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Preconnected ∧ Nonempty V
Tactic: rw [connected_iff, ← Finset.univ_nonempty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
rw : G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Preconnected ∧ Nonempty V
⊢ G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Connected
have rw₁ : G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ
Tactic: rw [connected_iff, ← Finset.univ_nonempty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))
have intro : ∀ (val : Fintype V),
  Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))
have intro : Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
  Odd
    (card.{u} (α := V)
      (disjiUnion {c : G.ConnectedComponent | c.supp ⊆ c'.supp} (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset) sorry))
Tactic: rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd
      (card.{u} (α := V)
        (disjiUnion {c : G.ConnectedComponent | c.supp ⊆ c'.supp} (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset) ⋯))
have intro : Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
  Odd (α := ℕ) (∑ x : G.ConnectedComponent with x.supp ⊆ c'.supp, #(filter (Membership.mem x.supp) univ))
Tactic: simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent with x.supp ⊆ c'.supp, #(filter (Membership.mem x.supp) univ))
have intro : Odd #({a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a}) ↔
  Odd
    (card.{u} (α := G.ConnectedComponent)
      ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}))
Tactic: rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
⊢ Odd #({a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a}) ↔
    Odd
      (card.{u} (α := G.ConnectedComponent)
        ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}))
have intro : {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} =
  {x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}
Tactic: congr! 2