Theorem: Fin.cons.nnnorm (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
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ ‖cons a b‖₊ = ‖a‖₊ ⊔ ‖b‖₊
Tactic:
simp [Pi.nnnorm_def, Fin.univ_succ, Function.comp_def]
State after:
no goals