awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
refine_2₁ : ∀ (e : Sym2 V) (he : e ∈ s), (G.deleteEdges s).Reachable u v
⊢ (G.deleteEdges s).Reachable u v

Tactic:
obtain rfl | ⟨e, he⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
hs : Set.encard.{u_1} (α := Sym2 V) ∅ < (↑(k + 1) : ℕ∞)
⊢ (G.deleteEdges ∅).Reachable u v

Tactic:
simpa using (h s(u, u)).reachable hk

Premises used: Sym2.mk, SimpleGraph.IsEdgeReachable.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
refine_2 : ((G.deleteEdges {e}).deleteEdges (s \ {e})).Reachable u v
⊢ (G.deleteEdges s).Reachable u v

Tactic:
rw [← Set.insert_diff_self_of_mem he, Set.insert_eq, ← deleteEdges_deleteEdges]

Premises used: Set.insert_eq, SimpleGraph.deleteEdges_deleteEdges, Set.insert_diff_self_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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

Tactic:
h e <| ENat.add_lt_add_iff_right ENat.one_ne_top |>.mp ?_

Premises used: ENat.one_ne_top, Iff.mp, ENat.add_lt_add_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
refine_2 : (s \ {e}).encard + 1 < HAdd.hAdd (α := ℕ∞) (↑k : ℕ∞) 1
⊢ ((G.deleteEdges {e}).deleteEdges (s \ {e})).Reachable u v

Tactic:
refine h e <| ENat.add_lt_add_iff_right ENat.one_ne_top |>.mp ?_

Premises used: ENat.one_ne_top, Iff.mp, ENat.add_lt_add_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
refine_2 refine_2₁ refine_2₂ refine_2₃ : s.encard < HAdd.hAdd (α := ℕ∞) (↑k : ℕ∞) 1
⊢ (s \ {e}).encard + 1 < HAdd.hAdd (α := ℕ∞) (↑k : ℕ∞) 1

Tactic:
rwa [Set.encard_diff_singleton_add_one he]

Premises used: Set.encard_diff_singleton_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
hk : k ≠ 0
⊢ G.IsEdgeConnected (k + 1) ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeConnected k

Tactic:
simp [IsEdgeConnected, isEdgeReachable_add_one hk, forall_comm (α := Sym2 _)]

Premises used: SimpleGraph.isEdgeReachable_add_one, forall_comm, SimpleGraph.IsEdgeConnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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

Tactic:
⟨fun h ↦ ⟨h.left, fun hc ↦ ?_⟩, fun ⟨hadj, hc⟩ ↦ ?_⟩

Premises used: Sym2.mk, SimpleGraph.IsBridge, _private.0.SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two.match_1, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
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)
⊢ G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v

Tactic:
refine ⟨fun h ↦ ⟨h.left, fun hc ↦ ?_⟩, fun ⟨hadj, hc⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hc : G.IsEdgeReachable 2 u v
⊢ False

Tactic:
isBridge_iff.mp h |>.right <| hc <| Set.encard_singleton _ |>.trans_lt Nat.one_lt_ofNat

Premises used: SimpleGraph.isBridge_iff, And.right, Eq.trans_lt, Iff.mp, Nat.one_lt_ofNat, Set.encard_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.IsBridge s(u, v)
hc : G.IsEdgeReachable 2 u v
⊢ False

Tactic:
exact isBridge_iff.mp h |>.right <| hc <| Set.encard_singleton _ |>.trans_lt Nat.one_lt_ofNat

Premises used: SimpleGraph.isBridge_iff, And.right, Eq.trans_lt, Iff.mp, Nat.one_lt_ofNat, Set.encard_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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)

Tactic:
isBridge_iff.mpr ⟨hadj, fun hr ↦ hc fun s hs₂ ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.isBridge_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
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
⊢ G.IsBridge s(u, v)

Tactic:
refine isBridge_iff.mpr ⟨hadj, fun hr ↦ hc fun s hs₂ ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.isBridge_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
neg : ∀ (hs₁ : s.encard = (↑1 : ℕ∞)), (G.deleteEdges s).Reachable u v
⊢ (G.deleteEdges s).Reachable u v

