Theorem: IsBump.integrable_continuous_mul (ForML/Bump.lean)

State before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (f * g)
Tactic:
rw [mul_comm]
State after:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (g * f)

State before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (g * f)
Tactic:
apply integrable_mul_continuous <;> assumption
State after:
no goals