awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
⊢ { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 = u ∨
    { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 ∈ p'.support

Tactic:
.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
⊢ { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 = u ∨
    { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 ∈ p'.support

Tactic:
exact .inl rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
.inr (dart_fst_mem_support_of_mem_darts _ hd)

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
exact .inr (dart_fst_mem_support_of_mem_darts _ hd)
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w ↔
      w = u ∨ ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e ∧ w ∈ e
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (w ∈ p.support ↔ w = w_1 ∨ ∃ e ∈ p.edges, w ∈ e) →
      (w ∈ (Walk.cons h p).support ↔ w = w_1 ∨ ∃ e ∈ (Walk.cons h p).edges, w ∈ e)
⊢ w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) w ↔
    w = u_1 ∨ ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e ∧ w ∈ e

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : w ∈ p.support ↔ w = w_1 ∨ ∃ e ∈ p.edges, w ∈ e
⊢ w ∈ (cons h p).support ↔ w = w_1 ∨ ∃ e ∈ (cons h p).edges, w ∈ e

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
h : List.Nodup.{u} (α := V) (support (G := G) (u := u_1) nil)
⊢ List.Nodup.{u} (α := G.Dart) (darts (u := u_1) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : ∀ (h : p'.support.Nodup), p'.darts.Nodup
h : (Walk.cons h_1 p').support.Nodup
cons :
  ∀ (h : u_1 ∉ p'.support ∧ p'.support.Nodup),
    { fst := u_1, snd := v_1, adj := h_1 : G.Dart } ∉ p'.darts ∧ p'.darts.Nodup
⊢ (Walk.cons h_1 p').darts.Nodup

Tactic:
simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢

Premises used: SimpleGraph.Walk.support_cons, List.nodup_cons, SimpleGraph.Walk.darts_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : ∀ (h : p'.support.Nodup), p'.darts.Nodup
h : u_1 ∉ p'.support ∧ p'.support.Nodup
⊢ { fst := u_1, snd := v_1, adj := h_1 : G.Dart } ∉ p'.darts ∧ p'.darts.Nodup

Tactic:
⟨(h.1 <| dart_fst_mem_support_of_mem_darts p' ·), ih h.2⟩

Premises used: SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : ∀ (h : p'.support.Nodup), p'.darts.Nodup
h : u_1 ∉ p'.support ∧ p'.support.Nodup
⊢ { fst := u_1, snd := v_1, adj := h_1 : G.Dart } ∉ p'.darts ∧ p'.darts.Nodup

Tactic:
exact ⟨(h.1 <| dart_fst_mem_support_of_mem_darts p' ·), ih h.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
nil :
  ∀ {u : V} (h : List.Nodup.{u} (α := V) (support (G := G) (u := u) Walk.nil)),
    List.Nodup.{u} (α := G.Dart) (darts (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w) (ih : ∀ (h : p'.support.Nodup), p'.darts.Nodup)
    (h_1 : (Walk.cons h p').support.Nodup), (Walk.cons h p').darts.Nodup
⊢ p.darts.Nodup

Tactic:
induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
    exact ⟨(h.1 <| dart_fst_mem_support_of_mem_darts p' ·), ih h.2⟩

Premises used: SimpleGraph.Walk.support_cons, List.nodup_cons, SimpleGraph.Walk.cons, SimpleGraph.Walk.darts_cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u_1) nil)
    (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := u_1) nil)
      (List.tail (support (G := G) (u := u_1) nil)))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p'.support p'.support.tail
cons :
  ∀
    (ih :
      Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v_1) nil)
        (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := v_1) nil)
          (List.tail (support (G := G) (u := v_1) nil)))),
    (Walk.cons h nil).edges =
      List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h nil).support (Walk.cons h nil).support.tail
cons₁ :
  ∀ {v : V} (h_1 : G.Adj v_1 v) (p : G.Walk v w)
    (ih :
      (Walk.cons h_1 p).edges =
        List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h_1 p).support (Walk.cons h_1 p).support.tail),
    (Walk.cons h (Walk.cons h_1 p)).edges =
      List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h (Walk.cons h_1 p)).support
        (Walk.cons h (Walk.cons h_1 p)).support.tail
⊢ (Walk.cons h p').edges =
    List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h p').support (Walk.cons h p').support.tail

Tactic:
cases p'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 : V
h : G.Adj u_1 v_1
ih :
  Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v_1) nil)
    (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := v_1) nil)
      (List.tail (support (G := G) (u := v_1) nil)))
