-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜)
    {f : α → β} : HasFiniteIntegral f μ → HasFiniteIntegral (c • f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ HasFiniteIntegral f μ → HasFiniteIntegral (c • f) μ

Tactic:
simp only [HasFiniteIntegral]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤ → ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

case hr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ‖c‖ₑ ≠ ⊤

Tactic:
exacts [mul_lt_top coe_lt_top hfi, coe_ne_top]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤ → ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ⊤

Tactic:
intro hfi

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ⊤

Tactic:
calc
  ∫⁻ a : α, ‖c • f a‖ₑ ∂μ ≤ ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_mono fun i ↦ enorm_smul_le
  _ < ∞ := by
    rw [lintegral_const_mul']
    exacts [mul_lt_top coe_lt_top hfi, coe_ne_top]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ⊤

Tactic:
rw [lintegral_const_mul']

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

case hr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
⊢ ‖c‖ₑ ≠ ⊤