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

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1) = vecCons y (vecCons x t)
Tactic:
rw [funext_iff]
State after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ ∀ (a : Fin (Nat.succ (Nat.succ i))), (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) a = vecCons y (vecCons x t) a

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ ∀ (a : Fin (Nat.succ (Nat.succ i))), (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) a = vecCons y (vecCons x t) a
Tactic:
simp only [forall_fin_succ]
State after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) 0 = vecCons y (vecCons x t) 0 ∧
    (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ 0) = vecCons y (vecCons x t) (succ 0) ∧
      ∀ (i_1 : Fin i),
        (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ i_1)) = vecCons y (vecCons x t) (succ (succ i_1))

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

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ j)) = vecCons y (vecCons x t) (succ (succ j))
Tactic:
simp only [vecCons, cons_succ, comp_apply]
State after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ cons x (cons y t) (↑(Equiv.swap 0 1) (succ (succ j))) = t j

State before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ cons x (cons y t) (↑(Equiv.swap 0 1) (succ (succ j))) = t j
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne, cons_succ, cons_succ]
State after:
case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 0

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

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

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