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 v' w'
h : G.Adj u v'
⊢ cons h (p.copy ⋯ ⋯) = Walk.copy (cons ⋯ p) ⋯ ⋯

Tactic:
rfl
-- 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 = p.append (cons h nil)

Tactic:
rfl

Premises used: SimpleGraph.Walk.concat, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
h : G.Adj u v
p : G.Walk v w
q : G.Walk w x
⊢ (cons h p).append q = cons h (p.append q)

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h nil).append p = cons h p

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ append nil p = p

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.append
-- 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} (α := G.Walk u u) (append Walk.nil Walk.nil) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    p.append Walk.nil = p → (Walk.cons h p).append Walk.nil = Walk.cons h p
⊢ p.append Walk.nil = p

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := G.Walk u_1 u_1) (append nil nil) 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.append nil = p
⊢ (cons h p).append nil = cons h p

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk w x
nil : ∀ {u : V} (q : G.Walk u w), append Walk.nil (q.append r) = (append Walk.nil q).append r
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 w), p.append (q.append r) = (p.append q).append r) →
      ∀ (q : G.Walk w_1 w), (Walk.cons h p).append (q.append r) = ((Walk.cons h p).append q).append r
⊢ p.append (q.append r) = (p.append q).append r

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

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (q : G.Walk w_1 w), p.append (q.append r) = (p.append q).append r
q : G.Walk w_1 w
⊢ (cons h p).append (q.append r) = ((cons h p).append q).append r

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u' v' w' : V
p : G.Walk u v
q : G.Walk v w
hu : u = u'
hv : v = v'
hw : w = w'
subst_vars : ∀ (p : G.Walk u' v') (q : G.Walk v' w'), (p.copy ⋯ ⋯).append (q.copy ⋯ ⋯) = (p.append q).copy ⋯ ⋯
⊢ (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw

Tactic:
subst_vars
-- 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'
⊢ (p.copy ⋯ ⋯).append (q.copy ⋯ ⋯) = (p.append q).copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ concat nil h = cons h nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.concat, rfl, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
h : G.Adj u v
p : G.Walk v w
h' : G.Adj w x
⊢ (cons h p).concat h' = cons h (p.concat h')

Tactic:
rfl

Premises used: SimpleGraph.Walk.concat, rfl, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
h : G.Adj w x
⊢ p.append (q.concat h) = (p.append q).concat h

Tactic:
append_assoc _ _ _

Premises used: SimpleGraph.Walk.concat, SimpleGraph.Walk.append_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
rw : (p.append (cons h nil)).append q = p.append (cons h q)
rw₁ : p.append ((cons h nil).append q) = p.append (cons h q)
rw₂ rw₃ : p.append (cons h q) = p.append (cons h q)
⊢ (p.concat h).append q = p.append (cons h q)

Tactic:
rw [concat_eq_append, ← append_assoc, cons_nil_append]

Premises used: SimpleGraph.Walk.concat_eq_append, SimpleGraph.Walk.cons_nil_append, SimpleGraph.Walk.append_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w u_1 u : V
h : G.Adj u u_1
⊢ ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x u_1), cons h nil = q.concat h'

Tactic:
⟨_, nil, h, rfl⟩

Premises used: SimpleGraph.Walk.nil, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w u_1 u : V
h : G.Adj u u_1
⊢ ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x u_1), cons h nil = q.concat h'

