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

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

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

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

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

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

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