mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).getVert 0 = if 0 ≤ nil.length then nil.getVert 0 else q.getVert (0 - nil.length)

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
n✝ : ℕ
⊢ (nil.append q).getVert (n✝ + 1) =
    if n✝ + 1 ≤ nil.length then nil.getVert (n✝ + 1) else q.getVert (n✝ + 1 - nil.length)

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ 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✝ 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)

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ 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✝ 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:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).getVert 0 = if 0 ≤ nil.length then nil.getVert 0 else q.getVert (0 - nil.length)

case nil.succ
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
n✝ : ℕ
⊢ (nil.append q).getVert (n✝ + 1) =
    if n✝ + 1 ≤ nil.length then nil.getVert (n✝ + 1) else q.getVert (n✝ + 1 - nil.length)

case cons.zero
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ 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✝ 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)

case cons.succ
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ 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✝ 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)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case cons.mp.nil
V : Type u_1
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p : G.Walk v✝ v
w✝ : G.Walk v u
h : nil = (nil.append (cons h✝ p)).append w✝
⊢ ∃ (hu : u = u) (hv : u = v), cons h✝ p = nil.copy hu hv

pp: case cons.mp.cons
V : Type u_1
G : SimpleGraph V
u v u' v✝¹ : V
h✝¹ : G.Adj u v✝¹
p : G.Walk v✝¹ v
v✝ : V
h✝ : G.Adj u' v✝
p✝ : G.Walk v✝ u
w✝ : G.Walk v u'
h : nil = ((cons h✝ p✝).append (cons h✝¹ p)).append w✝
⊢ ∃ (hu : u' = u) (hv : u' = v), cons h✝¹ p = nil.copy hu hv

Tactic:
<;>

Goal state after:
case cons.mp.nil
V : Type u_1
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p : G.Walk v✝ v
w✝ : G.Walk v u
h : nil = (nil.append (cons h✝ p)).append w✝
⊢ ∃ (hu : u = u) (hv : u = v), cons h✝ p = nil.copy hu hv

case cons.mp.cons
V : Type u_1
G : SimpleGraph V
u v u' v✝¹ : V
h✝¹ : G.Adj u v✝¹
p : G.Walk v✝¹ v
v✝ : V
h✝ : G.Adj u' v✝
p✝ : G.Walk v✝ u
w✝ : G.Walk v u'
h : nil = ((cons h✝ p✝).append (cons h✝¹ p)).append w✝
⊢ ∃ (hu : u' = u) (hv : u' = v), cons h✝¹ p = nil.copy hu hv
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
⊢ nil.takeUntil v ⋯ = nil

pp: case cons
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).takeUntil u ⋯ = nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
⊢ nil.takeUntil v ⋯ = nil

case cons
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).takeUntil u ⋯ = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case e_4
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ p.reverse.reverse = p

pp: case e_6
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat p.reverse ≍ ⋯ ▸ concatRecAux Hnil Hconcat p.reverse

Tactic:
<;>

Goal state after:
case e_4
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ p.reverse.reverse = p

case e_6
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat p.reverse ≍ ⋯ ▸ concatRecAux Hnil Hconcat p.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
h : G.Adj u u
⊢ nil.concat h ≠ nil

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj v u
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).concat h ≠ nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
h : G.Adj u u
⊢ nil.concat h ≠ nil

case cons
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj v u
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).concat h ≠ nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ (h' ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) h' ⋯) =
    cons h✝ p✝

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ (h' ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) h' ⋯) =
    cons h✝ p✝

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), (p✝.takeUntil u✝ h).append (p✝.dropUntil u✝ h) = p✝
a✝ : List.Mem u✝ p✝.support
⊢ (⋯ ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) ⋯ ⋯) =
    cons h✝ p✝

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), (p✝.takeUntil u✝ h).append (p✝.dropUntil u✝ h) = p✝
a✝ : List.Mem u✝ p✝.support
⊢ (⋯ ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) ⋯ ⋯) =
    cons h✝ p✝

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case h_1
V : Type u
G : SimpleGraph V
u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
h : u ∈ nil.support
⊢ ⋯.mpr nil = nil

pp: case h_2
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
v✝ : V
r✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : u ∈ (cons r✝ p✝).support
⊢ (if hx : u = u then Eq.ndrec (motive := fun u_1 ↦ u_1 ∈ (cons r✝ p✝).support → G.Walk u_1 v) (fun h ↦ cons r✝ p✝) hx h
    else p✝.dropUntil u ⋯) =
    cons r✝ p✝

Tactic:
<;>

Goal state after:
case h_1
V : Type u
G : SimpleGraph V
u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
h : u ∈ nil.support
⊢ ⋯.mpr nil = nil

case h_2
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
v✝ : V
r✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : u ∈ (cons r✝ p✝).support
⊢ (if hx : u = u then Eq.ndrec (motive := fun u_1 ↦ u_1 ∈ (cons r✝ p✝).support → G.Walk u_1 v) (fun h ↦ cons r✝ p✝) hx h
    else p✝.dropUntil u ⋯) =
    cons r✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1.fst
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k].toProd.1 = p₁.darts[i].toProd.1

pp: case refine_1.snd
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k].toProd.2 = p₁.darts[i].toProd.2

Tactic:
<;>

Goal state after:
case refine_1.fst
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k].toProd.1 = p₁.darts[i].toProd.1

