awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
rw : (cons ⋯ p.tail).length = p.length
rw₁ rw₂ : p.length = p.length
⊢ p.tail.length + 1 = p.length

Tactic:
rw [← length_cons (p.adj_snd hp), cons_tail_eq _ hp]

Premises used: SimpleGraph.Walk.length_cons, SimpleGraph.Walk.adj_snd, SimpleGraph.Walk.cons_tail_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
rw : (p.dropLast.concat ⋯).length = p.length
rw₁ rw₂ : p.length = p.length
⊢ p.dropLast.length + 1 = p.length

Tactic:
rw [← length_concat _ <| p.adj_penultimate hp, concat_dropLast]

Premises used: SimpleGraph.Walk.adj_penultimate, SimpleGraph.Walk.concat_dropLast, SimpleGraph.Walk.length_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  length.{u} (V := V) (G := G) (u := u) (v := penultimate (G := G) (u := u) Walk.nil) (dropLast Walk.nil) =
    length.{u} (V := V) (G := G) (u := u) Walk.nil - 1
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).dropLast.length = (Walk.cons h p).length - 1
⊢ p.dropLast.length = p.length - 1

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ length.{u} (V := V) (G := G) (u := u) (v := penultimate (G := G) (u := u) nil) (dropLast nil) =
    length.{u} (V := V) (G := G) (u := u) nil - 1

Tactic:
simp [← length_dropLast_add_one not_nil_cons]

Premises used: SimpleGraph.Walk.not_nil_cons, SimpleGraph.Walk.length_dropLast_add_one
-- 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).dropLast.length = (cons h p).length - 1

Tactic:
simp [← length_dropLast_add_one not_nil_cons]

Premises used: SimpleGraph.Walk.not_nil_cons, SimpleGraph.Walk.length_dropLast_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
nil :
  ∀ (hp : Nil.{u} (V := V) (G := G) (v := v) Walk.nil),
    Nil.{u} (V := V) (G := G) (v := snd (G := G) (u := v) Walk.nil) (tail Walk.nil)
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w) (hp : (Walk.cons h p).Nil), (Walk.cons h p).tail.Nil
⊢ p.tail.Nil

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

Tactic:
simp at hp ⊢
-- 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
hp : (cons h p).Nil
⊢ (cons h p).tail.Nil

Tactic:
simp at hp ⊢
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.tail.Nil
⊢ ¬p.Nil

Tactic:
mt Nil.tail hp

Premises used: mt, SimpleGraph.Walk.Nil.tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
nil :
  ∀ (hp : Nil.{u} (V := V) (G := G) (v := v) Walk.nil),
    Nil.{u} (V := V) (G := G) (v := v) (w := penultimate (G := G) (u := v) Walk.nil) (dropLast Walk.nil)
cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w) (hp : (Walk.cons h p).Nil), (Walk.cons h p).dropLast.Nil
⊢ p.dropLast.Nil

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

Tactic:
simp at hp ⊢
-- 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
hp : (cons h p).Nil
⊢ (cons h p).dropLast.Nil

Tactic:
simp at hp ⊢
-- 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 ⋯ ⋯).Nil = p.Nil
⊢ (p.copy hu hv).Nil = p.Nil

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

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.Nil
⊢ p = Walk.copy Walk.nil ⋯ ⋯

Tactic:
grind [eq_nil_iff_nil, copy_rfl_rfl]

Premises used: SimpleGraph.Walk.copy_rfl_rfl, SimpleGraph.Walk.eq_nil_iff_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ p.drop n = Walk.copy nil ⋯ ⋯

Tactic:
(nil_drop_of_length_le h).eq_copy_nil

Premises used: SimpleGraph.Walk.nil_drop_of_length_le, SimpleGraph.Walk.Nil.eq_copy_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
rw : p.tail.support = (u :: p.tail.support).tail
rw₁ rw₂ : p.tail.support = p.tail.support
⊢ p.tail.support = p.support.tail

Tactic:
rw [← cons_support_tail hp, List.tail_cons]

