Theorem: ContinuousLinearMap.invcoprod_fst_apply (ForML/ContinuousLinearMapCo.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ × M₂ →L[R] F
x : M₁
⊢ (invcoprod f).1 x = f (x, 0)
Tactic:
simp [invcoprod]
State after:
no goals