Theorem: Fin.map_cons' (ForML/ContinuousMultilinearMap.lean)

State before:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n✝ : ℕ
E : Fin n✝ → Type u_2
inst✝⁵ : (i : Fin n✝) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n✝) → NormedSpace 𝕜 (E i)
E₁ : Fin n✝ → Type u_3
inst✝³ : (i : Fin n✝) → NormedAddCommGroup (E₁ i)
inst✝² : (i : Fin n✝) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : Type u_5
δ₁ : Type u_6
n : ℕ
f : Fin (Nat.succ n) → α → δ₁
x : α
p : Fin n → α
⊢ (fun i => f i (cons x p i)) = cons (f 0 x) fun i => f (succ i) (p i)
Tactic:
ext i
State after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n✝ : ℕ
E : Fin n✝ → Type u_2
inst✝⁵ : (i : Fin n✝) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n✝) → NormedSpace 𝕜 (E i)
E₁ : Fin n✝ → Type u_3
inst✝³ : (i : Fin n✝) → NormedAddCommGroup (E₁ i)
inst✝² : (i : Fin n✝) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : Type u_5
δ₁ : Type u_6
n : ℕ
f : Fin (Nat.succ n) → α → δ₁
x : α
p : Fin n → α
i : Fin (Nat.succ n)
⊢ f i (cons x p i) = cons (f 0 x) (fun i => f (succ i) (p i)) i

State before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n✝ : ℕ
E : Fin n✝ → Type u_2
inst✝⁵ : (i : Fin n✝) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n✝) → NormedSpace 𝕜 (E i)
E₁ : Fin n✝ → Type u_3
inst✝³ : (i : Fin n✝) → NormedAddCommGroup (E₁ i)
inst✝² : (i : Fin n✝) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : Type u_5
δ₁ : Type u_6
n : ℕ
f : Fin (Nat.succ n) → α → δ₁
x : α
p : Fin n → α
i : Fin (Nat.succ n)
⊢ f i (cons x p i) = cons (f 0 x) (fun i => f (succ i) (p i)) i
Tactic:
cases i using Fin.cases <;> simp
State after:
no goals