awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
refine_2 :
  ∀ (bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞)
    (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
    (h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))) (f_measurable : AEStronglyMeasurable f μ),
    let b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a);
    ∀ (hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a)
      (h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)),
      ∫⁻ (a : α), b a ∂μ ≠ ∞
refine_2₁ : 0 ≤ᶠ[ae μ] bound
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞

Tactic:
rw [hasFiniteIntegral_iff_ofReal] at bound_hasFiniteIntegral

Premises used: MeasureTheory.hasFiniteIntegral_iff_ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
hr : Ne (α := ℝ≥0∞) 2 ∞
⊢ ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ

Tactic:
rw [lintegral_const_mul']

Premises used: MeasureTheory.lintegral_const_mul'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ ≠ ∞

Tactic:
mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne

Premises used: ENNReal.mul_ne_top, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
b₁ : ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞

Tactic:
calc
        ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ := by
          rw [lintegral_const_mul']
          finiteness
        _ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne

Premises used: ENNReal.mul_ne_top, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h_1 : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
a : α
h : ‖F 0 a‖ ≤ bound a
⊢ 0 a ≤ bound a

Tactic:
le_trans (norm_nonneg _) h

Premises used: norm_nonneg, le_trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖F 0 a‖ ≤ bound a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ bound x) x} x}
      a
h₂ h₃ : ∀ (a : α) (h : ‖F 0 a‖ ≤ bound a), 0 a ≤ bound a
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
filter_upwards [h_bound 0] with _ h using le_trans (norm_nonneg _) h

Premises used: OfNat.ofNat, norm_nonneg, le_trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)

Tactic:
h
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖max (f x) 0‖ ≤ ‖f x‖

Tactic:
simp [abs_le, le_abs_self]

Premises used: le_abs_self, abs_le
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖min (f x) 0‖ ≤ ‖f x‖

Tactic:
simpa [abs_le] using neg_abs_le _

Premises used: abs_le, neg_abs_le
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c • f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ

Tactic:
lintegral_mono fun i ↦ enorm_smul_le

Premises used: MeasureTheory.lintegral_mono, enorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
rw : ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
hr : ‖c‖ₑ ≠ ∞
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞

Tactic:
rw [lintegral_const_mul']

Premises used: MeasureTheory.lintegral_const_mul'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
mul_lt_top coe_lt_top hf

Premises used: ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ ≠ ∞

Tactic:
coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
exacts [mul_lt_top coe_lt_top hf, coe_ne_top]

Premises used: ENNReal.mul_lt_top, ENNReal.coe_lt_top, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
a : ∫⁻ (a : α), ‖c‖ₑ * ‖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 hf, coe_ne_top]

Premises used: MeasureTheory.lintegral_mono, enorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c • f a‖ₑ ∂μ = ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ

Tactic:
lintegral_congr fun i ↦ enorm_smul _ _

Premises used: enorm_smul, MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
rw : ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
hr : ‖c‖ₑ ≠ ∞
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞

Tactic:
rw [lintegral_const_mul']

Premises used: MeasureTheory.lintegral_const_mul'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
mul_lt_top coe_lt_top hf

Premises used: ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ ≠ ∞

Tactic:
coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
exacts [mul_lt_top coe_lt_top hf, coe_ne_top]

Premises used: ENNReal.mul_lt_top, ENNReal.coe_lt_top, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
a : ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ∞

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

Premises used: enorm_smul, MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
obtain : ∀ (c : 𝕜ˣ), HasFiniteIntegral ((↑c : 𝕜) • f) μ ↔ HasFiniteIntegral f μ
⊢ HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
obtain ⟨c, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
mp : HasFiniteIntegral ((↑c : 𝕜) • f) μ → HasFiniteIntegral f μ
mpr : HasFiniteIntegral f μ → HasFiniteIntegral ((↑c : 𝕜) • f) μ
⊢ HasFiniteIntegral ((↑c : 𝕜) • f) μ ↔ HasFiniteIntegral f μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
h : HasFiniteIntegral ((↑c : 𝕜) • f) μ
⊢ HasFiniteIntegral f μ

Tactic:
simpa only [smul_smul, Units.inv_mul, one_smul] using h.smul ((c⁻¹ : 𝕜ˣ) : 𝕜)

Premises used: Units.val, Units.inv_mul, smul_smul, one_smul, Inv.inv, MeasureTheory.HasFiniteIntegral.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f μ → HasFiniteIntegral ((↑c : 𝕜) • f) μ

Tactic:
HasFiniteIntegral.smul _

Premises used: MeasureTheory.HasFiniteIntegral.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f μ → HasFiniteIntegral ((↑c : 𝕜) • f) μ

Tactic:
exact HasFiniteIntegral.smul _

Premises used: MeasureTheory.HasFiniteIntegral.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_7
inst : NormedRing 𝕜
f : α → 𝕜
h : HasFiniteIntegral f μ
c : 𝕜
⊢ HasFiniteIntegral.{u_1, u_7} (ε := 𝕜) (fun (x : α) ↦ c * f x) μ

Tactic:
h.smul c

Premises used: MeasureTheory.HasFiniteIntegral.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_7
inst : NormedRing 𝕜
f : α → 𝕜
h : HasFiniteIntegral f μ
c : 𝕜
⊢ HasFiniteIntegral.{u_1, u_7} (ε := 𝕜) (fun (x : α) ↦ f x * c) μ

Tactic:
h.smul (MulOpposite.op c)

Premises used: MeasureTheory.HasFiniteIntegral.smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
inst : ENorm ε
inst_1 : MeasurableSingletonClass α
f : α → ε
⊢ @HasFiniteIntegral _ _ _ m f Measure.count ↔ LT.lt (α := ℝ≥0∞) (∑' (x : α), ‖f x‖ₑ) ∞

Tactic:
simp only [hasFiniteIntegral_iff_enorm, lintegral_count]

Premises used: MeasureTheory.lintegral_count, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
⊢ @HasFiniteIntegral _ _ _ m f Measure.count ↔ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
simp only [hasFiniteIntegral_iff_enorm, enorm, lintegral_count, lt_top_iff_ne_top,
    tsum_coe_ne_top_iff_summable, ← summable_coe, coe_nnnorm]

Premises used: NNReal.summable_coe, MeasureTheory.lintegral_count, lt_top_iff_ne_top, ENorm.enorm, ENNReal.tsum_coe_ne_top_iff_summable, coe_nnnorm, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
s : Set α
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
lt_of_le_of_lt ?_ h

Premises used: lt_of_le_of_lt, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
s : Set α
refine : ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
refine lt_of_le_of_lt ?_ h

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
s : Set α
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simpa [Measure.restrict_univ] using lintegral_mono_set (subset_univ s)

Premises used: Set.subset_univ, MeasureTheory.lintegral_mono_set, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
simp_rw : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
simp_rw₁ : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
simp_rw₂ : AEStronglyMeasurable f μ ∧ eLpNorm f 1 μ < ∞ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
⊢ MemLp f 1 μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, hasFiniteIntegral_iff_enorm, MemLp, eLpNorm_one_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, MeasureTheory.Integrable, MeasureTheory.MemLp, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : MeasurableSpace ε
inst_3 : BorelSpace ε
inst_4 : PseudoMetrizableSpace ε
f : α → ε
hf : Integrable f μ
⊢ AEMeasurable f μ

Tactic:
hf.aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral f μ

Tactic:
hf.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
ε' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
⊢ Integrable f μ

Tactic:
⟨hf, hg.hasFiniteIntegral.mono_enorm h⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.mono_enorm, And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
⊢ Integrable f μ

Tactic:
⟨hf, hg.hasFiniteIntegral.mono h⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.mono, And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ Integrable f μ

Tactic:
⟨hf, hg.hasFiniteIntegral.mono_nonneg hnonneg h⟩

Premises used: MeasureTheory.HasFiniteIntegral.mono_nonneg, MeasureTheory.Integrable, And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
g : α → ℝ≥0∞
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a
⊢ Integrable f μ

Tactic:
⟨hf, hg.hasFiniteIntegral.mono_enorm h⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.mono_enorm, And.intro, MeasureTheory.Integrable.hasFiniteIntegral