awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
nil : ∀ {u : V} (p' : G.Walk u w), (append Walk.nil p').darts = darts (u := u) Walk.nil ++ p'.darts
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (p' : G.Walk w_1 w), (p.append p').darts = p.darts ++ p'.darts) →
      ∀ (p' : G.Walk w_1 w), ((Walk.cons h p).append p').darts = (Walk.cons h p).darts ++ p'.darts
⊢ (p.append p').darts = p.darts ++ p'.darts

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
p' : G.Walk u_1 w
⊢ (append nil p').darts = darts (u := u_1) nil ++ p'.darts

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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 : ∀ (p' : G.Walk w_1 w), (p.append p').darts = p.darts ++ p'.darts
p' : G.Walk w_1 w
⊢ ((cons h p).append p').darts = (cons h p).darts ++ p'.darts

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Eq.{u + 1} (α := List G.Dart) (darts (u := u) (reverse Walk.nil))
      (List.reverse (List.map Dart.symm (darts (u := u) Walk.nil)))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    p.reverse.darts = (List.map Dart.symm p.darts).reverse →
      (Walk.cons h p).reverse.darts = (List.map Dart.symm (Walk.cons h p).darts).reverse
⊢ p.reverse.darts = (List.map Dart.symm p.darts).reverse

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (reverse nil))
    (List.reverse (List.map Dart.symm (darts (u := u_1) nil)))

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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
p_ih : p.reverse.darts = (List.map Dart.symm p.darts).reverse
⊢ (cons h p).reverse.darts = (List.map Dart.symm (cons h p).darts).reverse

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
d : G.Dart
p : G.Walk u v
⊢ d ∈ p.reverse.darts ↔ d.symm ∈ p.darts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 w u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ u = (p.darts.head ⋯).toProd.1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 w u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ v = (p.darts.getLast ⋯).toProd.2

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp_1 : ¬p.Nil
hp : ¬Nil.{u} (V := V) (G := G) (v := u) nil
⊢ ofDarts (darts (u := u) nil) ⋯ ⋯ = Walk.copy nil ⋯ ⋯

Tactic:
simp at hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
h : G.Adj u w
h_1 : ¬(cons h nil).Nil
⊢ ofDarts (cons h nil).darts ⋯ ⋯ = (cons h nil).copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
hp : ¬p_1.Nil
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
h : ¬(cons h₁ (cons h₂ p)).Nil
⊢ Eq (α := G.Walk ((cons h₂ p).darts.head ⋯).toProd.1 ((cons h₂ p).darts.getLast ⋯).toProd.2)
    (ofDarts (cons h₂ p).darts ⋯ ⋯ : G.Walk ((cons h₂ p).darts.head ⋯).toProd.1 ((cons h₂ p).darts.getLast ⋯).toProd.2)
    ((cons h₂ p).copy ⋯ ⋯ : G.Walk ((cons h₂ p).darts.head ⋯).toProd.1 ((cons h₂ p).darts.getLast ⋯).toProd.2)

Tactic:
have := p.cons h₂ |>.ofDarts_darts not_nil_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
hp : ¬p_1.Nil
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
h : ¬(cons h₁ (cons h₂ p)).Nil
this :
  Eq (α := G.Walk u' (({ fst := u', snd := v', adj := h₂ : G.Dart } :: p.darts).getLast ⋯).toProd.2)
    (ofDarts ({ fst := u', snd := v', adj := h₂ } :: p.darts) ⋯ ⋯) ((cons h₂ p).copy ⋯ ⋯)
⊢ ofDarts (cons h₁ (cons h₂ p)).darts ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ ofDarts p.darts ⋯ ⋯ = p.copy ⋯ ⋯

Tactic:
match p, hp with
  | nil, hp => simp at hp
  | cons (v := w) h .nil, _ => rfl
  | cons (v := u') h₁ (.cons (v := v') h₂ p), _ =>
    have := p.cons h₂ |>.ofDarts_darts not_nil_cons
    simp at this
    simp [this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).edges = p.edges.concat s(v, w)

Tactic:
simp [edges]

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
subst_vars : ∀ (p : G.Walk u' v'), (p.copy ⋯ ⋯).edges = p.edges
⊢ (p.copy hu hv).edges = p.edges

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).edges = p.edges

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').edges = p.edges ++ p'.edges

Tactic:
simp [edges]

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.edges = p.edges.reverse

Tactic:
simp [edges]

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
h : d ∈ p.darts
⊢ d.symm ∈ p.reverse.darts

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
h : d ∈ p.darts
⊢ d.toProd.2 ∈ p.support

Tactic:
simpa using p.reverse.dart_fst_mem_support_of_mem_darts (by simp [h] : d.symm ∈ p.reverse.darts)

Premises used: SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts, SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
obtain : ∀ (d : G.Dart) (hd : d ∈ p.darts) (he : d.edge = s(t, u)), t ∈ p.support
⊢ t ∈ p.support

Tactic:
obtain ⟨d, hd, he⟩ := List.mem_map.mp he

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he_1 : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.edge = s(t, u)
⊢ d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t

Tactic:
rw [dart_edge_eq_mk'_iff'] at he

Premises used: SimpleGraph.dart_edge_eq_mk'_iff'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he_1 : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
inl : ∀ (he : s(d.toProd.1, d.toProd.2) ∈ p.edges), d.toProd.1 ∈ p.support
inr : ∀ (he : s(d.toProd.2, d.toProd.1) ∈ p.edges), d.toProd.2 ∈ p.support
⊢ t ∈ p.support

Tactic:
rcases he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.1, d.toProd.2) ∈ p.edges
⊢ d.toProd.1 ∈ p.support