Tactic:
by_cases! hs₁ : s.encard ≠ (1 : ℕ)

Premises used: Set.encard, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
pos : s.encard < (↑1 : ℕ∞)
⊢ (G.deleteEdges s).Reachable u v

Tactic:
apply G.isEdgeReachable_one.mpr hadj.reachable

Premises used: Iff.mpr, SimpleGraph.Adj.reachable, SimpleGraph.isEdgeReachable_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
⊢ s.encard < (↑1 : ℕ∞)

Tactic:
lt_of_le_of_ne (ENat.lt_coe_add_one_iff.mp hs₂) hs₁

Premises used: Iff.mp, ENat.lt_coe_add_one_iff, lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
⊢ s.encard < (↑1 : ℕ∞)

Tactic:
exact lt_of_le_of_ne (ENat.lt_coe_add_one_iff.mp hs₂) hs₁

Premises used: Iff.mp, ENat.lt_coe_add_one_iff, lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
neg :
  ∀ (x : Sym2 V) (hs₂ : Set.encard (α := Sym2 V) {x} < (↑2 : ℕ∞)) (hs₁ : Set.encard (α := Sym2 V) {x} = (↑1 : ℕ∞)),
    (G.deleteEdges {x}).Reachable u v
⊢ (G.deleteEdges s).Reachable u v

Tactic:
obtain ⟨x, rfl⟩ := Set.encard_eq_one (s := s).mp hs₁

Premises used: Set.encard_eq_one, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
neg : ∀ (hx : ¬s(u, v) = x), (G.deleteEdges {x}).Reachable u v
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
by_cases hx : s(u, v) = x
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
hx : s(u, v) = x
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
hx ▸ hr

Premises used: Eq.rec
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
hx : s(u, v) = x
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
exact hx ▸ hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
hx : ¬s(u, v) = x
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
deleteEdges_adj.mpr ⟨hadj, hx⟩ |>.reachable

Premises used: Iff.mpr, SimpleGraph.Adj.reachable, SimpleGraph.deleteEdges_adj, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
hx : ¬s(u, v) = x
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
exact deleteEdges_adj.mpr ⟨hadj, hx⟩ |>.reachable

Premises used: Iff.mpr, SimpleGraph.Adj.reachable, SimpleGraph.deleteEdges_adj, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsEdgeReachable 2 u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Reachable u v

Tactic:
simp [isEdgeReachable_add_one]

Premises used: SimpleGraph.isEdgeReachable_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsEdgeConnected 2 ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Preconnected

Tactic:
simp [isEdgeConnected_add_one]

Premises used: SimpleGraph.isEdgeConnected_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
obtain : ∀ (w : G.Walk u v) (hw : w.IsPath), ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w
⊢ ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w

Tactic:
obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath

Premises used: SimpleGraph.Reachable.exists_isPath, SimpleGraph.IsEdgeReachable.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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.Nil

Tactic:
grind [Walk.not_nil_of_ne]

Premises used: SimpleGraph.Walk.not_nil_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
⊢ G.Adj u w.snd

Tactic:
have : G.Adj u w.snd := Walk.adj_snd (by grind [Walk.not_nil_of_ne])
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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

Tactic:
⟨w.snd, this, fun s hs ↦ ?_⟩

Premises used: And.intro, Exists.intro, SimpleGraph.Walk.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
refine : ∀ (s : Set (Sym2 V)) (hs : s.encard < (↑2 : ℕ∞)), (G.deleteEdges s).Reachable u w.snd
⊢ ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w

Tactic:
refine ⟨w.snd, this, fun s hs ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
neg : ∀ (h' : s ≠ {s(u, w.snd)}), (G.deleteEdges s).Reachable u w.snd
⊢ (G.deleteEdges s).Reachable u w.snd

Tactic:
by_cases! h' : s = {s(u, w.snd)}

Premises used: SimpleGraph.Walk.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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)}
pos : ∀ (hs : Set.encard (α := Sym2 V) {s(u, w.snd)} < (↑2 : ℕ∞)), (G.deleteEdges {s(u, w.snd)}).Reachable u w.snd
⊢ (G.deleteEdges s).Reachable u w.snd