⊢ (cons h nil).edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (cons h nil).support (cons h nil).support.tail

Tactic:
simp [edges_cons, ih]

Premises used: SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
v_2 : V
h_1 : G.Adj v_1 v_2
p : G.Walk v_2 w
ih : (cons h_1 p).edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (cons h_1 p).support (cons h_1 p).support.tail
⊢ (cons h (cons h_1 p)).edges =
    List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (cons h (cons h_1 p)).support (cons h (cons h_1 p)).support.tail

Tactic:
simp [edges_cons, ih]

Premises used: SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil)
      (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := u) Walk.nil)
        (List.tail (support (G := G) (u := u) Walk.nil)))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w)
    (ih : p'.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p'.support p'.support.tail),
    (Walk.cons h p').edges =
      List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h p').support (Walk.cons h p').support.tail
⊢ p.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p.support p.support.tail

Tactic:
induction p with
  | nil => simp
  | cons _ p' ih => cases p' <;> simp [edges_cons, ih]

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v u v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 u
h : edges (G := G) (u := u) nil = (cons h_1 p).edges
⊢ nil = cons h_1 p

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v u v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 u
h : (cons h_1 p).edges = edges (G := G) (u := u) nil
⊢ cons h_1 p = nil

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u u
w₂ : G.Walk u c
h : (cons' u v c h₁ w₁).edges = (cons' u u c h₂ w₂).edges
⊢ False

Tactic:
G.loopless.irrefl _ h₂

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u u
w₂ : G.Walk u c
h : (cons' u v c h₁ w₁).edges = (cons' u u c h₂ w₂).edges
⊢ False

Tactic:
exact G.loopless.irrefl _ h₂

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
⊢ u ≠ v'

Tactic:
have h₃ : u ≠ v' := by rintro rfl; exact G.loopless.irrefl _ h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
h₃ : u ≠ v'
⊢ v = v' ∧ w₁.edges = w₂.edges

Tactic:
simpa [h₁, h₃] using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
h₃ : u ≠ v'
obtain :
  ∀ (h₂ : G.Adj u v) (w₂ : G.Walk v c) (h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₂).edges) (h₃ : u ≠ v)
    (h₃ : w₁.edges = w₂.edges), cons' u v c h₁ w₁ = cons' u v c h₂ w₂
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂

Tactic:
obtain ⟨rfl, h₃⟩ : v = v' ∧ w₁.edges = w₂.edges := by simpa [h₁, h₃] using h

Premises used: rfl, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u v
w₂ : G.Walk v c
h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₂).edges
h₃_1 : u ≠ v
h₃ : w₁.edges = w₂.edges
rw rw₁ : cons' u v c h₁ w₂ = cons' u v c h₂ w₂
⊢ cons' u v c h₁ w₁ = cons' u v c h₂ w₂

Tactic:
rw [edges_injective h₃]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ Function.Injective.{u + 1, u + 1} (α := G.Walk u v) darts

Tactic:
edges_injective.of_comp

Premises used: SimpleGraph.Walk.edges_injective, Function.Injective.of_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
e : Sym2 V
⊢ e ∈ p.edgeSet ↔ e ∈ p.edges

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.Walk.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
h :
  ∀ (x : Sym2 V),
    Membership.mem (γ := Set (Sym2 V)) (edgeSet (G := G) (u := u) nil) x ↔ Membership.mem (γ := Set (Sym2 V)) ∅ x
⊢ Eq.{u + 1} (α := Set (Sym2 V)) (edgeSet (G := G) (u := u) nil) ∅

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
x : Sym2 V
⊢ Membership.mem (γ := Set (Sym2 V)) (edgeSet (G := G) (u := u) nil) x ↔ Membership.mem (γ := Set (Sym2 V)) ∅ x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
h₁ : ∀ (x : Sym2 V), x ∈ (cons h p).edgeSet ↔ x ∈ insert s(u, v) p.edgeSet
⊢ (cons h p).edgeSet = insert s(u, v) p.edgeSet

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
x : Sym2 V
⊢ x ∈ (cons h p).edgeSet ↔ x ∈ insert s(u, v) p.edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ (↑p.edges.toFinset : Set (Sym2 V)) = p.edgeSet

Tactic:
simp [edgeSet]

Premises used: SimpleGraph.Walk.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Nil.{u} (V := V) (G := G) (v := u) nil

Tactic:
Nil.nil

