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
n : ℕ
α : Fin (Nat.succ n) → Type u_5
δ₁ : Fin (Nat.succ n) → Type u_6
f : (i : Fin (Nat.succ n)) → α i → δ₁ i
x : α 0
p : (i : Fin n) → α (succ i)
⊢ (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
n : ℕ
α : Fin (Nat.succ n) → Type u_5
δ₁ : Fin (Nat.succ n) → Type u_6
f : (i : Fin (Nat.succ n)) → α i → δ₁ i
x : α 0
p : (i : Fin n) → α (succ i)
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
n : ℕ
α : Fin (Nat.succ n) → Type u_5
δ₁ : Fin (Nat.succ n) → Type u_6
f : (i : Fin (Nat.succ n)) → α i → δ₁ i
x : α 0
p : (i : Fin n) → α (succ i)
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