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

Goal state before:
pp: case refine_2.refine_2
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.getVert (s.length + p₁.length) = w

pp: case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂ = (((p₂.take s.length).copy ⋯ ⋯).append p₁).append ((p₂.drop (s.length + p₁.length)).copy ?refine_2.refine_2 ⋯)

Tactic:
·

Goal state after:
case refine_2.refine_2
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.getVert (s.length + p₁.length) = w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
·

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ s.length + p₁.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case head
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
hx : ¬v = v
⊢ v ∈ p.support

pp: case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support

Tactic:
·

Goal state after:
case head
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
hx : ¬v = v
⊢ v ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support

Tactic:
·

Goal state after:
case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: 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.concat h).reverse ≍ concatRecAux Hnil Hconcat (cons ⋯ p.reverse)

pp: 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 (cons ⋯ p.reverse) ≍ Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)

Tactic:
·

Goal state after:
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.concat h).reverse ≍ concatRecAux Hnil Hconcat (cons ⋯ p.reverse)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: 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 (cons ⋯ p.reverse) ≍ Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)

Tactic:
·

Goal state after:
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 (cons ⋯ p.reverse) ≍ Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' h : G.Adj v' w
he : nil.concat h = nil.concat h'
⊢ ∃ (hv : v' = v'), nil.copy ⋯ hv = nil

pp: case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝

Tactic:
·

Goal state after:
case nil.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' h : G.Adj v' w
he : nil.concat h = nil.concat h'
⊢ ∃ (hv : v' = v'), nil.copy ⋯ hv = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ (nil.takeUntil u h).append (nil.dropUntil u h) = nil

pp: case cons
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✝
h : u ∈ (cons h✝ p✝).support
⊢ ((cons h✝ p✝).takeUntil u h).append ((cons h✝ p✝).dropUntil u h) = cons h✝ p✝

Tactic:
·

Goal state after:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ (nil.takeUntil u h).append (nil.dropUntil u h) = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝

Tactic:
·

Goal state after:
case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons
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✝
h : u ∈ (cons h✝ p✝).support
⊢ ((cons h✝ p✝).takeUntil u h).append ((cons h✝ p✝).dropUntil u h) = cons h✝ p✝

Tactic:
·

Goal state after:
case cons
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✝
h : u ∈ (cons h✝ p✝).support
⊢ ((cons h✝ p✝).takeUntil u h).append ((cons h✝ p✝).dropUntil u h) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
h✝ : G.Adj u v✝
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝

pp: case cons.tail
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
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝

Tactic:
·

Goal state after:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
h✝ : G.Adj u v✝
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.tail
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
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝

Tactic:
·

Goal state after:
case cons.tail
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
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
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]? = some p₁.darts[i]

pp: case refine_2
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₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]

Tactic:
·

Goal state after:
case refine_1
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]? = some p₁.darts[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (p✝.concat h) = nil.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil

pp: case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
·

Goal state after:
case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (p✝.concat h) = nil.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w = a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

pp: case neg
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w = a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
·

Goal state after:
case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ q r, p = q.append r

pp: case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ q r, p = q.append r
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2
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₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]

Tactic:
·

Goal state after:
case refine_2
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₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ List.count u (nil.takeUntil u h).support = 1

pp: case cons
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
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1

Tactic:
·

Goal state after:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ List.count u (nil.takeUntil u h).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons
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
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1

Tactic:
·

Goal state after:
case cons
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
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

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

pp: case cons.tail
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
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

Tactic:
·

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

Goal state before:
pp: case cons.tail
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
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

Tactic:
·

Goal state after:
case cons.tail
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
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case pos
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₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
hi' : i = p₁.length
⊢ p₂.support[i + k] = p₁.support[i]

pp: case neg
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₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
hi' : ¬i = p₁.length
⊢ p₂.support[i + k] = p₁.support[i]

Tactic:
·

Goal state after:
case pos
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₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
hi' : i = p₁.length
⊢ p₂.support[i + k] = p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.tail
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
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

Tactic:
simp! only
      split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ List.count u (p.takeUntil u h).support = 1

Tactic:
induction p
  · rw [mem_support_nil_iff] at h
    subst u
    simp
  · cases h
    · simp
    · simp! only
      split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x v✝ w✝ : V
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v✝
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

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

Tactic:
·

Goal state after:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x v✝ w✝ : V
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v✝
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

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

Tactic:
·

Goal state after:
case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1