Premises used: SimpleGraph.Walk.Nil.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ ¬(cons h p).Nil

Tactic:
nofun

Premises used: False, _private.0.SimpleGraph.Walk.not_nil_cons.match_1, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ v ≠ w → ¬p.Nil

Tactic:
mt Nil.eq

Premises used: mt, SimpleGraph.Walk.Nil.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : Nil.{u} (V := V) (G := G) (v := v) Walk.nil ↔ support (G := G) (u := v) Walk.nil = [v]
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (Walk.cons h p).Nil ↔ (Walk.cons h p).support = [v]
⊢ p.Nil ↔ p.support = [v]

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Nil.{u} (V := V) (G := G) (v := v) nil ↔ support (G := G) (u := v) nil = [v]

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w v_1 : V
h : G.Adj v v_1
p : G.Walk v_1 w
⊢ (cons h p).Nil ↔ (cons h p).support = [v]

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : Eq.{u + 1} (α := List G.Dart) (darts (u := v) Walk.nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (Walk.cons h p).darts = [] ↔ (Walk.cons h p).Nil
⊢ p.darts = [] ↔ p.Nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := v) nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w v_1 : V
h : G.Adj v v_1
p : G.Walk v_1 w
⊢ (cons h p).darts = [] ↔ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil :
  Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v) Walk.nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (Walk.cons h p).edges = [] ↔ (Walk.cons h p).Nil
⊢ p.edges = [] ↔ p.Nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v) nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w v_1 : V
h : G.Adj v v_1
p : G.Walk v_1 w
⊢ (cons h p).edges = [] ↔ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : length.{u} (V := V) (G := G) (u := u) Walk.nil = 0 ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).length = 0 ↔ (Walk.cons h p).Nil
⊢ p.length = 0 ↔ p.Nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ length.{u} (V := V) (G := G) (u := u) nil = 0 ↔ Nil.{u} (V := V) (G := G) (v := u) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).length = 0 ↔ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.Nil ↔ p.length = 0

Tactic:
length_eq_zero_iff.symm

Premises used: Iff.symm, SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : ¬Nil.{u} (V := V) (G := G) (v := v) Walk.nil ↔ 0 < length.{u} (V := V) (G := G) (u := v) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), ¬(Walk.cons h p).Nil ↔ 0 < (Walk.cons h p).length
⊢ ¬p.Nil ↔ 0 < p.length

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ ¬Nil.{u} (V := V) (G := G) (v := v) nil ↔ 0 < length.{u} (V := V) (G := G) (u := v) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w v_1 : V
h : G.Adj v v_1
p : G.Walk v_1 w
⊢ ¬(cons h p).Nil ↔ 0 < (cons h p).length

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil :
  ¬Nil.{u} (V := V) (G := G) (v := v) Walk.nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u v), Walk.nil = Walk.cons h q
cons :
  ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w),
    ¬(Walk.cons h p).Nil ↔ ∃ (u : V) (h_1 : G.Adj v u) (q : G.Walk u w), Walk.cons h p = Walk.cons h_1 q
⊢ ¬p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = Walk.cons h q

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ ¬Nil.{u} (V := V) (G := G) (v := v) nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u v), nil = cons h q

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w v_1 : V
h : G.Adj v v_1
p : G.Walk v_1 w
⊢ ¬(cons h p).Nil ↔ ∃ (u : V) (h_1 : G.Adj v u) (q : G.Walk u w), cons h p = cons h_1 q

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
nil : Eq.{u + 1} (α := G.Walk v v) Walk.nil Walk.nil ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 v), Walk.cons h p = Walk.nil ↔ (Walk.cons h p).Nil
⊢ p = Walk.nil ↔ p.Nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Eq.{u + 1} (α := G.Walk v v) nil nil ↔ Nil.{u} (V := V) (G := G) (v := v) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v v_1 : V
h : G.Adj v v_1
p : G.Walk v_1 v
⊢ cons h p = nil ↔ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
⊢ p.Nil ↔ p = nil

Tactic:
eq_nil_iff_nil.symm

Premises used: SimpleGraph.Walk.eq_nil_iff_nil, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : Subsingleton V
p : G.Walk v w
⊢ p.Nil

Tactic:
match p with
  | nil => Nil.nil
  | cons h w => Unique.eq_default G ▸ h |>.elim

Premises used: _private.0.SimpleGraph.Walk.isChain_adj_cons_support.match_1, SimpleGraph.Walk.Nil.nil, SimpleGraph.Walk.Nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ (∃ (p : G.Walk u v), p.Nil) ↔ u = v

