Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing_apply (ForML/HasTemperateGrowth.lean)

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => (ContinuousMultilinearMap.mkPiRing ℝ ι x) m
Tactic:
simp only [ContinuousMultilinearMap.mkPiRing_apply]
State after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => (∏ i : ι, m i) • x

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => (∏ i : ι, m i) • x
Tactic:
refine .smul_const ?_ x
State after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => ∏ i : ι, m i

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => ∏ i : ι, m i
Tactic:
exact .prod Finset.univ fun i _ ↦ hasTemperateGrowth_clm (.proj (φ := fun _ ↦ ℝ) i)
State after:
no goals