Premises used: List.tail_cons, SimpleGraph.Walk.cons_support_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
i : ℕ
h : u = w
h' : v = x
subst_vars : ∀ (p : G.Walk w x), (p.copy ⋯ ⋯).getVert i = p.getVert i
⊢ (p.copy h h').getVert i = p.getVert i

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
w x : V
i : ℕ
p : G.Walk w x
⊢ (p.copy ⋯ ⋯).getVert i = p.getVert i

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
nil :
  Eq.{u + 1} (α := V) (getVert (G := G) (u := snd (G := G) (u := u) Walk.nil) (tail Walk.nil) n)
    (getVert (G := G) (u := u) Walk.nil (n + 1))
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).tail.getVert n = (Walk.cons h p).getVert (n + 1)
⊢ p.tail.getVert n = p.getVert (n + 1)

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := snd (G := G) (u := u) nil) (tail nil) n)
    (getVert (G := G) (u := u) nil (n + 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).tail.getVert n = (cons h p).getVert (n + 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
h : i + 1 ≠ 0
rw : p.tail.getVert i ∈ p.tail.support
⊢ p.getVert (i + 1) ∈ p.support.tail

Tactic:
rw [← getVert_tail, ← p.support_tail_of_not_nil hp]

Premises used: SimpleGraph.Walk.getVert_tail, SimpleGraph.Walk.support_tail_of_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
h : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.tail.support

Tactic:
getVert_mem_support ..

Premises used: SimpleGraph.Walk.getVert_mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
h : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.tail.support

Tactic:
exact getVert_mem_support ..

Premises used: SimpleGraph.Walk.getVert_mem_support
-- 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) support

Tactic:
fun _ _ ↦ ext_support

Premises used: SimpleGraph.Walk.ext_support, Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
this :
  ∀ (k : ℕ),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
      getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
⊢ p = q

Tactic:
ext_support <| List.ext_getElem?_iff.mpr this

Premises used: Iff.mpr, SimpleGraph.Walk.ext_support, List.ext_getElem?_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
this :
  ∀ (k : ℕ),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
      getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
⊢ p = q

Tactic:
exact ext_support <| List.ext_getElem?_iff.mpr this

Premises used: Iff.mpr, SimpleGraph.Walk.ext_support, List.ext_getElem?_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
suffices :
  ∀ (k : ℕ),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
      getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
⊢ p = q

Tactic:
suffices ∀ k : ℕ, p.support[k]? = q.support[k]? by
    exact ext_support <| List.ext_getElem?_iff.mpr this
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
inl : some (p.getVert k) = some (q.getVert k)
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k

Tactic:
rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem?
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ some (p.getVert k) = some (q.getVert k)

Tactic:
congrArg some (h k hk)

Premises used: congrArg, Option.some
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ some (p.getVert k) = some (q.getVert k)

Tactic:
exact congrArg some (h k hk)

Premises used: congrArg, Option.some
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length < k
⊢ p.length + 1 ≤ k

Tactic:
replace hk : p.length + 1 ≤ k := hk
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
⊢ q.length + 1 ≤ k

Tactic:
have ht : q.length + 1 ≤ k := hl ▸ hk
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
ht : q.length + 1 ≤ k
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none

Tactic:
rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht

Premises used: SimpleGraph.Walk.length_support, List.getElem?_eq_none_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
ht : q.length + 1 ≤ k
hk₁ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k = none

Tactic:
rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht

Premises used: SimpleGraph.Walk.length_support, List.getElem?_eq_none_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none
ht : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k = none
inr : none = getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
inr₁ inr₂ : Eq.{u + 1} (α := Option V) none none
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k

Tactic:
rw [hk, ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
⊢ k ≤ p.length ∨ p.length < k

Tactic:
cases le_or_gt k p.length with
  | inl hk =>
    rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
    exact congrArg some (h k hk)
  | inr hk =>
    replace hk : p.length + 1 ≤ k := hk
    have ht : q.length + 1 ≤ k := hl ▸ hk
    rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
    rw [hk, ht]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem?, SimpleGraph.Walk.length, SimpleGraph.Walk.length_support, le_or_gt, List.getElem?_eq_none_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
inr :
  ∀ (this : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q)
    (hpq : ¬p.length ≤ q.length), p = q
wlog : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q
⊢ p = q

Tactic:
wlog hpq : p.length ≤ q.length generalizing p q

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
this : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q
hpq : ¬p.length ≤ q.length
⊢ p = q

Tactic:
(this (h · |>.symm) (le_of_not_ge hpq)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
this : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q
hpq : ¬p.length ≤ q.length
⊢ p = q

Tactic:
exact (this (h · |>.symm) (le_of_not_ge hpq)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
⊢ p = q

Tactic:
ext_getVert_le_length (hpq.antisymm ?_) fun k _ ↦ h k

Premises used: LE.le.antisymm, SimpleGraph.Walk.ext_getVert_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
refine : q.length ≤ p.length
⊢ p = q

Tactic:
refine ext_getVert_le_length (hpq.antisymm ?_) fun k _ ↦ h k

Premises used: LE.le.antisymm, SimpleGraph.Walk.ext_getVert_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
by_contra! : ∀ (this : p.length < q.length), False
⊢ q.length ≤ p.length

Tactic:
by_contra!
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
this : p.length < q.length
⊢ q.getVert p.length = q.getVert (p.length + 1)

Tactic:
simp [← h, getVert_of_length_le]

Premises used: SimpleGraph.Walk.getVert_of_length_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
this : p.length < q.length
⊢ False

Tactic:
exact (q.adj_getVert_succ this).ne (by simp [← h, getVert_of_length_le])

Premises used: SimpleGraph.Adj.ne, SimpleGraph.Walk.adj_getVert_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p = (append nil p).append nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
q : G.Walk u v
⊢ q = append (append nil nil) q

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj w u'
obtain : ∀ (r1 : G.Walk u' u) (r2 : G.Walk v v'), p.IsSubwalk (cons h ((r1.append p).append r2))
⊢ p.IsSubwalk (cons h q)

Tactic:
obtain ⟨r1, r2, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj w u'
r1 : G.Walk u' u
r2 : G.Walk v v'
h₁ : cons h ((r1.append p).append r2) = ((cons h r1).append p).append r2
⊢ p.IsSubwalk (cons h ((r1.append p).append r2))

Tactic:
use r1.cons h, r2

Premises used: SimpleGraph.Walk.cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj w u'
r1 : G.Walk u' u
r2 : G.Walk v v'
⊢ cons h ((r1.append p).append r2) = ((cons h r1).append p).append r2

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj w u
⊢ p.IsSubwalk (cons h p)

Tactic:
(isSubwalk_rfl p).cons h

Premises used: SimpleGraph.Walk.isSubwalk_rfl, SimpleGraph.Walk.IsSubwalk.cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj v' w
obtain : ∀ (r₁ : G.Walk u' u) (r₂ : G.Walk v v'), p.IsSubwalk (((r₁.append p).append r₂).concat h)
⊢ p.IsSubwalk (q.concat h)

Tactic:
obtain ⟨r₁, r₂, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj v' w
r₁ : G.Walk u' u
r₂ : G.Walk v v'
rw rw₁ : ((r₁.append p).append r₂).concat h = ((r₁.append p).append r₂).concat h
⊢ ((r₁.append p).append r₂).concat h = (r₁.append p).append (r₂.concat h)

Tactic:
rw [append_concat]

Premises used: SimpleGraph.Walk.append_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj v' w
r₁ : G.Walk u' u
r₂ : G.Walk v v'
⊢ p.IsSubwalk (((r₁.append p).append r₂).concat h)

Tactic:
exact ⟨r₁, r₂.concat h, by rw [append_concat]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ p.IsSubwalk (p.concat h)

Tactic:
(isSubwalk_rfl p).concat h

Premises used: SimpleGraph.Walk.isSubwalk_rfl, SimpleGraph.Walk.IsSubwalk.concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
p₂ : G.Walk u₂ v₂
p₃ : G.Walk u₃ v₃
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₃
obtain : ∀ (q₁ : G.Walk u₂ u₁) (r₁ : G.Walk v₁ v₂) (h₂ : ((q₁.append p₁).append r₁).IsSubwalk p₃), p₁.IsSubwalk p₃
⊢ p₁.IsSubwalk p₃

Tactic:
obtain ⟨q₁, r₁, rfl⟩ := h₁

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
p₃ : G.Walk u₃ v₃
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
h₂ : ((q₁.append p₁).append r₁).IsSubwalk p₃
obtain : ∀ (q₂ : G.Walk u₃ u₂) (r₂ : G.Walk v₂ v₃), p₁.IsSubwalk ((q₂.append ((q₁.append p₁).append r₁)).append r₂)
⊢ p₁.IsSubwalk p₃

Tactic:
obtain ⟨q₂, r₂, rfl⟩ := h₂

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
h : (q₂.append ((q₁.append p₁).append r₁)).append r₂ = ((q₂.append q₁).append p₁).append (r₁.append r₂)
⊢ p₁.IsSubwalk ((q₂.append ((q₁.append p₁).append r₁)).append r₂)

Tactic:
use q₂.append q₁, r₁.append r₂

Premises used: SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
⊢ (q₂.append ((q₁.append p₁).append r₁)).append r₂ = ((q₂.append q₁).append p₁).append (r₁.append r₂)

Tactic:
simp [append_assoc]

Premises used: SimpleGraph.Walk.append_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u u' : V
nil :
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil →
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)
nil₁ :
  (∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)) →
    IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil
⊢ IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil ↔
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u : V
⊢ ∃ (hu : u = u) (hv : u = u), Eq (α := G.Walk u u) nil (Walk.copy nil hu hv)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u' : V
w : u' = u'
h : Eq (α := G.Walk u' u') nil (Walk.copy nil ⋯ w)
⊢ IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u') (u₂ := u') nil nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
cons : (Walk.cons h p).IsSubwalk (u₂ := u') nil → ∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy nil hu hv
cons₁ : (∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy nil hu hv) → (Walk.cons h p).IsSubwalk (u₂ := u') nil
⊢ (Walk.cons h p).IsSubwalk (u₂ := u') nil ↔ ∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy nil hu hv

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
w : G.Walk v u
h : nil = (append nil (cons h_1 p)).append w
⊢ ∃ (hu : u = u) (hv : u = v), cons h_1 p = Walk.copy nil hu hv

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
v_2 : V
h_2 : G.Adj u' v_2
p_1 : G.Walk v_2 u
w : G.Walk v u'
h : nil = ((cons h_2 p_1).append (cons h_1 p)).append w
⊢ ∃ (hu : u' = u) (hv : u' = v), cons h_1 p = Walk.copy nil hu hv

Tactic:
simp at h