awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ).toReal =
    (∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ).toReal
have e_a : ∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ =
  ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ =
    ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ
have e_a : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ) fun (a : α) ↦
  ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ
Tactic: rw [lintegral_congr_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ) fun (a : α) ↦
    ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ
have h : ∀ (a : α) (ha : (↑(↑(f - g) : α →ₘ[μ] β) : α → β) a = ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) a),
  ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ = ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ
Tactic: filter_upwards [Lp.coeFn_sub f g] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ
have rw : ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ ≠ ∞
Tactic: rw [norm_def, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ
have simp_rw : ∫⁻ (x : α), edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) x) 0 ∂μ =
  ∫⁻ (x : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x) 0 ∂μ
Tactic: simp_rw [ofReal_norm_eq_lintegral, ← edist_zero_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (x : α), edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) x) 0 ∂μ =
    ∫⁻ (x : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x) 0 ∂μ
have h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0) fun (a : α) ↦
  edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0) fun (a : α) ↦
    edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0
have h : ∀ (a : α) (ha : (↑(↑(f - g) : α →ₘ[μ] β) : α → β) a = ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) a),
  edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0 =
    edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0
Tactic: filter_upwards [Lp.coeFn_sub f g] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ₑ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
have simp : eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
Tactic: simp only [Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have rw : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: rw [norm_toL1, lintegral_norm_eq_lintegral_edist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
rw : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have rw₁ : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
Tactic: rw [norm_toL1, lintegral_norm_eq_lintegral_edist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
have simp_rw : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: simp_rw [norm_toL1, edist_zero_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ edist (toL1 f hf) (toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
have simp : (if Eq (α := ℝ≥0∞) 1 ∞ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ‖f a - g a‖ₑ ∂μ) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
Tactic: simp only [toL1, Lp.edist_toLp_toLp, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm,
    Pi.sub_apply, toReal_one, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
have simp : eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
Tactic: simp only [edist_zero_right, Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ
have rw : ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
Tactic: rw [← lintegral_add_left' (hf.edist hh)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
have refine : ∀ (a : α), edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
Tactic: refine lintegral_mono fun a => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᶠ[ae μ] f
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
have rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᶠ[ae μ] f
rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
have rw₁ : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
⊢ HasFiniteIntegral f μ
have hg₁ : ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞
Tactic: simp only [hasFiniteIntegral_iff_enorm] at *
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ HasFiniteIntegral f μ
have refine : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
Tactic: refine HasFiniteIntegral.mono hg ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
have h₁ : ∀ (a : α) (hn : 0 ≤ f a) (ha : f a ≤ g a), ‖f a‖ ≤ ‖g a‖
Tactic: filter_upwards [hnonneg, h] with a hn ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ ‖f a‖ ≤ ‖g a‖
have h₁ : |f a| ≤ |g a|
Tactic: apply norm_le_norm_of_abs_le_abs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ |f a| ≤ |g a|
have h₁ : f a ≤ |g a|
Tactic: rwa [abs_of_nonneg hn, abs_of_nonneg (hn.trans ha)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ HasFiniteIntegral X μ
have this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
Tactic: have : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ⊤ := by simp [ha, hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
⊢ HasFiniteIntegral X μ
have apply : ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
Tactic: apply (hasFiniteIntegral_const_enorm this (μ := μ)).mono'_enorm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ X x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x ≤ b) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖X a_4‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ) x} x}
          x}
    a_1
Tactic: filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω h₁ h₂ using by simp [h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ X x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x ≤ b) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖X a_4‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ) x} x}
            x}
      a_1
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
have h₂ : ∀ (a_1 : α), a ≤ X a_1 → X a_1 ≤ b → ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
Tactic: filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω h₁ h₂ using by simp [h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ HasFiniteIntegral X μ
have apply : ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ max ‖a‖ ‖b‖
Tactic: apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ max ‖a‖ ‖b‖
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ X x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x ≤ b) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖X a_4‖ ≤ max ‖a‖ ‖b‖) x} x}
          x}
    a_1
Tactic: filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ X x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x ≤ b) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖X a_4‖ ≤ max ‖a‖ ‖b‖) x} x}
            x}
      a_1
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ max ‖a‖ ‖b‖
have h₂ : ∀ (a_1 : α), a ≤ X a_1 → X a_1 ≤ b → ‖X a_1‖ ≤ max ‖a‖ ‖b‖
Tactic: filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
hμ : HasFiniteIntegral f μ
hν : HasFiniteIntegral f ν
⊢ HasFiniteIntegral f (μ + ν)
have simp : ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞
Tactic: simp only [HasFiniteIntegral, lintegral_add_measure] at *
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ HasFiniteIntegral f (c • μ)
have simp : c • ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Tactic: simp only [HasFiniteIntegral, lintegral_smul_measure] at *
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
x : α
⊢ ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
have rw : ENNReal.ofReal (f x).toReal = ENNReal.ofReal (f x).toReal
Tactic: rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
have h : ∀ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
have simp_rw : ∫⁻ (a : α), ENNReal.ofReal (f a).toReal ∂μ < ∞
Tactic: simp_rw [hasFiniteIntegral_iff_enorm, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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 ∂μ < ∞
have refine : ∀ (x : α), ENNReal.ofReal (f x).toReal ≤ f x
Tactic: refine lt_of_le_of_lt (lintegral_mono fun x => ?_) (lt_top_iff_ne_top.2 hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
⊢ ENNReal.ofReal (f x).toReal ≤ f x
have pos : ∀ (hfx : f x = ∞), ENNReal.ofReal (f x).toReal ≤ f x
Tactic: by_cases hfx : f x = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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
⊢ ENNReal.ofReal (f x).toReal ≤ f x
have neg : ∀ (hfx : ¬f x = ∞), ENNReal.ofReal (f x).toReal ≤ f x
Tactic: by_cases hfx : f x = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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
have neg : ∀ (fx : ℝ≥0) (h : (↑fx : ℝ≥0∞) = f x), ENNReal.ofReal (↑fx : ℝ≥0∞).toReal ≤ (↑fx : ℝ≥0∞)
Tactic: lift f x to ℝ≥0 using hfx with fx h
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x
have h : ∀ (x : α) (hx : f x ≠ ∞), ENNReal.ofReal (f x).toReal = f x
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞
have this : ∀ᵐ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
have refine : ∀ (x : α), ENNReal.ofReal (f x) ≤ ‖f x‖ₑ
Tactic: refine isFiniteMeasure_withDensity ((lintegral_mono fun x => ?_).trans_lt hfi).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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 : ℕ) ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))
have h₁ : ∀ (x : α) (x_1 : ℕ), ENNReal.ofReal ‖F x_1 x‖ = ‖F x_1 x‖ₑ
Tactic: convert! ae_tendsto_enorm h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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‖ₑ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))
have h₂ : ∀ (x : α), ENNReal.ofReal ‖f x‖ = ‖f x‖ₑ
Tactic: convert! ae_tendsto_enorm h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
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))
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
have F_le_bound : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
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 : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
have F_le_bound₁ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
Tactic: rw [← ae_all_iff] at F_le_bound
Cleared hypotheses: F_le_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
have 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)
Tactic: apply F_le_bound.mp ((ae_tendsto_ofReal_norm h_lim).mono _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
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 : α) ∂μ, ‖f' a‖ₑ ≤ bound' a
have h_bound₁ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
Tactic: rw [← ae_all_iff] at h_bound
Cleared hypotheses: h_bound, h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
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))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a
have apply : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ ‖F' n x‖ₑ) atTop (𝓝 ‖f' x‖ₑ) → (∀ (i : ℕ), ‖F' i x‖ₑ ≤ bound' x) → ‖f' x‖ₑ ≤ bound' x
Tactic: apply h_bound.mp ((ae_tendsto_enorm h_lim).mono _)