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 : α → β
⊢ HasFiniteIntegral (-f) μ ↔ HasFiniteIntegral f μ

Tactic:
⟨fun h => neg_neg f ▸ h.neg, HasFiniteIntegral.neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, MeasureTheory.HasFiniteIntegral.neg
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
⊢ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ HasFiniteIntegral f μ

Tactic:
hasFiniteIntegral_congr'_enorm <| Eventually.of_forall fun x => enorm_enorm (f x)

Premises used: Filter.Eventually.of_forall, MeasureTheory.hasFiniteIntegral_congr'_enorm, enorm_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ HasFiniteIntegral f μ

Tactic:
hasFiniteIntegral_congr' <| Eventually.of_forall fun x => norm_norm (f x)

Premises used: Filter.Eventually.of_forall, norm_norm, MeasureTheory.hasFiniteIntegral_congr'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Subsingleton α
inst_2 : IsFiniteMeasure μ
f : α → β
⊢ HasFiniteIntegral f μ

Tactic:
.of_finite

Premises used: MeasureTheory.HasFiniteIntegral.of_finite
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsEmpty α
f : α → β
⊢ HasFiniteIntegral f μ

Tactic:
.of_finite

Premises used: MeasureTheory.HasFiniteIntegral.of_finite
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : Subsingleton ε
f : α → ε
⊢ HasFiniteIntegral f μ

Tactic:
hasFiniteIntegral_zero _ _ |>.congr <| .of_forall fun _ ↦ Subsingleton.elim _ _

Premises used: MeasureTheory.hasFiniteIntegral_zero, Filter.Eventually.of_forall, MeasureTheory.HasFiniteIntegral.congr, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
x : α
rw rw₁ : ENNReal.ofReal (f x).toReal = ENNReal.ofReal (f x).toReal
⊢ ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal

Tactic:
rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]

Premises used: ENNReal.toReal_nonneg, Real.enorm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal

Tactic:
have h x : ‖(f x).toReal‖ₑ = .ofReal (f x).toReal := by
    rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
simp_rw : ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, h]

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ∞

Tactic:
lt_of_le_of_lt (lintegral_mono fun x => ?_) (lt_top_iff_ne_top.2 hf)

Premises used: Iff.mpr, lt_of_le_of_lt, lt_top_iff_ne_top, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
refine : ∀ (x : α), ENNReal.ofReal (f x).toReal ≤ f x
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ∞

Tactic:
refine lt_of_le_of_lt (lintegral_mono fun x => ?_) (lt_top_iff_ne_top.2 hf)

Premises used: Iff.mpr, lt_of_le_of_lt, lt_top_iff_ne_top, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
pos : ∀ (hfx : f x = ∞), ENNReal.ofReal (f x).toReal ≤ f x
neg : ∀ (hfx : ¬f x = ∞), ENNReal.ofReal (f x).toReal ≤ f x
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
by_cases hfx : f x = ∞
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
simp [hfx]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ f x ≠ ∞

Tactic:
hfx
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
neg : ∀ (fx : ℝ≥0) (h : (↑fx : ℝ≥0∞) = f x), ENNReal.ofReal (↑fx : ℝ≥0∞).toReal ≤ (↑fx : ℝ≥0∞)
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
lift f x to ℝ≥0 using hfx with fx h
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_1 : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
fx : ℝ≥0
h : (↑fx : ℝ≥0∞) = f x
⊢ ENNReal.ofReal (↑fx : ℝ≥0∞).toReal ≤ (↑fx : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
h : ∀ (x : α) (hx : f x ≠ ∞), ENNReal.ofReal (f x).toReal = f x
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x

Tactic:
filter_upwards [hf] with x hx
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hx : f x ≠ ∞
⊢ ENNReal.ofReal (f x).toReal = f x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x

Tactic:
have : ∀ᵐ x ∂μ, .ofReal (f x).toReal = f x := by filter_upwards [hf] with x hx; simp [hx]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
simp [hasFiniteIntegral_iff_enorm, Real.enorm_of_nonneg ENNReal.toReal_nonneg,
    lintegral_congr_ae this, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_nonneg, lt_top_iff_ne_top, MeasureTheory.lintegral_congr_ae, Real.enorm_of_nonneg, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))

Tactic:
isFiniteMeasure_withDensity ((lintegral_mono fun x => ?_).trans_lt hfi).ne

Premises used: MeasureTheory.isFiniteMeasure_withDensity, MeasureTheory.lintegral_mono, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
refine : ∀ (x : α), ENNReal.ofReal (f x) ≤ ‖f x‖ₑ
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))

Tactic:
refine isFiniteMeasure_withDensity ((lintegral_mono fun x => ?_).trans_lt hfi).ne

Premises used: MeasureTheory.isFiniteMeasure_withDensity, MeasureTheory.lintegral_mono, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
x : α
⊢ ENNReal.ofReal (f x) ≤ ‖f x‖ₑ

Tactic:
Real.ofReal_le_enorm (f x)

Premises used: Real.ofReal_le_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
x : α
⊢ ENNReal.ofReal (f x) ≤ ‖f x‖ₑ

Tactic:
exact Real.ofReal_le_enorm (f x)

Premises used: Real.ofReal_le_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
bound : α → ℝ
h : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
fun n =>
  (h n).mono fun _ h => ENNReal.ofReal_le_ofReal h

Premises used: ENNReal.ofReal_le_ofReal, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ)