case refine_1.snd
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k].toProd.2 = p₁.darts[i].toProd.2
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).support = nil.support ++ [w]

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).support = p✝.support ++ [w]
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).support = (cons h✝ p✝).support ++ [w]

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).support = nil.support ++ [w]

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).support = p✝.support ++ [w]
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).support = (cons h✝ p✝).support ++ [w]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').support = nil.support ++ p'.support.tail

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').support = p✝.support ++ p'.support.tail
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').support = (cons h✝ p✝).support ++ p'.support.tail

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').support = nil.support ++ p'.support.tail

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').support = p✝.support ++ p'.support.tail
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').support = (cons h✝ p✝).support ++ p'.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.nil
V : Type u
G : SimpleGraph V
u v w : V
⊢ (nil.append nil).support = nil.support ++ nil.support.tail

pp: case nil.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).support = nil.support ++ (cons h✝ p✝).support.tail

pp: case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ 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 ++ nil.support.tail

pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝¹.append p').support = p✝¹.support ++ p'.support.tail
v✝ : V
h✝ : G.Adj w✝ v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).support = (cons h✝¹ p✝¹).support ++ (cons h✝ p✝).support.tail

Tactic:
<;>

Goal state after:
case nil.nil
V : Type u
G : SimpleGraph V
u v w : V
⊢ (nil.append nil).support = nil.support ++ nil.support.tail

case nil.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).support = nil.support ++ (cons h✝ p✝).support.tail

case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ 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 ++ nil.support.tail

case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝¹.append p').support = p✝¹.support ++ p'.support.tail
v✝ : V
h✝ : G.Adj w✝ v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).support = (cons h✝¹ p✝¹).support ++ (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ List.count u (h' ▸ nil).support = 1

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ List.count u (h' ▸ nil).support = 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.support = nil.support.reverse

pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.support = p✝.support.reverse
⊢ (cons h✝ p✝).reverse.support = (cons h✝ p✝).support.reverse

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.support = nil.support.reverse

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.support = p✝.support.reverse
⊢ (cons h✝ p✝).reverse.support = (cons h✝ p✝).support.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').support = nil.support.dropLast ++ p'.support

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').support = p✝.support.dropLast ++ p'.support
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').support = (cons h✝ p✝).support.dropLast ++ p'.support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').support = nil.support.dropLast ++ p'.support

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').support = p✝.support.dropLast ++ p'.support
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').support = (cons h✝ p✝).support.dropLast ++ p'.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : u✝ = u
h' : u = u✝
⊢ List.count u (h'✝ ▸ nil).support = 1

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : u✝ = u
h' : u = u✝
⊢ List.count u (h'✝ ▸ nil).support = 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), List.count u✝ (p✝.takeUntil u✝ h).support = 1
a✝ : List.Mem u✝ p✝.support
h' : u✝ = u✝
⊢ List.count u✝ (⋯ ▸ nil).support = 1

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), List.count u✝ (p✝.takeUntil u✝ h).support = 1
a✝ : List.Mem u✝ p✝.support
h' : u✝ = u✝
⊢ List.count u✝ (⋯ ▸ nil).support = 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos.inr.nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
ih : ∀ (h : u ∈ nil.support), List.count s(u, x) (nil.takeUntil u h).edges ≤ 1
a✝ : List.Mem u nil.support
⊢ List.count s(u, x) (nil.takeUntil u ⋯).edges + 1 ≤ 1

pp: case pos.inr.cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
v✝ : V
h✝ : G.Adj (u, x).1 v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (h : u ∈ (cons h✝ p✝).support), List.count s(u, x) ((cons h✝ p✝).takeUntil u h).edges ≤ 1
a✝ : List.Mem u (cons h✝ p✝).support
⊢ List.count s(u, x) ((cons h✝ p✝).takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
<;>

Goal state after:
case pos.inr.nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
ih : ∀ (h : u ∈ nil.support), List.count s(u, x) (nil.takeUntil u h).edges ≤ 1
a✝ : List.Mem u nil.support
⊢ List.count s(u, x) (nil.takeUntil u ⋯).edges + 1 ≤ 1

case pos.inr.cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
v✝ : V
h✝ : G.Adj (u, x).1 v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (h : u ∈ (cons h✝ p✝).support), List.count s(u, x) ((cons h✝ p✝).takeUntil u h).edges ≤ 1
a✝ : List.Mem u (cons h✝ p✝).support
⊢ List.count s(u, x) ((cons h✝ p✝).takeUntil u ⋯).edges + 1 ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).darts = nil.darts.concat { fst := u✝, snd := w, adj := h }

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).darts = p✝.darts.concat { fst := w✝, snd := w, adj := h }
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).darts = (cons h✝ p✝).darts.concat { fst := w✝, snd := w, adj := h }

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).darts = nil.darts.concat { fst := u✝, snd := w, adj := h }

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).darts = p✝.darts.concat { fst := w✝, snd := w, adj := h }
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).darts = (cons h✝ p✝).darts.concat { fst := w✝, snd := w, adj := h }
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').darts = nil.darts ++ p'.darts

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').darts = p✝.darts ++ p'.darts
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').darts = (cons h✝ p✝).darts ++ p'.darts

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').darts = nil.darts ++ p'.darts

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').darts = p✝.darts ++ p'.darts
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').darts = (cons h✝ p✝).darts ++ p'.darts