Theorem: Function.update_head (ExponentialRamsey/Prereq/Mathlib/Data/Fin/VecNotation.lean)

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ update (vecCons x t) 0 y = vecCons y t
Tactic:
rw [funext_iff, Fin.forall_fin_succ]
State after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ update (vecCons x t) 0 y 0 = vecCons y t 0 ∧
    ∀ (i_1 : Fin i), update (vecCons x t) 0 y (succ i_1) = vecCons y t (succ i_1)

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ update (vecCons x t) 0 y 0 = vecCons y t 0 ∧
    ∀ (i_1 : Fin i), update (vecCons x t) 0 y (succ i_1) = vecCons y t (succ i_1)
Tactic:
refine' ⟨rfl, fun j => _⟩
State after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x t) 0 y (succ j) = vecCons y t (succ j)

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x t) 0 y (succ j) = vecCons y t (succ j)
Tactic:
rw [update_noteq]
State after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ vecCons x t (succ j) = vecCons y t (succ j)

case h
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ j ≠ 0

State before:
case h
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ j ≠ 0
Tactic:
exact succ_ne_zero j
State after:
no goals

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ vecCons x t (succ j) = vecCons y t (succ j)
Tactic:
simp only [vecCons, Fin.cons_succ]
State after:
no goals