Theorem: piFinSuccCastSucc_apply (Controlbits/Equivs.lean)

State before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ piFinSuccCastSucc v = ((v 0, v (last (n + 1))), v ∘ fun i => i.castSucc.succ)
Tactic:
simp_rw [Prod.ext_iff, Function.funext_iff]
State after:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ ((piFinSuccCastSucc v).1.1 = v 0 ∧ (piFinSuccCastSucc v).1.2 = v (last (n + 1))) ∧
    ∀ (a : Fin n), (piFinSuccCastSucc v).2 a = (v ∘ fun i => i.castSucc.succ) a

State before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ ((piFinSuccCastSucc v).1.1 = v 0 ∧ (piFinSuccCastSucc v).1.2 = v (last (n + 1))) ∧
    ∀ (a : Fin n), (piFinSuccCastSucc v).2 a = (v ∘ fun i => i.castSucc.succ) a
Tactic:
refine' ⟨⟨rfl, rfl⟩, fun _ => _⟩
State after:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ (piFinSuccCastSucc v).2 x✝ = (v ∘ fun i => i.castSucc.succ) x✝

State before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ (piFinSuccCastSucc v).2 x✝ = (v ∘ fun i => i.castSucc.succ) x✝
Tactic:
simp_rw [piFinSuccCastSucc, Equiv.instTrans_trans, Equiv.trans_apply, Equiv.prodCongr_apply,
Equiv.piFinSuccAbove_apply, extractNth, succAbove_last]
State after:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ ((Equiv.prodAssoc α α (Fin n → α)).symm
          (Prod.map (⇑(Equiv.refl α)) (fun f => (f (last n), fun j => f j.castSucc)) ((Equiv.piFinSucc (n + 1) α) v))).2
      x✝ =
    (v ∘ fun i => i.castSucc.succ) x✝

State before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ ((Equiv.prodAssoc α α (Fin n → α)).symm
          (Prod.map (⇑(Equiv.refl α)) (fun f => (f (last n), fun j => f j.castSucc)) ((Equiv.piFinSucc (n + 1) α) v))).2
      x✝ =
    (v ∘ fun i => i.castSucc.succ) x✝
Tactic:
rfl
State after:
no goals