Tactic:
dart_fst_mem_support_of_mem_darts _ hd

Premises used: SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.1, d.toProd.2) ∈ p.edges
⊢ d.toProd.1 ∈ p.support

Tactic:
exact dart_fst_mem_support_of_mem_darts _ hd

Premises used: SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.2, d.toProd.1) ∈ p.edges
⊢ d.toProd.2 ∈ p.support

Tactic:
dart_snd_mem_support_of_mem_darts _ hd

Premises used: SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.2, d.toProd.1) ∈ p.edges
⊢ d.toProd.2 ∈ p.support

Tactic:
exact dart_snd_mem_support_of_mem_darts _ hd

Premises used: SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
⊢ u ∈ p.support

Tactic:
p.fst_mem_support_of_mem_edges (Sym2.eq_swap ▸ he)

Premises used: SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
e : Sym2 V
p : G.Walk u v
he : e ∈ p.edges
hv : w ∈ e
⊢ w ∈ p.support

Tactic:
hv.elim fun _ heq ↦ p.fst_mem_support_of_mem_edges <| heq ▸ he

Premises used: SimpleGraph.Walk.fst_mem_support_of_mem_edges, Exists.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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} (α := Sym2 V) (edges (G := G) (u := u_1) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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'.edges.Nodup
h : (Walk.cons h_1 p').support.Nodup
cons : ∀ (h : u_1 ∉ p'.support ∧ p'.support.Nodup), s(u_1, v_1) ∉ p'.edges ∧ p'.edges.Nodup
⊢ (Walk.cons h_1 p').edges.Nodup

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

Premises used: SimpleGraph.Walk.support_cons, List.nodup_cons, SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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'.edges.Nodup
h : u_1 ∉ p'.support ∧ p'.support.Nodup
⊢ s(u_1, v_1) ∉ p'.edges ∧ p'.edges.Nodup

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

Premises used: And.right, And.left, And.intro, SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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'.edges.Nodup
h : u_1 ∉ p'.support ∧ p'.support.Nodup
⊢ s(u_1, v_1) ∉ p'.edges ∧ p'.edges.Nodup

Tactic:
exact ⟨(h.1 <| fst_mem_support_of_mem_edges p' ·), ih h.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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} (α := Sym2 V) (edges (G := G) (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'.edges.Nodup)
    (h_1 : (Walk.cons h p').support.Nodup), (Walk.cons h p').edges.Nodup
⊢ p.edges.Nodup

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

Premises used: SimpleGraph.Walk.support_cons, List.nodup_cons, SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

Tactic:
p.support_reverse ▸ p.support.nodup_tail_reverse ?_

Premises used: List.nodup_tail_reverse, SimpleGraph.Walk.support, Eq.rec, SimpleGraph.Walk.support_reverse, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
refine : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 = p.support.getLast?
⊢ p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

Tactic:
refine p.support_reverse ▸ p.support.nodup_tail_reverse ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ 0 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
rw : p.length + 1 - 1 ≤ p.length
⊢ p.support.length - 1 ≤ p.length

Tactic:
rw [Walk.length_support]

Premises used: SimpleGraph.Walk.length_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.length + 1 - 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
rw : some (p.getVert 0) = some (p.getVert (p.support.length - 1))
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 = p.support.getLast?

Tactic:
rw [← getVert_eq_support_getElem? _ (by lia), List.getLast?_eq_getElem?,
    ← getVert_eq_support_getElem? _ (by rw [Walk.length_support]; lia)]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem?, List.getLast?_eq_getElem?
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ some (p.getVert 0) = some (p.getVert (p.support.length - 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (x : Sym2 V), x ∈ p.reverse.edgeSet ↔ x ∈ p.edgeSet
⊢ p.reverse.edgeSet = p.edgeSet

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x : Sym2 V
⊢ x ∈ p.reverse.edgeSet ↔ x ∈ p.edgeSet

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

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

Tactic:
simp [or_comm]

Premises used: or_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : ∀ (x : Sym2 V), x ∈ (p.append q).edgeSet ↔ x ∈ p.edgeSet ∪ q.edgeSet
⊢ (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
x : Sym2 V
⊢ x ∈ (p.append q).edgeSet ↔ x ∈ p.edgeSet ∪ q.edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ (x : Sym2 V), x ∈ (p.copy hu hv).edgeSet ↔ x ∈ p.edgeSet
⊢ (p.copy hu hv).edgeSet = p.edgeSet

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
x : Sym2 V
⊢ x ∈ (p.copy hu hv).edgeSet ↔ x ∈ p.edgeSet

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

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u w : V
q : G.Walk u w
nil :
  Nil.{u} (V := V) (G := G) (v := u) (append Walk.nil Walk.nil) ↔
    Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ Nil.{u} (V := V) (G := G) (v := u) Walk.nil
nil₁ :
  ∀ {v : V} (h : G.Adj u v) (p : G.Walk v w),
    (append Walk.nil (cons h p)).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ (cons h p).Nil
⊢ (append Walk.nil q).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ q.Nil

Tactic:
cases q
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
cons : ((Walk.cons h p).append nil).Nil ↔ (Walk.cons h p).Nil ∧ Nil.{u} (V := V) (G := G) (v := v) nil
cons₁ :
  ∀ {v_2 : V} (h_1 : G.Adj v v_2) (p_1 : G.Walk v_2 w),
    ((Walk.cons h p).append (Walk.cons h_1 p_1)).Nil ↔ (Walk.cons h p).Nil ∧ (Walk.cons h_1 p_1).Nil
⊢ ((Walk.cons h p).append q).Nil ↔ (Walk.cons h p).Nil ∧ q.Nil

Tactic:
cases q
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Nil.{u} (V := V) (G := G) (v := u) (append nil nil) ↔
    Nil.{u} (V := V) (G := G) (v := u) nil ∧ Nil.{u} (V := V) (G := G) (v := u) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u w v : V
h : G.Adj u v
p : G.Walk v w
⊢ (append nil (cons h p)).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) nil ∧ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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).append nil).Nil ↔ (cons h p).Nil ∧ Nil.{u} (V := V) (G := G) (v := v) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
v_2 : V
h_1 : G.Adj v v_2
p_1 : G.Walk v_2 w
⊢ ((cons h p).append (cons h_1 p_1)).Nil ↔ (cons h p).Nil ∧ (cons h_1 p_1).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hp : p.Nil
hq : q.Nil
⊢ (p.append q).Nil

Tactic:
simp [hp, hq]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : Nil.{u} (V := V) (G := G) (v := v) (reverse 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).reverse.Nil ↔ (Walk.cons h p).Nil
⊢ p.reverse.Nil ↔ p.Nil

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

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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).reverse.Nil ↔ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) =
      length.{u} (V := V) (G := G) (u := u) Walk.nil - n
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (p.drop n).length = p.length - n) →
      ∀ (n : ℕ), ((Walk.cons h p).drop n).length = (Walk.cons h p).length - n
⊢ (p.drop n).length = p.length - n

Tactic:
induction p generalizing n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0) =
    length.{u} (V := V) (G := G) (u := u_1) Walk.nil - 0
