awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : G.connectedComponentMk a = i
hsy : i = j
⊢ False

Tactic:
exact h hsy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := Set V) (⋃ (c : G.ConnectedComponent), c.supp) Set.univ

Tactic:
Set.eq_univ_of_forall fun v ↦ ⟨G.connectedComponentMk v, ?_⟩

Premises used: SimpleGraph.connectedComponentMk, SetLike.coe, Set.eq_univ_of_forall, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
refine :
  ∀ (v : V),
    Membership.mem (γ := Set (Set V)) (Set.range fun (c : G.ConnectedComponent) ↦ c.supp)
        (↑(G.connectedComponentMk v) : Set V) ∧
      v ∈ (↑(G.connectedComponentMk v) : Set V)
⊢ Eq.{u + 1} (α := Set V) (⋃ (c : G.ConnectedComponent), c.supp) Set.univ

Tactic:
refine Set.eq_univ_of_forall fun v ↦ ⟨G.connectedComponentMk v, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ (∃ (y : G.ConnectedComponent), y.supp = (↑(G.connectedComponentMk v) : Set V)) ∧ v ∈ G.connectedComponentMk v

Tactic:
⟨⟨G.connectedComponentMk v, rfl⟩, rfl⟩

Premises used: SimpleGraph.connectedComponentMk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ (∃ (y : G.ConnectedComponent), y.supp = (↑(G.connectedComponentMk v) : Set V)) ∧ v ∈ G.connectedComponentMk v

Tactic:
exact ⟨⟨G.connectedComponentMk v, rfl⟩, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
rw : Nonempty.{u + 1} (G.Walk u v)
⊢ Set.Nonempty.{u} (α := G.Walk u v) Set.univ

Tactic:
rw [← Set.nonempty_iff_univ_nonempty]

Premises used: Set.nonempty_iff_univ_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty.{u + 1} (G.Walk u v)

Tactic:
hconn u v

Premises used: SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty.{u + 1} (G.Walk u v)

Tactic:
exact hconn u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hconn : G.Connected
u v : V
⊢ Set.Nonempty.{u} (α := G.Walk u v) Set.univ

Tactic:
hconn.preconnected.set_univ_walk_nonempty u v

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Preconnected.set_univ_walk_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
have : ∀ (u : V) (huv : u ≠ v), ∃ (u : V), G.Adj v u
⊢ ∃ (u : V), G.Adj v u

Tactic:
have ⟨u, huv⟩ := exists_ne v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v u : V
huv : u ≠ v
have : ∀ (w : G.Walk v u), ∃ (u : V), G.Adj v u
⊢ ∃ (u : V), G.Adj v u

Tactic:
have ⟨w⟩ := h v u
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v u : V
huv : u ≠ v
w : G.Walk v u
⊢ ∃ (u : V), G.Adj v u

Tactic:
⟨_, w.adj_snd <| w.not_nil_of_ne huv.symm⟩

Premises used: Ne.symm, Exists.intro, SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v u : V
huv : u ≠ v
w : G.Walk v u
⊢ ∃ (u : V), G.Adj v u

Tactic:
exact ⟨_, w.adj_snd <| w.not_nil_of_ne huv.symm⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
G : SimpleGraph V
e : Sym2 V
⊢ ∀ (a₁ a₂ : V),
    Eq (α := Prop) ((fun (v w : V) ↦ ¬(G.deleteEdges {e}).Reachable v w) a₁ a₂)
      ((fun (v w : V) ↦ ¬(G.deleteEdges {e}).Reachable v w) a₂ a₁)

Tactic:
simp [reachable_comm]

Premises used: SimpleGraph.reachable_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G.deleteEdges {s(u, v)}).Reachable u v

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.IsBridge, Sym2.fromRel, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : ¬G.Reachable u v
h : G.Adj u v
⊢ G.IsBridge s(u, v)

