awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
p : G.Walk u v
h : G.Adj v w
p' : G.Walk u v'
h' : G.Adj v' w
he : p.concat h = p'.concat h'
nil :
  ∀ {u : V} {h : G.Adj u w} {p' : G.Walk u v'} (he : concat Walk.nil h = p'.concat h'),
    ∃ (hv : u = v'), Walk.copy Walk.nil ⋯ hv = p'
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
    (ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p')
    {h_1 : G.Adj w_1 w} {p' : G.Walk u v'} (he : (Walk.cons h p).concat h_1 = p'.concat h'),
    ∃ (hv : w_1 = v'), (Walk.cons h p).copy ⋯ hv = p'
⊢ ∃ (hv : v = v'), p.copy ⋯ hv = p'

Tactic:
induction p with
  | nil =>
    cases p'
    · exact ⟨rfl, rfl⟩
    · simp only [concat_nil, concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim
  | cons _ _ ih =>
    rw [concat_cons] at he
    cases p'
    · simp only [concat_nil, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he)).elim
    · rw [concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)
      exact ⟨rfl, rfl⟩

Premises used: SimpleGraph.Walk.cons.injEq, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.concat_nil, SimpleGraph.Walk.concat_cons, 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
nil : ∀ {u : V} (h : G.Adj u w), (concat Walk.nil h).support = support (G := G) (u := u) Walk.nil ++ [w]
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (h : G.Adj w_1 w), (p.concat h).support = p.support ++ [w]) →
      ∀ (h_1 : G.Adj w_1 w), ((Walk.cons h p).concat h_1).support = (Walk.cons h p).support ++ [w]
⊢ (p.concat h).support = p.support ++ [w]

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
h : G.Adj u_1 w
⊢ (concat nil h).support = support (G := G) (u := u_1) nil ++ [w]

Tactic:
simp [*, concat_nil]

Premises used: SimpleGraph.Walk.concat_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : G.Adj w_1 w), (p.concat h).support = p.support ++ [w]
h : G.Adj w_1 w
⊢ ((cons h_1 p).concat h).support = (cons h_1 p).support ++ [w]

Tactic:
simp [*, concat_nil]

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

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

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
nil : ∀ {u : V} (p' : G.Walk u w), (append Walk.nil p').support = support (G := G) (u := u) Walk.nil ++ p'.support.tail
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').support = p.support ++ p'.support.tail) →
      ∀ (p' : G.Walk w_1 w), ((Walk.cons h p).append p').support = (Walk.cons h p).support ++ p'.support.tail
⊢ (p.append p').support = p.support ++ p'.support.tail

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
nil :
  support (G := G) (u := w) (append Walk.nil Walk.nil) =
    HAppend.hAppend (α := List V) (support (G := G) (u := w) Walk.nil) (List.tail (support (G := G) (u := w) Walk.nil))
nil₁ :
  ∀ {v : V} (h : G.Adj u_1 v) (p : G.Walk v w),
    (append Walk.nil (cons h p)).support = support (G := G) (u := u_1) Walk.nil ++ (cons h p).support.tail
⊢ (append Walk.nil p').support = support (G := G) (u := u_1) Walk.nil ++ p'.support.tail

Tactic:
cases p'
-- 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').support = p.support ++ p'.support.tail
p' : G.Walk w_1 w
cons :
  ∀ (p : G.Walk v_1 w),
    (∀ (p' : G.Walk w w), (p.append p').support = p.support ++ p'.support.tail) →
      ((Walk.cons h p).append nil).support = (Walk.cons h p).support ++ List.tail (support (G := G) (u := w) nil)
cons₁ :
  ∀ {v : V} (h_1 : G.Adj w_1 v) (p_1 : G.Walk v w),
    ((Walk.cons h p).append (Walk.cons h_1 p_1)).support = (Walk.cons h p).support ++ (Walk.cons h_1 p_1).support.tail
⊢ ((Walk.cons h p).append p').support = (Walk.cons h p).support ++ p'.support.tail

Tactic:
cases p'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
⊢ support (G := G) (u := w) (append nil nil) =
    HAppend.hAppend (α := List V) (support (G := G) (u := w) nil) (List.tail (support (G := G) (u := w) nil))

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
⊢ (append nil (cons h p)).support = support (G := G) (u := u_1) nil ++ (cons h p).support.tail

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (p' : G.Walk w w), (p.append p').support = p.support ++ p'.support.tail
⊢ ((cons h p).append nil).support = (cons h p).support ++ List.tail (support (G := G) (u := w) 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 : ∀ (p' : G.Walk w_1 w), (p.append p').support = p.support ++ p'.support.tail
v_2 : V
h_1 : G.Adj w_1 v_2
p_1 : G.Walk v_2 w
⊢ ((cons h p).append (cons h_1 p_1)).support = (cons h p).support ++ (cons h_1 p_1).support.tail

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 V) (support (G := G) (u := u) (reverse Walk.nil))
      (List.reverse (support (G := G) (u := u) Walk.nil))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    p.reverse.support = p.support.reverse → (Walk.cons h p).reverse.support = (Walk.cons h p).support.reverse
⊢ p.reverse.support = p.support.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 V) (support (G := G) (u := u_1) (reverse nil)) (List.reverse (support (G := G) (u := u_1) nil))

Tactic:
simp [support_append, *]

Premises used: SimpleGraph.Walk.support_append
-- 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.support = p.support.reverse
⊢ (cons h p).reverse.support = (cons h p).support.reverse

Tactic:
simp [support_append, *]

Premises used: SimpleGraph.Walk.support_append
-- 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').support = List.dropLast (support (G := G) (u := u) Walk.nil) ++ p'.support
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').support = p.support.dropLast ++ p'.support) →
      ∀ (p' : G.Walk w_1 w), ((Walk.cons h p).append p').support = (Walk.cons h p).support.dropLast ++ p'.support
⊢ (p.append p').support = p.support.dropLast ++ p'.support

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').support = List.dropLast (support (G := G) (u := u_1) nil) ++ p'.support

Tactic:
simp_all [List.dropLast_cons_of_ne_nil]

Premises used: List.dropLast_cons_of_ne_nil
-- 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').support = p.support.dropLast ++ p'.support
p' : G.Walk w_1 w
⊢ ((cons h p).append p').support = (cons h p).support.dropLast ++ p'.support

Tactic:
simp_all [List.dropLast_cons_of_ne_nil]

Premises used: List.dropLast_cons_of_ne_nil
-- 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
rw : (p.support ++ p'.support.tail).tail = p.support.tail ++ p'.support.tail
rw₁ rw₂ : p.support.tail ++ p'.support.tail = p.support.tail ++ p'.support.tail
⊢ (p.append p').support.tail = p.support.tail ++ p'.support.tail

Tactic:
rw [support_append, List.tail_append_of_ne_nil (support_ne_nil _)]

Premises used: List.tail_append_of_ne_nil, SimpleGraph.Walk.support_append, SimpleGraph.Walk.support_ne_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ List.dropLast (support (G := G) (u := u) nil) ++ [u] = support (G := G) (u := u) nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).support.dropLast ++ [v] = (Walk.cons h p).support
⊢ p.support.dropLast ++ [v] = p.support

Tactic:
cases p with | nil => rfl | cons h p

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- 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 :
  ∀ (w : V) (w_1 : G.Walk u w) (w_2 : G.Adj w v) (hp : Walk.cons h p = w_1.concat w_2),
    (Walk.cons h p).support.dropLast ++ [v] = (Walk.cons h p).support
⊢ (Walk.cons h p).support.dropLast ++ [v] = (Walk.cons h p).support

Tactic:
have ⟨_, _, _, hp⟩ := p.exists_cons_eq_concat h
-- 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
w : V
w_1 : G.Walk u w
w_2 : G.Adj w v
hp : cons h p = w_1.concat w_2
⊢ (cons h p).support.dropLast ++ [v] = (cons h p).support

Tactic:
simp [hp]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support = p.support.dropLast.concat v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
⊢ p = q

Tactic:
darts_injective (Dart.toProd_injective.list_map (List.rightInverse_unzip_zip.injective ?_))

Premises used: SimpleGraph.Walk.darts_injective, Function.Injective.list_map, List.rightInverse_unzip_zip, Function.RightInverse.injective, SimpleGraph.Dart.toProd_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
refine : (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip
⊢ p = q

Tactic:
refine darts_injective (Dart.toProd_injective.list_map (List.rightInverse_unzip_zip.injective ?_))

Premises used: SimpleGraph.Walk.darts_injective, Function.Injective.list_map, List.rightInverse_unzip_zip, Function.RightInverse.injective, SimpleGraph.Dart.toProd_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
⊢ Eq.{u + 1} (α := G.Dart → V) (Prod.fst ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.1

Tactic:
have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
this : Eq.{u + 1} (α := G.Dart → V) (Prod.fst ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.1
⊢ Eq.{u + 1} (α := G.Dart → V) (Prod.snd ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.2

Tactic:
have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
this_1 : Eq.{u + 1} (α := G.Dart → V) (Prod.fst ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.1
this : Eq.{u + 1} (α := G.Dart → V) (Prod.snd ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.2
⊢ (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip

Tactic:
grind [map_fst_darts, map_snd_darts]

Premises used: SimpleGraph.Walk.map_snd_darts, SimpleGraph.Walk.map_fst_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
rw : t ∈ p.support.tail ++ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
rw₁ rw₂ : t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
⊢ t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

Tactic:
rw [tail_support_append, List.mem_append]

Premises used: List.mem_append, SimpleGraph.Walk.tail_support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
simp : t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
⊢ t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support

Tactic:
simp only [mem_support_iff, mem_tail_support_append_iff]

Premises used: SimpleGraph.Walk.mem_tail_support_append_iff, SimpleGraph.Walk.mem_support_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
inl :
  ∀ (p : G.Walk u t) (p' : G.Walk t w),
    t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
inr :
  ∀ (h : t ≠ v),
    t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
obtain rfl | h := eq_or_ne t v

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
inl :
  ∀ (p : G.Walk t t),
    t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
inl₁ :
  ∀ (h' : t ≠ u),
    t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail

Tactic:
obtain rfl | h' := eq_or_ne t u

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
inr :
  ∀ (p : G.Walk t v),
    t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
inr₁ :
  ∀ (h' : t ≠ u),
    t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
obtain rfl | h' := eq_or_ne t u

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
h' : t ≠ u
⊢ u ≠ t

Tactic:
have := h'.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
h' : t ≠ u
⊢ u ≠ t

Tactic:
try have := h'.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
⊢ u ≠ t

Tactic:
have := h'.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
⊢ u ≠ t

Tactic:
try have := h'.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t w : V
p' : G.Walk t w
p : G.Walk t t
⊢ t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
h' : t ≠ u
this : u ≠ t
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t v w : V
p' : G.Walk v w
h : t ≠ v
p : G.Walk t v
⊢ t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
this : u ≠ t
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hadj : G.Adj v w
⊢ p.support ⊆ (p.concat hadj).support

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
⊢ p.support ⊆ (p.append q).support

Tactic:
simp [support_append]

Premises used: SimpleGraph.Walk.support_append
-- 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
a : V
⊢ a ∈ q.support → a ∈ (p.append q).support

Tactic:
simp +contextual [mem_support_append_iff]

Premises used: SimpleGraph.Walk.mem_support_append_iff
-- 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
rw :
  (↑(p.support ++ p'.support.tail) : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
rw₁ :
  (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
rw₂ rw₃ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
⊢ (↑(p.append p').support : Multiset V) = {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)

Tactic:
rw [support_append, ← Multiset.coe_add, coe_support]

Premises used: Multiset.coe_add, SimpleGraph.Walk.support_append, SimpleGraph.Walk.coe_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
simp_rw : (↑(p.support ++ p'.support.tail) : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₁ :
  (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
    (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₂ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + ({v} + (↑p'.support.tail : Multiset V)) - {v}
simp_rw₃ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + ((↑p'.support.tail : Multiset V) + {v}) - {v}
simp_rw₄ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) + {v} - {v}
⊢ (↑(p.append p').support : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}

Tactic:
simp_rw [support_append, ← Multiset.coe_add, coe_support, add_comm ({v} : Multiset V),
    ← add_assoc, add_tsub_cancel_right]

Premises used: Multiset.coe_add, add_assoc, add_comm, SimpleGraph.Walk.support_append, add_tsub_cancel_right, Singleton.singleton, SimpleGraph.Walk.coe_support
-- 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
⊢ u = p.support.head ⋯

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
⊢ v = p.support.getLast ⋯

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Eq.{u + 1} (α :=
    G.Walk (List.head (support (G := G) (u := u) nil) ⋯) (List.getLast (support (G := G) (u := u) nil) ⋯))
    (ofSupport (support (G := G) (u := u) nil) ⋯ ⋯) (Walk.copy nil ⋯ ⋯)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
w : V
h : G.Adj u w
⊢ ofSupport (cons h nil).support ⋯ ⋯ = (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
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
⊢ ofSupport (cons h₂ p).support ⋯ ⋯ = (cons h₂ p).copy ⋯ ⋯

Tactic:
have := p.cons h₂ |>.ofSupport_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
this : ofSupport (u' :: p.support) ⋯ ⋯ = (cons h₂ p).copy ⋯ ⋯
⊢ ofSupport (cons h₁ (cons h₂ p)).support ⋯ ⋯ = (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
⊢ ofSupport p.support ⋯ ⋯ = p.copy ⋯ ⋯

Tactic:
match p with
  | nil => rfl
  | cons (v := w) h .nil => rfl
  | cons (v := u') h₁ (.cons (v := v') h₂ p) =>
    have := p.cons h₂ |>.ofSupport_support
    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
nil :
  ∀ {u : V} (h : G.Adj u w),
    (concat Walk.nil h).darts = List.concat (darts (u := u) Walk.nil) { fst := u, snd := w, adj := h }
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (h : G.Adj w_1 w), (p.concat h).darts = p.darts.concat { fst := w_1, snd := w, adj := h }) →
      ∀ (h_1 : G.Adj w_1 w),
        ((Walk.cons h p).concat h_1).darts = (Walk.cons h p).darts.concat { fst := w_1, snd := w, adj := h_1 }
⊢ (p.concat h).darts = p.darts.concat { fst := v, snd := w, adj := h }

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
h : G.Adj u_1 w
⊢ (concat nil h).darts = List.concat (darts (u := u_1) nil) { fst := u_1, snd := w, adj := h }

Tactic:
simp [*, concat_nil]

Premises used: SimpleGraph.Walk.concat_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : G.Adj w_1 w), (p.concat h).darts = p.darts.concat { fst := w_1, snd := w, adj := h }
h : G.Adj w_1 w
⊢ ((cons h_1 p).concat h).darts = (cons h_1 p).darts.concat { fst := w_1, snd := w, adj := h }

Tactic:
simp [*, concat_nil]

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

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

Tactic:
rfl