awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : Integrable f μ
hν : Integrable f ν
⊢ Integrable f (μ + ν)
have simp_rw : ∀ (hμ : MemLp f 1 μ) (hν : MemLp f 1 ν), MemLp f 1 (μ + ν)
Tactic: simp_rw [← memLp_one_iff_integrable] at hμ hν ⊢
Cleared hypotheses: hμ, hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ MemLp f 1 (μ + ν)
have refine : eLpNorm f 1 (μ + ν) < ∞
Tactic: refine ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 (μ + ν) < ∞
have rw : eLpNorm f 1 μ < ∞ ∧ eLpNorm f 1 ν < ∞
Tactic: rw [eLpNorm_one_add_measure, ENNReal.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : Integrable f (μ + ν)
⊢ Integrable f μ
have rw : ∀ (h : MemLp f 1 (μ + ν)), MemLp f 1 μ
Tactic: rw [← memLp_one_iff_integrable] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : Integrable f (μ + ν)
⊢ Integrable f ν
have rw : ∀ (h : MemLp f 1 (μ + ν)), MemLp f 1 ν
Tactic: rw [← memLp_one_iff_integrable] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
⊢ @Integrable _ _ _ _ m f 0
have left : AEStronglyMeasurable (m₀ := m) f 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
left : AEStronglyMeasurable (m₀ := m) f 0
⊢ @Integrable _ _ _ _ m f 0
have right : @HasFiniteIntegral _ _ _ m f 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
⊢ @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
have empty : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
empty : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
⊢ @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
      (@Integrable _ _ _ _ m f (∑ i ∈ insert a s, μ i) ↔ ∀ i ∈ insert a s, Integrable f (μ i))
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
⊢ @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
have empty : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
Tactic: classical
  induction s using Finset.induction_on <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
empty : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
⊢ @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
      (@Integrable _ _ _ _ m f (∑ i ∈ insert a s, μ i) ↔ ∀ i ∈ insert a s, Integrable f (μ i))
Tactic: classical
  induction s using Finset.induction_on <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ Integrable f (c • μ)
have rw : ∀ (h : MemLp f 1 μ) {c : ℝ≥0∞} (hc : c ≠ ∞), MemLp f 1 (c • μ)
Tactic: rw [← memLp_one_iff_integrable] at h ⊢
Cleared hypotheses: h, c, hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0
⊢ Integrable f (c • μ)
have apply : (↑c : ℝ≥0∞) ≠ ∞
Tactic: apply h.smul_measure
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inl : ∀ (h : @Integrable _ _ _ _ m f 0),
  Integrable f (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
Tactic: rcases eq_or_ne μ 0 with (rfl | hne)
Cleared hypotheses: μ, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
inl :
  ∀ (h : @Integrable _ _ _ _ m f 0),
    Integrable f (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inr : ∀ (hne : μ ≠ 0), Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
Tactic: rcases eq_or_ne μ 0 with (rfl | hne)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
hne : μ ≠ 0
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inr : Ne (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply h.smul_measure
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
α' : Type u_8
inst_2 : MeasurableSpace α'
f : α → α'
g : α' → ε
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ @Integrable _ _ _ _ inst_2 g (Measure.map f μ) ↔ Integrable (g ∘ f) μ
have simp_rw : MemLp (m0 := inst_2) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → δ
hf : MeasurableEmbedding f
g : δ → ε
⊢ @Integrable _ _ _ _ inst g (Measure.map f μ) ↔ Integrable (g ∘ f) μ
have simp_rw : MemLp (m0 := inst) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α ≃ᵐ δ
g : δ → ε
⊢ @Integrable _ _ _ _ inst g (Measure.map (⇑f : (a : α) → δ) μ) ↔ Integrable (g ∘ (⇑f : (a : α) → δ)) μ
have simp_rw : MemLp (m0 := inst) g 1 (Measure.map (⇑f : (a : α) → δ) μ) ↔ MemLp (g ∘ (⇑f : (a : α) → δ)) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g ν
⊢ Integrable (g ∘ f) μ ↔ Integrable g ν
have rw : ∀ (hg : AEStronglyMeasurable (m₀ := inst) g (Measure.map f μ)),
  Integrable (g ∘ f) μ ↔ @Integrable _ _ _ _ inst g (Measure.map f μ)
Tactic: rw [← hf.map_eq] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫⁻ (a : α), edist (f a) (0 a) ∂μ < ∞ ∧ ∫⁻ (a : α), edist (g a) (0 a) ∂μ < ∞
have simp_rw : HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ
Tactic: simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable (g + f) μ ↔ Integrable g μ
have rw : Integrable (f + g) μ ↔ Integrable g μ
Tactic: rw [add_comm, integrable_add_iff_integrable_right hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
rw : Integrable (f + g) μ ↔ Integrable g μ
⊢ Integrable (g + f) μ ↔ Integrable g μ
have rw₁ : Integrable g μ ↔ Integrable g μ
Tactic: rw [add_comm, integrable_add_iff_integrable_right hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ Integrable f μ
have refine : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a
Tactic: refine h_int.mono' h_meas ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a
have h : ∀ (a : α) (haf : 0 a ≤ f a) (hag : 0 a ≤ g a), ‖f a‖ ≤ (f + g) a
Tactic: filter_upwards [hf, hg] with a haf hag
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
have rw : Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ
Tactic: rw [← integrable_neg_iff, ← integrable_neg_iff (f := f), ← integrable_neg_iff (f := g), neg_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
have left : AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
left : AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
have right : HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
Tactic: constructor
-- 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 μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ
have left : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ
Tactic: constructor
-- 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 μ
left : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ
have right : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊓ g) μ
have rw : ∀ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ), MemLp (f ⊓ g) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊔ g) μ
have rw : ∀ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ), MemLp (f ⊔ g) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f : α → β
hf : Integrable f μ
⊢ Integrable.{u_8, u_1} (ε := β) (fun (a : α) ↦ |f a|) μ
have rw : ∀ (hf : MemLp f 1 μ), MemLp.{u_1, u_8} (ε := β) (fun (a : α) ↦ |f a|) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : Integrable f μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ g x • f x) μ
have rw : ∀ (hf : MemLp f 1 μ) {g : α → R} (g_aestronglyMeasurable : AEStronglyMeasurable g μ)
  (ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞),
  MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at *
Cleared hypotheses: hf, g, g_aestronglyMeasurable, ess_sup_g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ
have refine : eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ < ∞
Tactic: refine ⟨g_aestronglyMeasurable.smul hf.1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ eLpNorm g ∞ μ ≠ ∞
have rwa : eLpNormEssSup g μ ≠ ∞
Tactic: rwa [eLpNorm_exponent_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ < ∞
have hg' : eLpNorm g ∞ μ ≠ ∞
Tactic: have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ < ∞
have eLpNorm : eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ ≤ eLpNorm g ∞ μ * eLpNorm f 1 μ
Tactic: calc
    eLpNorm (fun x : α => g x • f x) 1 μ ≤ _ := by
      simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm hf.1 g_aestronglyMeasurable
        (p := ∞) (q := 1)
    _ < ∞ := ENNReal.mul_lt_top hg'.lt_top hf.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : Integrable f μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ f x • g x) μ
have rw : ∀ (hf : MemLp f 1 μ) {g : α → β} (g_aestronglyMeasurable : AEStronglyMeasurable g μ)
  (ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞),
  MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at *
Cleared hypotheses: hf, g, g_aestronglyMeasurable, ess_sup_g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ
have refine : eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ < ∞
Tactic: refine ⟨hf.1.smul g_aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ eLpNorm g ∞ μ ≠ ∞
have rwa : eLpNormEssSup g μ ≠ ∞
Tactic: rwa [eLpNorm_exponent_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ < ∞
have hg' : eLpNorm g ∞ μ ≠ ∞
Tactic: have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ < ∞
have eLpNorm : eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ ≤ eLpNorm f 1 μ * eLpNorm g ∞ μ
Tactic: calc
    eLpNorm (fun x : α => f x • g x) 1 μ ≤ _ := by
      simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm g_aestronglyMeasurable hf.1
        (p := 1) (q := ∞)
    _ < ∞ := ENNReal.mul_lt_top hf.2 hg'.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ Integrable f μ
have simp_rw : AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
  AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, and_iff_right hf, and_iff_right hf.enorm.aestronglyMeasurable,
    hasFiniteIntegral_enorm_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
simp_rw :
  AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ Integrable f μ
have simp_rw₁ : AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
  HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, and_iff_right hf, and_iff_right hf.enorm.aestronglyMeasurable,
    hasFiniteIntegral_enorm_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
simp_rw :
  AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
simp_rw₁ :
  AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
    HasFiniteIntegral f μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ Integrable f μ
have simp_rw₂ : HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, and_iff_right hf, and_iff_right hf.enorm.aestronglyMeasurable,
    hasFiniteIntegral_enorm_iff]