Tactic:
subst h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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

Tactic:
Reachable.trans (h hs) <| w.tail.toDeleteEdge _ (fun hh ↦ ?_) |>.reachable.symm

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Walk.reachable, SimpleGraph.Walk.toDeleteEdge, SimpleGraph.Reachable.trans, SimpleGraph.Walk.tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
pos : ∀ (hh : s(u, w.snd) ∈ w.tail.edges), False
⊢ (G.deleteEdges {s(u, w.snd)}).Reachable u w.snd

Tactic:
refine Reachable.trans (h hs) <| w.tail.toDeleteEdge _ (fun hh ↦ ?_) |>.reachable.symm

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Walk.reachable, SimpleGraph.Walk.toDeleteEdge, SimpleGraph.Reachable.trans, SimpleGraph.Walk.tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
⊢ u = w.tail.snd

Tactic:
have := hw.tail.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hh)
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
⊢ u = w.getVert 2

Tactic:
simp only [Walk.getVert_tail, Nat.reduceAdd] at this

Premises used: SimpleGraph.Walk.getVert_tail, Nat.reduceAdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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.getVert 2
⊢ False

Tactic:
simpa using hw.getVert_eq_start_iff_of_not_nil (Walk.not_nil_of_ne hne) |>.mp this.symm

Premises used: Iff.mp, SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.IsPath.getVert_eq_start_iff_of_not_nil, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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

Tactic:
Walk.reachable <| Walk.cons (deleteEdges_adj.mpr ⟨this, ?_⟩) Walk.nil

Premises used: Iff.mpr, SimpleGraph.Walk.reachable, SimpleGraph.deleteEdges_adj, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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)}
neg : s(u, w.snd) ∉ s
⊢ (G.deleteEdges s).Reachable u w.snd

Tactic:
refine Walk.reachable <| Walk.cons (deleteEdges_adj.mpr ⟨this, ?_⟩) Walk.nil

Premises used: Iff.mpr, SimpleGraph.Walk.reachable, SimpleGraph.deleteEdges_adj, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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)}
neg : ∀ (h' : s(u, w.snd) ∈ s), s = {s(u, w.snd)}
⊢ s(u, w.snd) ∉ s

Tactic:
contrapose h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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)}

Tactic:
(Set.subsingleton_iff_singleton h').mp ?_

Premises used: Set.subsingleton_iff_singleton, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
neg : s.Subsingleton
⊢ s = {s(u, w.snd)}

Tactic:
refine (Set.subsingleton_iff_singleton h').mp ?_

Premises used: Set.subsingleton_iff_singleton, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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.Subsingleton

Tactic:
Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs)

Premises used: Iff.mp, Set.encard_le_one_iff_subsingleton, Order.le_of_lt_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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.Subsingleton

Tactic:
exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs)

Premises used: Iff.mp, Set.encard_le_one_iff_subsingleton, Order.le_of_lt_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ∀ (huy : ¬G.IsEdgeReachable 2 u x), x ∉ w.support
⊢ G.IsEdgeReachable 2 u x

Tactic:
contrapose huy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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_1 : Sym2 V), ¬(G.deleteEdges {x_1}).Reachable u x

Tactic:
simpa [isEdgeReachable_two] using huy

Premises used: SimpleGraph.isEdgeReachable_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
obtain : ∀ (e : Sym2 V) (he : ¬(G.deleteEdges {e}).Reachable u x), x ∉ w.support
⊢ x ∉ w.support

Tactic:
obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
⊢ ¬(G.deleteEdges {e}).Reachable v x

Tactic:
have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
he' : ¬(G.deleteEdges {e}).Reachable v x
hy : x ∈ w.support
⊢ e ∈ (w.dropUntil x hy).edges

Tactic:
simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he'

Premises used: SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
he' : ¬(G.deleteEdges {e}).Reachable v x
⊢ x ∉ w.support

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

Premises used: SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
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
⊢ 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')