Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMap_right (ForML/ContinuousMultilinearMap.lean)

State before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ Continuous fun f => compContinuousLinearMap g f
Tactic:
simp only [← compContinuousLinearMapL_apply]
State after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ Continuous fun f => (compContinuousLinearMapL f) g

State before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ Continuous fun f => (compContinuousLinearMapL f) g
Tactic:
exact .clm_apply (continuous_compContinuousLinearMapL G) continuous_const
State after:
no goals