Theorem: Nat.Arith₁.tail (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f v.tail
Tactic:
rw[←ofFn_get v.tail]
State after:
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)

State before:
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)
Tactic:
congr
State after:
case e_a.e_a
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ (fun i => v.get i.succ) = v.tail.get

State before:
case e_a.e_a
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ (fun i => v.get i.succ) = v.tail.get
Tactic:
funext i
State after:
case e_a.e_a.h
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
i : Fin n
⊢ v.get i.succ = v.tail.get i

State before:
case e_a.e_a.h
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
i : Fin n
⊢ v.get i.succ = v.tail.get i
Tactic:
simp
State after:
no goals