awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
hxy : s(x, y) ∈ w.edges
⊢ s(x, y) ∈ (w.dropUntil y ⋯).edges

Tactic:
simpa using (w.dropUntil y _).reverse.mem_edges_of_not_reachable_deleteEdges hvy

Premises used: SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
⊢ s(x, y) ∉ w.edges

Tactic:
exact fun hxy ↦ hw.disjoint_edges_takeUntil_dropUntil (w.snd_mem_support_of_mem_edges hxy)
    ((w.takeUntil y _).mem_edges_of_not_reachable_deleteEdges huy)
    (by simpa using (w.dropUntil y _).reverse.mem_edges_of_not_reachable_deleteEdges hvy)

Premises used: SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.snd_mem_support_of_mem_edges, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
⊢ s(x, y) ∉ w.edges

Tactic:
classical
  exact fun hxy ↦ hw.disjoint_edges_takeUntil_dropUntil (w.snd_mem_support_of_mem_edges hxy)
    ((w.takeUntil y _).mem_edges_of_not_reachable_deleteEdges huy)
    (by simpa using (w.dropUntil y _).reverse.mem_edges_of_not_reachable_deleteEdges hvy)
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
⊢ y ∉ w.support

Tactic:
fun hy ↦ hw.not_mem_edges_of_not_reachable huy hvy <| w.edges_takeUntil_subset hy <|
    mem_edges_of_not_reachable_deleteEdges (w.takeUntil y hy) huy

Premises used: SimpleGraph.Walk.edges_takeUntil_subset, SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable, SimpleGraph.Walk.takeUntil, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
⊢ y ∉ w.support

Tactic:
exact fun hy ↦ hw.not_mem_edges_of_not_reachable huy hvy <| w.edges_takeUntil_subset hy <|
    mem_edges_of_not_reachable_deleteEdges (w.takeUntil y hy) huy

Premises used: SimpleGraph.Walk.edges_takeUntil_subset, SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable, SimpleGraph.Walk.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
⊢ y ∉ w.support

Tactic:
classical
  exact fun hy ↦ hw.not_mem_edges_of_not_reachable huy hvy <| w.edges_takeUntil_subset hy <|
    mem_edges_of_not_reachable_deleteEdges (w.takeUntil y hy) huy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u x : V
hxu : x ≠ u
hx : (G.neighborSet x).Subsingleton
w : V
hxv : x ≠ u
hw : IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
hxw : Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) x
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
obtain : ∀ (y : V) (hxy : G.Adj x y), False
⊢ False

Tactic:
obtain ⟨y, -, hxy⟩ := adj_of_mem_walk_support w (by rintro ⟨⟩; simp_all) hxw

Premises used: SimpleGraph.adj_of_mem_walk_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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

Tactic:
hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw

Premises used: SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
refine_2 : ¬(G.deleteEdges {s(y, x)}).Reachable v x
⊢ False

Tactic:
refine hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw

Premises used: SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
⊢ G.Adj x p.penultimate ∧ (x = y → ¬p.penultimate = x) ∧ ¬p.penultimate = y

Tactic:
simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)

Premises used: SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
⊢ 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 ‹_›)

Premises used: SimpleGraph.Adj, SimpleGraph.Walk.penultimate
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
⊢ ¬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 ‹_›)

Premises used: SimpleGraph.Adj, SimpleGraph.Walk.penultimate
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hy₂ : ¬p.penultimate = y
⊢ False

Tactic:
hy₂ <| hx hx₂ hxy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hy₂ : ¬p.penultimate = y
⊢ False

Tactic:
exact hy₂ <| hx hx₂ hxy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
⊢ G.Adj x p.penultimate ∧ (x = y → ¬p.penultimate = x) ∧ ¬p.penultimate = y

Tactic:
simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)

Premises used: SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
⊢ 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 ‹_›)

Premises used: SimpleGraph.Adj, SimpleGraph.Walk.penultimate
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
⊢ ¬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 ‹_›)

Premises used: SimpleGraph.Adj, SimpleGraph.Walk.penultimate
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hy₂ : ¬p.penultimate = y
⊢ False

Tactic:
hy₂ <| hx hx₂ hxy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hy₂ : ¬p.penultimate = y
⊢ False

