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

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

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

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

case h
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1

State before:
case h
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1
Tactic:
exact (succ_injective _).ne (Fin.succ_ne_zero _)
State after:
no goals

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