awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ Integrable f μ
have simp_rw : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
  AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
simp_rw :
  AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ Integrable f μ
have simp_rw₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
  HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
simp_rw :
  AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
simp_rw₁ :
  AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
    HasFiniteIntegral f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ Integrable f μ
have simp_rw₂ : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
⊢ ∀ᵐ (a : α) ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a
have apply : ∀ (x : α), ‖f₀ x - f₁ x‖ ≤ g x → ‖f₁ x‖ ≤ ‖f₀ x‖ + g x
Tactic: apply h.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a
have a₁ : ‖f₀ a‖ + ‖f₀ a - f₁ a‖ ≤ ‖f₀ a‖ + g a
Tactic: calc
      ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ := norm_le_insert _ _
      _ ≤ ‖f₀ a‖ + g a := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
have h : ∀ (x : α) (hx1 : g₁ x ≤ f x) (hx2 : f x ≤ g₂ x), ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
Tactic: filter_upwards [h_le₁, h_le₂] with x hx1 hx2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ Integrable f μ
have this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
Tactic: have : ∀ᵐ x ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖ := by
    filter_upwards [h_le₁, h_le₂] with x hx1 hx2
    simp only [Real.norm_eq_abs]
    exact abs_le_max_abs_abs hx1 hx2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
have h : ∀ (x : α) (hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖), ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
have h : max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Tactic: refine hx.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
| ‖‖g₁ x‖ + ‖g₂ x‖‖
have rw : ‖g₁ x‖ + ‖g₂ x‖
Tactic: rw [Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
have h : max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖
Tactic: conv_rhs => rw [Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ Integrable f μ
have h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
Tactic: have h_le_add : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖ := by
    filter_upwards [this] with x hx
    refine hx.trans ?_
    conv_rhs => rw [Real.norm_of_nonneg (by positivity)]
    exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ε⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞
Tactic: refine meas_ge_le_mul_pow_eLpNorm_enorm μ one_ne_zero one_ne_top hf.1 hε.ne' (by simp [hε'])
    |>.trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ ε⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞
have a : ε⁻¹ ^ ENNReal.toReal 1 < ∞
Tactic: apply ENNReal.mul_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
a : ε⁻¹ ^ ENNReal.toReal 1 < ∞
⊢ ε⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞
have a₁ : eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞
Tactic: apply ENNReal.mul_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖} : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : ∀ (x : α), ε ≤ ‖f x‖ ↔ ENNReal.ofReal ε ≤ ‖f x‖ₑ
Tactic: convert! Integrable.measure_enorm_ge_lt_top hf (ofReal_pos.mpr hε) ofReal_ne_top with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
⊢ ε ≤ ‖f x‖ ↔ ENNReal.ofReal ε ≤ ‖f x‖ₑ
have h : ε ≤ ‖f x‖ ↔ ‖ε‖ₑ ≤ ‖f x‖ₑ
Tactic: rw [← Real.enorm_of_nonneg hε.le, enorm_le_iff_norm_le, Real.norm_of_nonneg hε.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
h : ε ≤ ‖f x‖ ↔ ‖ε‖ₑ ≤ ‖f x‖ₑ
⊢ ε ≤ ‖f x‖ ↔ ENNReal.ofReal ε ≤ ‖f x‖ₑ
have h₁ : ε ≤ ‖f x‖ ↔ ‖ε‖ ≤ ‖f x‖
Tactic: rw [← Real.enorm_of_nonneg hε.le, enorm_le_iff_norm_le, Real.norm_of_nonneg hε.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
h : ε ≤ ‖f x‖ ↔ ‖ε‖ₑ ≤ ‖f x‖ₑ
h₁ : ε ≤ ‖f x‖ ↔ ‖ε‖ ≤ ‖f x‖
⊢ ε ≤ ‖f x‖ ↔ ENNReal.ofReal ε ≤ ‖f x‖ₑ
have h₂ : ε ≤ ‖f x‖ ↔ ε ≤ ‖f x‖
Tactic: rw [← Real.enorm_of_nonneg hε.le, enorm_le_iff_norm_le, Real.norm_of_nonneg hε.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (hε' : ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hε' : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
pos : ∀ (hε' : ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (hε' : ¬ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases hε' : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
ε : β
ε_pos : 0 < ε
⊢ 0 < ‖ε‖
have positivity : ε ≠ 0 → 0 < ‖ε‖
Tactic: positivity [ε_pos.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
⊢ 0 < ‖c‖
have positivity : c ≠ 0 → 0 < ‖c‖
Tactic: positivity [c_neg.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ c} : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : 0 < ‖c‖
Tactic: have : 0 < ‖c‖ := by positivity [c_neg.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ c} : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x), Membership.mem (γ := Set α) {x : α | ‖c‖ ≤ ‖f x‖} x
Tactic: refine lt_of_le_of_lt (measure_mono fun x hx => ?_) (hf.measure_norm_ge_lt_top this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
⊢ -c ≤ -f x
have simp : f x ≤ c
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
⊢ Membership.mem (γ := Set α) {x : α | ‖c‖ ≤ ‖f x‖} x
have this₁ : -c ≤ -f x
Tactic: have : -c ≤ -f x := by simp; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ
have refine : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ
have rw : ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ < ∞
have refine : ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
Tactic: refine lt_of_le_of_lt ?_ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
have hfg : LE.le.{u_1} (α := α → ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖) fun (a : α) ↦ ENNReal.ofReal ‖f a‖
Tactic: apply lintegral_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ (fun (x : α) ↦ ENNReal.ofReal (f x).toReal) =ᶠ[ae μ] f
have h : ∀ (a : α), f a < ∞ → ENNReal.ofReal (f a).toReal = f a
Tactic: filter_upwards [hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ (fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)) =ᶠ[ae μ] f
have h : ∀ (a : α), f a < ∞ → (↑(f a).toNNReal : ℝ≥0∞) = f a
Tactic: filter_upwards [hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
⊢ @Integrable _ _ _ _ m f Measure.count ↔ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
have rw : (Summable (α := ℝ) fun (x : α) ↦ ‖f x‖) → AEStronglyMeasurable (m₀ := m) f Measure.count
Tactic: rw [Integrable, hasFiniteIntegral_count_iff, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
⊢ AEStronglyMeasurable (m₀ := m) f Measure.count
have hs' : (Function.support f).Countable
Tactic: have hs' : (Function.support f).Countable := by
    simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
      using hs.countable_support
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this : MeasurableSpace β := borel β
⊢ AEStronglyMeasurable (m₀ := m) f Measure.count
have this₁ : BorelSpace β
Tactic: haveI : BorelSpace β := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEStronglyMeasurable (m₀ := m) f Measure.count
have refine_1 : AEMeasurable (_m := m) f Measure.count
Tactic: refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
refine_1 : AEMeasurable (_m := m) f Measure.count
⊢ AEStronglyMeasurable (m₀ := m) f Measure.count
have refine_2 : ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t
Tactic: refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEMeasurable (_m := m) f Measure.count
have refine_1 : Set.Countable.{u_1} (α := α) {x : α | 0 x ≠ f x}
Tactic: refine (measurable_zero.measurable_of_countable_ne ?_).aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t
have refine_2 : IsSeparable (f '' univ)
Tactic: refine ⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ IsSeparable (f '' univ)
have refine_2 : f '' univ ⊆ f '' Function.support f ∪ {0}
Tactic: suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
      (((hs'.image f).union (countable_singleton 0)).mono this).isSeparable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have pos : ∀ (H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ),
  Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
Tactic: by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
pos :
  ∀ (H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ),
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
      Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have neg : ∀ (H : ¬AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ),
  Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
Tactic: by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have pos : (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) < ∞ ↔ ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
Tactic: simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, hasFiniteIntegral_iff_enorm, H,
      true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) < ∞ ↔ ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
have pos : ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) (fun (a : α) ↦ ‖g a‖ₑ) a ∂μ < ∞ ↔
  ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
Tactic: rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
pos :
  ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) (fun (a : α) ↦ ‖g a‖ₑ) a ∂μ <
      ∞ ↔
    ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
⊢ (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) < ∞ ↔ ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
have pos₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ) (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
Tactic: rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
have rw : Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toNNReal • g x) μ ↔
  Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
Tactic: rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_smul]