Tactic:
exact hy₂ <| hx hx₂ hxy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
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)
⊢ (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

Premises used: SimpleGraph.Preconnected.exists_isPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
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)
⊢ (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:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
val : ∀ x ∈ p.support, x ∈ s
⊢ (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:
convert! p.induce s _

Premises used: SimpleGraph.Walk.induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
val : ∀ (hws : w ∉ s), False
⊢ w ∈ s

Tactic:
by_contra hws
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hws : w ∉ s
⊢ w ≠ u

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hws : w ∉ s
⊢ w ≠ v

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
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
hws : w ∉ s
⊢ False

Tactic:
exact hp.not_mem_support_of_subsingleton_neighborSet (by grind) (by grind) (hs _ hws) hwp

Premises used: SimpleGraph.Walk.IsPath.isTrail, SimpleGraph.Walk.IsTrail.not_mem_support_of_subsingleton_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u : V
⊢ G.IsEdgeReachable k u u

Tactic:
fun _ _ ↦ .rfl

Premises used: SimpleGraph.IsEdgeReachable, SimpleGraph.Reachable.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u : V
⊢ G.IsEdgeReachable k u u

Tactic:
.rfl

Premises used: SimpleGraph.IsEdgeReachable.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
h : G.IsEdgeReachable k u v
⊢ G.IsEdgeReachable k v u

Tactic:
fun _ hk ↦ (h hk).symm

Premises used: SimpleGraph.IsEdgeReachable, SimpleGraph.Reachable.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
⊢ G.IsEdgeReachable k u v ↔ G.IsEdgeReachable k v u

Tactic:
⟨.symm, .symm⟩

Premises used: SimpleGraph.IsEdgeReachable.symm, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v w : V
h1 : G.IsEdgeReachable k u v
h2 : G.IsEdgeReachable k v w
⊢ G.IsEdgeReachable k u w

Tactic:
fun _ hk ↦ (h1 hk).trans (h2 hk)

Premises used: SimpleGraph.IsEdgeReachable, SimpleGraph.Reachable.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G H : SimpleGraph V
k : ℕ
u v : V
hGH : G ≤ H
h : G.IsEdgeReachable k u v
⊢ H.IsEdgeReachable k u v

Tactic:
fun _ hk ↦ h hk |>.mono <| deleteEdges_mono hGH

Premises used: SimpleGraph.IsEdgeReachable, SimpleGraph.Reachable.mono, SimpleGraph.deleteEdges_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x : Set (Sym2 V)
hk grw : x.encard < (↑k : ℕ∞)
⊢ x.encard < (↑l : ℕ∞)

Tactic:
grw [← hkl]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x : Set (Sym2 V)
hk : x.encard < (↑k : ℕ∞)
⊢ x.encard < (↑k : ℕ∞)

Tactic:
hk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x : Set (Sym2 V)
hk : x.encard < (↑k : ℕ∞)
⊢ x.encard < (↑k : ℕ∞)

Tactic:
exact hk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsEdgeReachable 0 u v

Tactic:
simp [IsEdgeReachable]

Premises used: SimpleGraph.IsEdgeReachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsEdgeConnected 0

Tactic:
fun _ _ ↦ .zero

Premises used: SimpleGraph.IsEdgeReachable.zero, SimpleGraph.IsEdgeConnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsEdgeReachable 1 u v ↔ G.Reachable u v

Tactic:
simp [IsEdgeReachable, ENat.lt_one_iff_eq_zero]

Premises used: SimpleGraph.IsEdgeReachable, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsEdgeConnected 1 ↔ G.Preconnected

Tactic:
simp [IsEdgeConnected, Preconnected]

Premises used: SimpleGraph.Preconnected, SimpleGraph.IsEdgeConnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
huv : G.IsEdgeReachable k u v
⊢ G.Reachable u v

Tactic:
isEdgeReachable_one.mp (huv.anti (Nat.one_le_iff_ne_zero.mpr hk))

Premises used: Iff.mpr, SimpleGraph.isEdgeReachable_one, SimpleGraph.IsEdgeReachable.anti, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst : Subsingleton V
⊢ G.IsEdgeReachable k u v

Tactic:
fun _ _ ↦ .of_subsingleton

Premises used: SimpleGraph.IsEdgeReachable, SimpleGraph.Reachable.of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
inst : Subsingleton V
⊢ G.IsEdgeConnected k

Tactic:
fun _ _ ↦ .of_subsingleton

Premises used: SimpleGraph.IsEdgeReachable.of_subsingleton, SimpleGraph.IsEdgeConnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
k : ℕ
hk : k ≠ 0
h : G.IsEdgeConnected k
⊢ G.Preconnected

Tactic:
fun u v ↦ (h u v).reachable hk

Premises used: SimpleGraph.Preconnected, SimpleGraph.IsEdgeReachable.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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! : ∀ (hh : G.degree u < k), False
⊢ k ≤ G.degree u

Tactic:
by_contra! hh
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
⊢ (G.incidenceSet u).encard < (↑k : ℕ∞)

Tactic:
rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh

Premises used: SimpleGraph.card_incidenceSet_eq_degree, Set.coe_fintypeCard, ENat.coe_lt_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
obtain : ∀ (w : (G.deleteEdges (G.incidenceSet u)).Walk u v), w.IsPath → False
⊢ False

Tactic:
obtain ⟨w, _⟩ := h hh |>.exists_isPath

Premises used: SimpleGraph.Reachable.exists_isPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
w : (G.deleteEdges (G.incidenceSet u)).Walk u v
h_1 : w.IsPath
⊢ False

Tactic:
simpa using w.adj_snd <| mt Walk.Nil.eq huv

Premises used: mt, SimpleGraph.Walk.Nil.eq, SimpleGraph.Walk.adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
by_contra!₁₂ :
  ∀ (hh : (G.incidenceSet u).encard < (↑k : ℕ∞)) (w : (G.deleteEdges (G.incidenceSet u)).Walk u v), w.IsPath → False
⊢ k ≤ G.degree u

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

Premises used: SimpleGraph.card_incidenceSet_eq_degree, Set.coe_fintypeCard, mt, SimpleGraph.Walk.Nil.eq, ENat.coe_lt_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
obtain : ∀ (v : V) (hv : v ≠ u), k ≤ G.degree u
⊢ k ≤ G.degree u

Tactic:
obtain ⟨v, hv⟩ := exists_ne u

Premises used: exists_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
v : V
hv : v ≠ u
⊢ k ≤ G.degree u

Tactic:
(h u v).le_degree hv.symm

Premises used: Ne.symm, SimpleGraph.IsEdgeReachable.le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
v : V
hv : v ≠ u
⊢ k ≤ G.degree u

Tactic:
exact (h u v).le_degree hv.symm

Premises used: Ne.symm, SimpleGraph.IsEdgeReachable.le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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

Tactic:
⟨fun h e s hk ↦ ?_, fun h s hs ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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
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
⊢ G.IsEdgeReachable (k + 1) u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v

Tactic:
refine ⟨fun h e s hk ↦ ?_, fun h s hs ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
refine_1 : (G.deleteEdges (s ∪ {e})).Reachable u v
⊢ ((G.deleteEdges {e}).deleteEdges s).Reachable u v

Tactic:
rw [deleteEdges_deleteEdges, Set.union_comm]

Premises used: Set.union_comm, SimpleGraph.deleteEdges_deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
refine_1 : (s ∪ {e}).encard < (↑(k + 1) : ℕ∞)
⊢ (G.deleteEdges (s ∪ {e})).Reachable u v

Tactic:
apply h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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 : ℕ∞)
refine_1 : s.encard + 1 < (↑(k + 1) : ℕ∞)
⊢ (s ∪ {e}).encard < (↑(k + 1) : ℕ∞)

Tactic:
grw [Set.encard_union_le, Set.encard_singleton]

Premises used: Set.encard_union_le, Set.encard_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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.encard + 1 < (↑(k + 1) : ℕ∞)

Tactic:
ENat.add_lt_add_iff_right ENat.one_ne_top |>.mpr hk

Premises used: Iff.mpr, ENat.one_ne_top, WithTop.map₂, WithTop.some, ENat.add_lt_add_iff_right, Option.map₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
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.encard + 1 < (↑(k + 1) : ℕ∞)

Tactic:
exact ENat.add_lt_add_iff_right ENat.one_ne_top |>.mpr hk

Premises used: Iff.mpr, ENat.one_ne_top, ENat.add_lt_add_iff_right