Tactic:
exact ⟨_, nil, h, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w u_1 v_1 w_1 : V
h' : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {u : V} (h : G.Adj u v_1), ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w_1), Walk.cons h p = q.concat h'
u : V
h : G.Adj u u_1
cons :
  ∀ (y : V) (q : G.Walk u_1 y) (h'' : G.Adj y w_1) (hc : Walk.cons h' p = q.concat h''),
    ∃ (x : V) (q : G.Walk u x) (h'_1 : G.Adj x w_1), Walk.cons h (Walk.cons h' p) = q.concat h'_1
⊢ ∃ (x : V) (q : G.Walk u x) (h'_1 : G.Adj x w_1), Walk.cons h (Walk.cons h' p) = q.concat h'_1

Tactic:
obtain ⟨y, q, h'', hc⟩ := ih h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w u_1 v_1 w_1 : V
h' : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {u : V} (h : G.Adj u v_1), ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w_1), cons h p = q.concat h'
u : V
h : G.Adj u u_1
y : V
q : G.Walk u_1 y
h'' : G.Adj y w_1
hc : cons h' p = q.concat h''
⊢ ∃ (x : V) (q : G.Walk u x) (h'_1 : G.Adj x w_1), cons h (cons h' p) = q.concat h'_1

Tactic:
⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩

Premises used: Eq.rec, SimpleGraph.Walk.cons, Exists.intro, SimpleGraph.Walk.concat_cons, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w u_1 v_1 w_1 : V
h' : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {u : V} (h : G.Adj u v_1), ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w_1), cons h p = q.concat h'
u : V
h : G.Adj u u_1
y : V
q : G.Walk u_1 y
h'' : G.Adj y w_1
hc : cons h' p = q.concat h''
⊢ ∃ (x : V) (q : G.Walk u x) (h'_1 : G.Adj x w_1), cons h (cons h' p) = q.concat h'_1

Tactic:
exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
nil : ∀ {u u_1 : V} (h : G.Adj u_1 u), ∃ (x : V) (q : G.Walk u_1 x) (h' : G.Adj x u), Walk.cons h Walk.nil = q.concat h'
cons :
  ∀ {u v w : V} (h' : G.Adj u v) (p : G.Walk v w)
    (ih : ∀ {u : V} (h : G.Adj u v), ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), Walk.cons h p = q.concat h') {u_1 : V}
    (h : G.Adj u_1 u), ∃ (x : V) (q : G.Walk u_1 x) (h'_1 : G.Adj x w), Walk.cons h (Walk.cons h' p) = q.concat h'_1
⊢ ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), Walk.cons h p = q.concat h'

Tactic:
induction p generalizing u with
  | nil => exact ⟨_, nil, h, rfl⟩
  | cons h' p ih =>
    obtain ⟨y, q, h'', hc⟩ := ih h'
    exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq.{u + 1} (α := G.Walk u u) (reverse nil) nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.reverseAux, SimpleGraph.Walk.reverse, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).reverse = cons ⋯ nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.reverseAux, SimpleGraph.Walk.reverse, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.reverse = ⋯.toWalk

Tactic:
rfl

Premises used: SimpleGraph.Walk.reverseAux, SimpleGraph.Walk.reverse, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk w x
h : G.Adj w u
⊢ (cons h p).reverseAux q = p.reverseAux (cons ⋯ q)

Tactic:
rfl

Premises used: SimpleGraph.Walk.reverseAux, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x u_1 : V
q : G.Walk u_1 w
r : G.Walk u_1 x
⊢ (append nil q).reverseAux r = q.reverseAux (Walk.reverseAux nil r)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ (q : G.Walk w_1 w) (r : G.Walk v_1 x), (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
q : G.Walk w_1 w
r : G.Walk u_1 x
⊢ ((cons h p).append q).reverseAux r = q.reverseAux ((cons h p).reverseAux r)

Tactic:
ih q (cons (G.symm h) r)

Premises used: SimpleGraph.Walk.reverseAux, SimpleGraph.symm, SimpleGraph.Walk.cons, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ (q : G.Walk w_1 w) (r : G.Walk v_1 x), (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
q : G.Walk w_1 w
r : G.Walk u_1 x
⊢ ((cons h p).append q).reverseAux r = q.reverseAux ((cons h p).reverseAux r)

Tactic:
exact ih q (cons (G.symm h) r)

Premises used: SimpleGraph.symm, SimpleGraph.Walk.cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk u x
nil :
  ∀ {u : V} (q : G.Walk u w) (r : G.Walk u x),
    (append Walk.nil q).reverseAux r = q.reverseAux (Walk.reverseAux Walk.nil r)
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
    (ih : ∀ (q : G.Walk w_1 w) (r : G.Walk v x), (p.append q).reverseAux r = q.reverseAux (p.reverseAux r))
    (q : G.Walk w_1 w) (r : G.Walk u x),
    ((Walk.cons h p).append q).reverseAux r = q.reverseAux ((Walk.cons h p).reverseAux r)
⊢ (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)

Tactic:
induction p with
  | nil => rfl
  | cons h _ ih => exact ih q (cons (G.symm h) r)

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u_1 : V
q : G.Walk u_1 w
⊢ (Walk.reverseAux nil q).append r = Walk.reverseAux nil (q.append r)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ (q : G.Walk v_1 w), (p.reverseAux q).append r = p.reverseAux (q.append r)
q : G.Walk u_1 w
⊢ ((cons h p).reverseAux q).append r = (cons h p).reverseAux (q.append r)

Tactic:
simp [ih (cons (G.symm h) q)]

Premises used: SimpleGraph.symm, SimpleGraph.Walk.cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
nil : ∀ {u : V} (q : G.Walk u w), (Walk.reverseAux Walk.nil q).append r = Walk.reverseAux Walk.nil (q.append r)
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
    (ih : ∀ (q : G.Walk v w), (p.reverseAux q).append r = p.reverseAux (q.append r)) (q : G.Walk u w),
    ((Walk.cons h p).reverseAux q).append r = (Walk.cons h p).reverseAux (q.append r)
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)

Tactic:
induction p with
  | nil => rfl
  | cons h _ ih => simp [ih (cons (G.symm h) q)]

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- 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 u w
⊢ p.reverseAux q = p.reverse.append q

Tactic:
simp [reverse]

Premises used: SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).reverse = p.reverse.append (cons ⋯ nil)

Tactic:
simp [reverse]

Premises used: SimpleGraph.Walk.reverse
-- 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 ⋯ ⋯).reverse = p.reverse.copy ⋯ ⋯
⊢ (p.copy hu hv).reverse = p.reverse.copy hv hu

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 ⋯ ⋯).reverse = p.reverse.copy ⋯ ⋯