Tactic:
h.mono fun _ h ↦ Tendsto.comp (Continuous.tendsto continuous_enorm _) h

Premises used: continuous_enorm, Filter.Eventually.mono, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ‖F n a‖ₑ) atTop (𝓝 ‖f a‖ₑ)

Tactic:
ae_tendsto_enorm h

Premises used: MeasureTheory.ae_tendsto_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
h₁ : ∀ (x : α) (x_1 : ℕ), ENNReal.ofReal ‖F x_1 x‖ = ‖F x_1 x‖ₑ
h₂ : ∀ (x : α), ENNReal.ofReal ‖f x‖ = ‖f x‖ₑ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))

Tactic:
convert! ae_tendsto_enorm h

Premises used: MeasureTheory.ae_tendsto_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
x : α
x_1 : ℕ
⊢ ENNReal.ofReal ‖F x_1 x‖ = ‖F x_1 x‖ₑ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
x : α
⊢ ENNReal.ofReal ‖f x‖ = ‖f x‖ₑ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
have F_le_bound := all_ae_norm_ofReal_F_le_bound h_bound
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
rw [← ae_all_iff] at F_le_bound

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
apply :
  ∀ (x : α),
    Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n x‖) atTop (𝓝 (ENNReal.ofReal ‖f x‖)) →
      (∀ (i : ℕ), ENNReal.ofReal ‖F i x‖ ≤ ENNReal.ofReal (bound x)) → ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (bound x)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
apply F_le_bound.mp ((ae_tendsto_ofReal_norm h_lim).mono _)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, MeasureTheory.ae_tendsto_ofReal_norm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
F_le_bound_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
a : α
tendsto_norm : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))
F_le_bound : ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
le_of_tendsto' tendsto_norm F_le_bound

Premises used: le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
F_le_bound_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
a : α
tendsto_norm : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))
F_le_bound : ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
exact le_of_tendsto' tendsto_norm F_le_bound

Premises used: le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a

Tactic:
rw [← ae_all_iff] at h_bound

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))
h_bound₁ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))

Tactic:
rw [← ae_all_iff] at h_bound

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))
apply :
  ∀ (x : α),
    Tendsto (fun (n : ℕ) ↦ ‖F' n x‖ₑ) atTop (𝓝 ‖f' x‖ₑ) → (∀ (i : ℕ), ‖F' i x‖ₑ ≤ bound' x) → ‖f' x‖ₑ ≤ bound' x
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a

Tactic:
apply h_bound.mp ((ae_tendsto_enorm h_lim).mono _)

Premises used: MeasureTheory.ae_tendsto_enorm, Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))
a : α
tendsto_norm : Tendsto (fun (n : ℕ) ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ)
h_bound : ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
⊢ ‖f' a‖ₑ ≤ bound' a

Tactic:
le_of_tendsto' tendsto_norm h_bound

Premises used: le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F' n a) atTop (𝓝 (f' a))
a : α
tendsto_norm : Tendsto (fun (n : ℕ) ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ)
h_bound : ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
⊢ ‖f' a‖ₑ ≤ bound' a

Tactic:
exact le_of_tendsto' tendsto_norm h_bound

Premises used: le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
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))
⊢ ∫⁻ (a : α), ‖f' a‖ₑ ∂μ ≤ ∫⁻ (a : α), bound' a ∂μ

Tactic:
lintegral_mono_ae <| ae_enorm_le_bound h_bound h_lim

Premises used: MeasureTheory.lintegral_mono_ae, MeasureTheory.ae_enorm_le_bound
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
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))
⊢ ∫⁻ (a : α), bound' a ∂μ < ∞

Tactic:
bound_hasFiniteIntegral

Premises used: MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
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))
⊢ ∫⁻ (a : α), ‖f' a‖ₑ ∂μ < ∞

Tactic:
calc
    (∫⁻ a, ‖f' a‖ₑ ∂μ) ≤ ∫⁻ a, bound' a ∂μ :=
      lintegral_mono_ae <| ae_enorm_le_bound h_bound h_lim
    _ < ∞ := bound_hasFiniteIntegral

Premises used: MeasureTheory.lintegral_mono_ae, MeasureTheory.ae_enorm_le_bound, ENorm.enorm, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
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))
rw : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞
⊢ HasFiniteIntegral f μ

Tactic:
rw [hasFiniteIntegral_iff_norm]

Premises used: MeasureTheory.hasFiniteIntegral_iff_norm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
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))
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ

Tactic:
lintegral_mono_ae <| ae_norm_ofReal_f_le_bound h_bound h_lim

Premises used: MeasureTheory.lintegral_mono_ae, MeasureTheory.ae_norm_ofReal_f_le_bound
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
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))
rw : HasFiniteIntegral bound μ
rw₁ : 0 ≤ᶠ[ae μ] bound
⊢ ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞

Tactic:
rw [← hasFiniteIntegral_iff_ofReal]

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 : α → ℝ
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))
⊢ HasFiniteIntegral bound μ

Tactic:
bound_hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
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))
⊢ HasFiniteIntegral bound μ

Tactic:
exact bound_hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
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))
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
(h_bound 0).mono fun a h => le_trans (norm_nonneg _) h

Premises used: Filter.Eventually.mono, Filter.EventuallyLE, 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 : α → ℝ
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))
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h

Premises used: Filter.Eventually.mono, OfNat.ofNat, norm_nonneg, le_trans