awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) μ
⊢ Integrable g (μ.withDensity f) ↔ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
have hf₁ : Measurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal
Tactic: rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_smul]
-- 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.{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) μ
have simp_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: simp_rw [NNReal.smul_def, ENNReal.toReal]
-- 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 : AEMeasurable f μ
g : α → E
this : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞))
have rw : Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)) ↔
  Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞))
Tactic: rw [withDensity_congr_ae this]
-- 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 : AEMeasurable f μ
g : α → E
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞))
have suffices : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
Tactic: suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by
        rw [withDensity_congr_ae this]
-- 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 : AEMeasurable f μ
g : α → E
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
have h : ∀ (x : α) (hx : f x = AEMeasurable.mk f hf x), (↑(f x) : ℝ≥0∞) = (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
Tactic: filter_upwards [hf.ae_eq_mk] with x hx
-- 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 : AEMeasurable f μ
g : α → E
⊢ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ) • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have h : EventuallyEq.{u_1, u_8} (β := E) (ae μ) (fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ) • g x) fun (x : α) ↦
  (↑(f x) : ℝ) • g x
Tactic: apply integrable_congr
-- 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 : AEMeasurable f μ
g : α → E
⊢ EventuallyEq.{u_1, u_8} (β := E) (ae μ) (fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ) • g x) fun (x : α) ↦
    (↑(f x) : ℝ) • g x
have h : ∀ (x : α) (hx : f x = AEMeasurable.mk f hf x), (↑(AEMeasurable.mk f hf x) : ℝ) • g x = (↑(f x) : ℝ) • g x
Tactic: filter_upwards [hf.ae_eq_mk] with x hx
-- 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 : AEMeasurable 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_coe_smul₀]
-- 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 : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
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) μ
⊢ Integrable g (μ.withDensity f) ↔ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
have hf₁ : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ
Tactic: rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_coe_smul₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
⊢ Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ g x * (f x).toReal) μ
have this : Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x
Tactic: have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ g x * (f x).toReal) μ
have rw : Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal • g x) μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ =
    MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
      MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯
have h : (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
        α →ₘ[μ] E) :
    α → E) =ᶠ[ae μ]
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry +
            MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
              sorry) :
        α →ₘ[μ] E) :
    α → E)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hu :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
hv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
huv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    ((↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E) +
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h'' :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      ((↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) +
          (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E))
        x
⊢ (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x
have h : f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
  f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x +
    f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
Tactic: rw [huv, h', Pi.add_apply, hu, hv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hu :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
hv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
huv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    ((↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E) +
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h'' :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      ((↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) +
          (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E))
        x
⊢ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x +
      f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
have h : ∀ (hx : f x = 0),
  f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x +
      f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
Tactic: rcases eq_or_ne (f x) 0 with (hx | hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hu :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
hv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
huv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    ((↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E) +
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h'' :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      ((↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) +
          (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E))
        x
hx : f x ≠ 0
⊢ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x +
      f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
have rw : (↑(f x) : ℝ≥0∞) ≠ 0
Tactic: rw [h'' _, Pi.add_apply, smul_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
      (MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯)
have h : (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
        α →ₘ[μ] E) :
    α → E) =ᶠ[ae μ]
  (↑(↑(HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
            (MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
              sorry)) :
        α →ₘ[μ] E) :
    α → E)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
h :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      (r • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h'' :
  (↑(↑(r • MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (r •
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h''' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
⊢ (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (↑(↑(HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
                (MemLp.toLp
                  (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯)) :
            α →ₘ[μ] E) :
        α → E)
      x
have h₁ : f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
  r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
Tactic: rw [RingHom.id_apply, h', h'', Pi.smul_apply, h''']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
h :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      (r • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h'' :
  (↑(↑(r • MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (r •
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h''' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
⊢ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
have h₁ : ∀ (hx : f x = 0),
  f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
Tactic: rcases eq_or_ne (f x) 0 with (hx | hx)