Tactic:
rfl
-- 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
⊢ (p.append q).reverse = q.reverse.append p.reverse

Tactic:
simp [reverse]

Premises used: SimpleGraph.Walk.reverse
-- 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).reverse = cons ⋯ p.reverse

Tactic:
simp [concat_eq_append]

Premises used: SimpleGraph.Walk.concat_eq_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := G.Walk u_1 u_1) (reverse (reverse nil)) nil

Tactic:
rfl
-- 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
ih : p.reverse.reverse = p
⊢ (cons h p).reverse.reverse = cons h p

Tactic:
simp [ih]
-- 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} (α := G.Walk u u) (reverse (reverse Walk.nil)) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.reverse.reverse = p),
    (Walk.cons h p).reverse.reverse = Walk.cons h p
⊢ p.reverse.reverse = p

Tactic:
induction p with
  | nil => rfl
  | cons _ _ ih => simp [ih]

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ Surjective.{u + 1, u + 1} (α := G.Walk u v) reverse

Tactic:
RightInverse.surjective reverse_reverse

Premises used: Function.RightInverse.surjective, SimpleGraph.Walk.reverse_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ Injective.{u + 1, u + 1} (α := G.Walk u v) reverse

Tactic:
RightInverse.injective reverse_reverse

Premises used: Function.RightInverse.injective, SimpleGraph.Walk.reverse_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ Bijective.{u + 1, u + 1} (α := G.Walk u v) reverse

Tactic:
⟨reverse_injective, reverse_surjective⟩

Premises used: SimpleGraph.Walk.reverse_injective, SimpleGraph.Walk.reverse_surjective, And.intro, Function.Bijective
-- 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 ⋯ ⋯).length = p.length
⊢ (p.copy hu hv).length = p.length

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 ⋯ ⋯).length = p.length

Tactic:
rfl
-- 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 : ∀ {u : V} (q : G.Walk u w), (append Walk.nil q).length = length.{u} (V := V) (G := G) (u := u) Walk.nil + q.length
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 w), (p.append q).length = p.length + q.length) →
      ∀ (q : G.Walk w_1 w), ((Walk.cons h p).append q).length = (Walk.cons h p).length + q.length
⊢ (p.append q).length = p.length + q.length

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

Tactic:
simp [*, add_comm, add_assoc]

Premises used: add_assoc, add_comm
-- 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 : ∀ (q : G.Walk w_1 w), (p.append q).length = p.length + q.length
q : G.Walk w_1 w
⊢ ((cons h p).append q).length = (cons h p).length + q.length

Tactic:
simp [*, add_comm, add_assoc]

Premises used: add_assoc, add_comm
-- 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).length = p.length + 1

Tactic:
length_append _ _

Premises used: SimpleGraph.Walk.length, SimpleGraph.Walk.concat, SimpleGraph.Walk.length_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
q : G.Walk u_1 w
⊢ (Walk.reverseAux nil q).length = length.{u} (V := V) (G := G) (u := u_1) nil + q.length

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
ih : ∀ (q : G.Walk v_1 w), (p.reverseAux q).length = p.length + q.length
q : G.Walk u_1 w
⊢ ((cons h p).reverseAux q).length = (cons h p).length + q.length

Tactic:
simp [ih, Nat.succ_add, add_assoc]