nil₁ :
  ∀ (n : ℕ),
    length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)) =
      length.{u} (V := V) (G := G) (u := u_1) Walk.nil - (n + 1)
⊢ length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n) =
    length.{u} (V := V) (G := G) (u := u_1) Walk.nil - n

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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
p_ih : ∀ (n : ℕ), (p.drop n).length = p.length - n
n : ℕ
cons : length (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) = (Walk.cons h p).length - 0
cons₁ :
  ∀ (n : ℕ),
    length (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) = (Walk.cons h p).length - (n + 1)
⊢ ((Walk.cons h p).drop n).length = (Walk.cons h p).length - n

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0) =
    length.{u} (V := V) (G := G) (u := u_1) nil - 0

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) nil (n + 1)) (drop nil (n + 1)) =
    length.{u} (V := V) (G := G) (u := u_1) nil - (n + 1)

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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
p_ih : ∀ (n : ℕ), (p.drop n).length = p.length - n
⊢ length (u := (cons h p).getVert 0) ((cons h p).drop 0) = (cons h p).length - 0

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
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
p_ih : ∀ (n : ℕ), (p.drop n).length = p.length - n
n : ℕ
⊢ length (u := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) = (cons h p).length - (n + 1)

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) m)
      (getVert (G := G) (u := u) Walk.nil (n + m))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (p.drop n).getVert m = p.getVert (n + m)) →
      ∀ (n : ℕ), ((Walk.cons h p).drop n).getVert m = (Walk.cons h p).getVert (n + m)
⊢ (p.drop n).getVert m = p.getVert (n + m)

Tactic:
induction p generalizing n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0) m)
    (getVert (G := G) (u := u_1) Walk.nil (0 + m))
nil₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)) m)
      (getVert (G := G) (u := u_1) Walk.nil (n + 1 + m))
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n) m)
    (getVert (G := G) (u := u_1) Walk.nil (n + m))

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.drop n).getVert m = p.getVert (n + m)
n : ℕ
cons : getVert (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) m = (Walk.cons h p).getVert (0 + m)
cons₁ :
  ∀ (n : ℕ),
    getVert (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) m =
      (Walk.cons h p).getVert (n + 1 + m)
⊢ ((Walk.cons h p).drop n).getVert m = (Walk.cons h p).getVert (n + m)

Tactic:
cases n