Tactic:
⟨fun ⟨_, h⟩ ↦ h.eq, (· ▸ ⟨nil, .nil⟩)⟩

Premises used: Eq.rec, SimpleGraph.Walk.Nil.nil, SimpleGraph.Walk.Nil.eq, _private.0.SimpleGraph.Walk.exists_nil_iff.match_1, SimpleGraph.Walk.nil, Iff.intro, Exists.intro, Eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1
cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (Walk.cons h q) ⋯
h' : G.Adj u v
q' : G.Walk v w
⊢ notNilRec (motive := @motive) (fun {u v w : V} ↦ cons) (Walk.cons h' q') ⋯ = cons h' q'

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), w ∈ (cons h q).support.tail

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
hnil : ¬Nil.{u} (V := V) (G := G) (v := u_1) nil
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) w ↔
    ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e ∧ w ∈ e

Tactic:
simp at hnil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ (hnil : ¬p.Nil), w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e
hnil : ¬(Walk.cons h p).Nil
cons :
  ∀
    (ih :
      ∀ (hnil : ¬Nil.{u} (V := V) (G := G) (v := v_1) nil),
        Membership.mem (γ := List V) (support (G := G) (u := v_1) nil) w ↔
          ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := v_1) nil) e ∧ w ∈ e)
    (hnil : ¬(Walk.cons h nil).Nil), w ∈ (Walk.cons h nil).support ↔ ∃ e ∈ (Walk.cons h nil).edges, w ∈ e
cons₁ :
  ∀ {v : V} (h_1 : G.Adj v_1 v) (p : G.Walk v w_1)
    (ih : ∀ (hnil : ¬(Walk.cons h_1 p).Nil), w ∈ (Walk.cons h_1 p).support ↔ ∃ e ∈ (Walk.cons h_1 p).edges, w ∈ e)
    (hnil : ¬(Walk.cons h (Walk.cons h_1 p)).Nil),
    w ∈ (Walk.cons h (Walk.cons h_1 p)).support ↔ ∃ e ∈ (Walk.cons h (Walk.cons h_1 p)).edges, w ∈ e
⊢ w ∈ (Walk.cons h p).support ↔ ∃ e ∈ (Walk.cons h p).edges, w ∈ e

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 : V
h : G.Adj u_1 v_1
ih :
  ∀ (hnil : ¬Nil.{u} (V := V) (G := G) (v := v_1) nil),
    Membership.mem (γ := List V) (support (G := G) (u := v_1) nil) w ↔
      ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := v_1) nil) e ∧ w ∈ e
hnil : ¬(cons h nil).Nil
⊢ w ∈ (cons h nil).support ↔ ∃ e ∈ (cons h nil).edges, w ∈ e

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
v_2 : V
h_1 : G.Adj v_1 v_2
p : G.Walk v_2 w_1
ih : ∀ (hnil : ¬(cons h_1 p).Nil), w ∈ (cons h_1 p).support ↔ ∃ e ∈ (cons h_1 p).edges, w ∈ e
hnil : ¬(cons h (cons h_1 p)).Nil
⊢ w ∈ (cons h (cons h_1 p)).support ↔ ∃ e ∈ (cons h (cons h_1 p)).edges, w ∈ e

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hnil : ¬p.Nil
nil :
  ∀ {u : V} (hnil : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil),
    Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w ↔
      ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e ∧ w ∈ e
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1) (ih : ∀ (hnil : ¬p.Nil), w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e)
    (hnil : ¬(Walk.cons h p).Nil), w ∈ (Walk.cons h p).support ↔ ∃ e ∈ (Walk.cons h p).edges, w ∈ e
⊢ w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e

Tactic:
induction p with
  | nil => simp at hnil
  | cons h p ih => cases p <;> aesop

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u_1 : V
uS : u_1 ∈ S
vS : u_1 ∉ S
⊢ ∃ (d : G.Dart), Membership.mem (γ := List G.Dart) (darts (u := u_1) nil) d ∧ d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
cases vS uS
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u_1 x w : V
a : G.Adj u_1 x
p' : G.Walk x w
ih : ∀ (uS : x ∈ S) (vS : w ∉ S), ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u_1 ∈ S
vS : w ∉ S
pos : ∀ (h : x ∈ S), ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
neg : ∀ (h : x ∉ S), ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
by_cases h : x ∈ S