Premises used: add_assoc, Nat.succ_add
-- 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 u w
nil :
  ∀ {u : V} (q : G.Walk u w),
    (Walk.reverseAux Walk.nil q).length = length.{u} (V := V) (G := G) (u := u) Walk.nil + q.length
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
    (ih : ∀ (q : G.Walk v w), (p.reverseAux q).length = p.length + q.length) (q : G.Walk u w),
    ((Walk.cons h p).reverseAux q).length = (Walk.cons h p).length + q.length
⊢ (p.reverseAux q).length = p.length + q.length

Tactic:
induction p with
  | nil => simp!
  | cons _ _ ih => simp [ih, Nat.succ_add, add_assoc]

Premises used: add_assoc, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, Nat.succ_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.length = p.length

Tactic:
simp [reverse]

Premises used: SimpleGraph.Walk.reverse
-- 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
i : ℕ
nil :
  ∀ {u : V} (q : G.Walk u w) (i : ℕ),
    (append Walk.nil q).getVert i =
      if i < length.{u} (V := V) (G := G) (u := u) Walk.nil then getVert (G := G) (u := u) Walk.nil i
      else q.getVert (i - length.{u} (V := V) (G := G) (u := u) Walk.nil)
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 w) (i : ℕ),
        (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)) →
      ∀ (q : G.Walk w_1 w) (i : ℕ),
        ((Walk.cons h p).append q).getVert i =
          if i < (Walk.cons h p).length then (Walk.cons h p).getVert i else q.getVert (i - (Walk.cons h p).length)
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

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

Tactic:
cases i
-- 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 :
  ∀ (q : G.Walk w_1 w) (i : ℕ), (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
q : G.Walk w_1 w
i : ℕ
cons :
  ((Walk.cons h p).append q).getVert 0 =
    if 0 < (Walk.cons h p).length then (Walk.cons h p).getVert 0 else q.getVert (0 - (Walk.cons h p).length)
cons₁ :
  ∀ (n : ℕ),
    ((Walk.cons h p).append q).getVert (n + 1) =
      if n + 1 < (Walk.cons h p).length then (Walk.cons h p).getVert (n + 1)
      else q.getVert (n + 1 - (Walk.cons h p).length)
⊢ ((Walk.cons h p).append q).getVert i =
    if i < (Walk.cons h p).length then (Walk.cons h p).getVert i else q.getVert (i - (Walk.cons h p).length)

Tactic:
cases i
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
q : G.Walk u_1 w
⊢ (append nil q).getVert 0 =
    if 0 < length.{u} (V := V) (G := G) (u := u_1) nil then getVert (G := G) (u := u_1) nil 0
    else q.getVert (0 - length.{u} (V := V) (G := G) (u := u_1) nil)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
q : G.Walk u_1 w
n : ℕ
⊢ (append nil q).getVert (n + 1) =
    if n + 1 < length.{u} (V := V) (G := G) (u := u_1) nil then getVert (G := G) (u := u_1) nil (n + 1)
    else q.getVert (n + 1 - length.{u} (V := V) (G := G) (u := u_1) nil)

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 :
  ∀ (q : G.Walk w_1 w) (i : ℕ), (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
q : G.Walk w_1 w
⊢ ((cons h p).append q).getVert 0 =
    if 0 < (cons h p).length then (cons h p).getVert 0 else q.getVert (0 - (cons h p).length)

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 :
  ∀ (q : G.Walk w_1 w) (i : ℕ), (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
q : G.Walk w_1 w
n : ℕ
⊢ ((cons h p).append q).getVert (n + 1) =
    if n + 1 < (cons h p).length then (cons h p).getVert (n + 1) else q.getVert (n + 1 - (cons h p).length)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 : V
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := u_1) (reverse nil) i)
    (getVert (G := G) (u := u_1) nil (length.{u} (V := V) (G := G) (u := u_1) nil - i))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
cons :
  (if i < p.length then p.getVert (p.length - i) else (Walk.cons ⋯ nil).getVert (i - p.length)) =
    (Walk.cons h p).getVert (p.length + 1 - i)
⊢ (Walk.cons h p).reverse.getVert i = (Walk.cons h p).getVert ((Walk.cons h p).length - i)

Tactic:
simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]

Premises used: SimpleGraph.Walk.getVert_append, SimpleGraph.Walk.length_reverse, SimpleGraph.Walk.length_cons, SimpleGraph.Walk.reverse_cons