Tactic:
⟨h, fun h ↦ huv <| h.mono <| deleteEdges_le _⟩

Premises used: Sym2.mk, SimpleGraph.IsBridge, SimpleGraph.Reachable.mono, And.intro, Singleton.singleton, SimpleGraph.deleteEdges_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
he : G.IsBridge e
h : ∀ (u v : V) (he : G.IsBridge s(u, v)), Nontrivial V
⊢ Nontrivial V

Tactic:
cases e with | h u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u : V
he : G.IsBridge s(u, u)
⊢ False

Tactic:
simp [IsBridge] at he

Premises used: SimpleGraph.IsBridge
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
he : G.IsBridge s(u, v)
⊢ Nontrivial V

Tactic:
exact ⟨u, v, by rintro rfl; simp [IsBridge] at he⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
mp : (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges
mpr : (∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ G.deleteEdges {s(v, w)} ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
h :
  s(v, w) ∉
    Walk.edges (u := v') (v := w')
      (Walk.map (Hom.ofLE ⋯) p : G.Walk ((Hom.ofLE ⋯ : (a : V) → V) v') ((Hom.ofLE ⋯ : (a : V) → V) w'))
⊢ ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges

Tactic:
use p.map (.ofLE (by simp))

Premises used: SimpleGraph.Walk.map, SimpleGraph.Hom.ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
h : ¬∃ a ∈ p.edges, a = s(v, w)
⊢ s(v, w) ∉
    Walk.edges (u := v') (v := w')
      (Walk.map (Hom.ofLE ⋯) p : G.Walk ((Hom.ofLE ⋯ : (a : V) → V) v') ((Hom.ofLE ⋯ : (a : V) → V) w'))

Tactic:
simp_rw [Walk.edges_map, List.mem_map, Hom.ofLE_apply, Sym2.map_id', id]

Premises used: Sym2.map_id', id, SimpleGraph.Walk.edges_map, List.mem_map, SimpleGraph.Hom.ofLE_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
h : s(v, w) ∈ p.edges
⊢ False

Tactic:
simpa using p.edges_subset_edgeSet h

Premises used: SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w'

Tactic:
⟨p.transfer _ fun e ep => ?_⟩

Premises used: Nonempty.intro, SimpleGraph.Walk.transfer, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
mpr : ∀ (e : Sym2 V) (ep : e ∈ p.edges), e ∈ (G.deleteEdges {s(v, w)}).edgeSet
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w'

Tactic:
refine ⟨p.transfer _ fun e ep => ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
mpr : e ∈ G.edgeSet \ {s(v, w)}
⊢ e ∈ (G.deleteEdges {s(v, w)}).edgeSet

Tactic:
rw [edgeSet_deleteEdges]

Premises used: SimpleGraph.edgeSet_deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ G.edgeSet \ {s(v, w)}

Tactic:
⟨p.edges_subset_edgeSet ep, fun h' => h (h' ▸ ep)⟩

Premises used: Set.Mem, Set.diff, setOf, Eq.rec, And.intro, SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ G.edgeSet \ {s(v, w)}

Tactic:
exact ⟨p.edges_subset_edgeSet ep, fun h' => h (h' ▸ ep)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
rw : ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

Tactic:
rw [isBridge_iff, and_congr_right']

Premises used: and_congr_right', SimpleGraph.isBridge_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
rw : (¬∃ (p : G.Walk v w), s(v, w) ∉ p.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
rw₁ rw₂ : (∀ (x : G.Walk v w), s(v, w) ∈ x.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

Tactic:
rw [reachable_deleteEdges_iff_exists_walk, not_exists_not]

Premises used: SimpleGraph.reachable_deleteEdges_iff_exists_walk, Classical.not_exists_not
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
⊢ v ∈ c.support

Tactic:
have hv := c.fst_mem_support_of_mem_edges he
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
⊢ c = (puw.append pwv).append pvu

Tactic:
simp [puw, pwv, pvu]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
⊢ c = (puw.append pwv).append pvu

Tactic:
have : c = (puw.append pwv).append pvu := by simp [puw, pwv, pvu]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
⊢ s(v, w) ∈ (pvu.append puw).edges

Tactic:
have hbq := hb (pvu.append puw)
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
⊢ s(v, w) ∈ pwv.reverse.edges

Tactic:
have hpq' := hb pwv.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.reverse.edges
⊢ s(v, w) ∈ pwv.edges

Tactic:
rw [Walk.edges_reverse, List.mem_reverse] at hpq'

Premises used: List.mem_reverse, SimpleGraph.Walk.edges_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ s(v, w) ∈ c.edges

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
⊢ w ∈ (c.takeUntil v ⋯).support

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
hw₁ : w ∈ (c.takeUntil v ⋯).support
⊢ v ∈ c.support

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
hw₁ : w ∈ (c.takeUntil v ⋯).support
hv₁ : v ∈ c.support
⊢ let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  ((pvu.append puw).edges ++ pwv.edges).Nodup

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
hw₁ : w ∈ (c.takeUntil v ⋯).support
hv₁ : v ∈ c.support
hc₁ :
  let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  ((pvu.append puw).edges ++ pwv.edges).Nodup
⊢ let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  c = (puw.append pwv).append pvu

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
hw₁ : w ∈ (c.takeUntil v ⋯).support
hv₁ : v ∈ c.support
hc₁ :
  let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  ((pvu.append puw).edges ++ pwv.edges).Nodup
this₁ :
  let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  c = (puw.append pwv).append pvu
⊢ let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  s(v, w) ∈ (pvu.append puw).edges

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
he₁ : s(v, w) ∈ c.edges
hw₁ : w ∈ (c.takeUntil v ⋯).support
hv₁ : v ∈ c.support
hc₁ :
  let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  ((pvu.append puw).edges ++ pwv.edges).Nodup
this₁ :
  let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  c = (puw.append pwv).append pvu
hbq₁ :
  let puw := (c.takeUntil v hv₁).takeUntil w hw₁;
  let pvu := c.dropUntil v hv₁;
  s(v, w) ∈ (pvu.append puw).edges
⊢ let pwv := (c.takeUntil v hv₁).dropUntil w hw₁;
  s(v, w) ∈ pwv.edges

Tactic:
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
    ← List.append_assoc, ← Walk.edges_append] at hc

Premises used: List.append_assoc, SimpleGraph.Walk.isTrail_def, List.nodup_append_comm, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
hc : ((pvu.append puw).edges ++ pwv.edges).Nodup
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False

Tactic:
List.disjoint_of_nodup_append hc hbq hpq'

Premises used: List.disjoint_of_nodup_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
hc : ((pvu.append puw).edges ++ pwv.edges).Nodup
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False

Tactic:
exact List.disjoint_of_nodup_append hc hbq hpq'

Premises used: List.disjoint_of_nodup_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
rw : (G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges) ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
⊢ G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
rw [reachable_deleteEdges_iff_exists_walk]

Premises used: SimpleGraph.reachable_deleteEdges_iff_exists_walk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
mp : (G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges) → ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges
mpr : (∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges
⊢ (G.Adj v w ∧ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges) ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.toPath, SimpleGraph.Walk.cons, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
mp : (Walk.cons ⋯ (↑p.toPath : G.Walk v w)).IsCycle
mp₁ : s(v, w) ∈ (Walk.cons ⋯ (↑p.toPath : G.Walk v w)).edges
⊢ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
mp : s(w, v) ∉ (↑p.toPath : G.Walk v w).edges
⊢ (Walk.cons ⋯ (↑p.toPath : G.Walk v w)).IsCycle

Tactic:
apply Path.cons_isCycle

Premises used: SimpleGraph.Path.cons_isCycle