Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).getVert 0 = nil.getVert (min 0 0)

pp: case nil.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take 0).getVert (n✝ + 1) = nil.getVert (min 0 (n✝ + 1))

pp: case nil.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert 0 = nil.getVert (min (n✝ + 1) 0)

pp: case nil.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝¹ n✝ : ℕ
⊢ (nil.take (n✝¹ + 1)).getVert (n✝ + 1) = nil.getVert (min (n✝¹ + 1) (n✝ + 1))

pp: case cons.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
⊢ ((cons h✝ p✝).take 0).getVert 0 = (cons h✝ p✝).getVert (min 0 0)

pp: case cons.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take 0).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min 0 (n✝ + 1))

pp: case cons.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert 0 = (cons h✝ p✝).getVert (min (n✝ + 1) 0)

pp: case cons.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝¹ n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝¹ + 1)).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min (n✝¹ + 1) (n✝ + 1))

Tactic:
<;>

Goal state after:
case nil.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).getVert 0 = nil.getVert (min 0 0)

case nil.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take 0).getVert (n✝ + 1) = nil.getVert (min 0 (n✝ + 1))

case nil.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert 0 = nil.getVert (min (n✝ + 1) 0)

case nil.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝¹ n✝ : ℕ
⊢ (nil.take (n✝¹ + 1)).getVert (n✝ + 1) = nil.getVert (min (n✝¹ + 1) (n✝ + 1))

case cons.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
⊢ ((cons h✝ p✝).take 0).getVert 0 = (cons h✝ p✝).getVert (min 0 0)

case cons.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take 0).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min 0 (n✝ + 1))

case cons.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert 0 = (cons h✝ p✝).getVert (min (n✝ + 1) 0)

case cons.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝¹ n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝¹ + 1)).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min (n✝¹ + 1) (n✝ + 1))