awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
rw : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ = ENNReal.ofReal (dist f g)
rw₁ :
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    ENNReal.ofReal (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₂ :
  eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ = ENNReal.ofReal (eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ).toReal
⊢ edist f g = ENNReal.ofReal (dist f g)
have rw₃ : eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ = eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ
Tactic: rw [edist_def, dist_def, ← eLpNorm_congr_ae (coeFn_sub _ _),
    ENNReal.ofReal_toReal (eLpNorm_ne_top (f - g))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ edist (MemLp.toLp f hf) (MemLp.toLp g hg) = eLpNorm (f - g) p μ
have rw : eLpNorm ((↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp g hg) : α →ₘ[μ] E) : α → E)) p μ =
  eLpNorm (f - g) p μ
Tactic: rw [edist_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
⊢ nnnorm (E := ↥(Lp E p μ)) 0 = 0
have rw : (eLpNorm.{u_1, u_4} (ε := E) (↑0 : α → E) p μ).toNNReal = 0
Tactic: rw [nnnorm_def, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
f : ↥(Lp E p 0)
⊢ ‖f‖ = 0
have simp_rw : (@eLpNorm _ _ _ m (↑(↑f : α →ₘ[0] E) : α → E) p 0).toReal = 0
Tactic: simp_rw [norm_def, eLpNorm_measure_zero, ENNReal.toReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
f : ↥(Lp E p 0)
simp_rw : (@eLpNorm _ _ _ m (↑(↑f : α →ₘ[0] E) : α → E) p 0).toReal = 0
⊢ ‖f‖ = 0
have simp_rw₁ : ENNReal.toReal 0 = 0
Tactic: simp_rw [norm_def, eLpNorm_measure_zero, ENNReal.toReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E 0 μ)
⊢ ‖f‖ = 0
have simp_rw : (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 0 μ).toReal = 0
Tactic: simp_rw [norm_def, eLpNorm_exponent_zero, ENNReal.toReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E 0 μ)
simp_rw : (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 0 μ).toReal = 0
⊢ ‖f‖ = 0
have simp_rw₁ : ENNReal.toReal 0 = 0
Tactic: simp_rw [norm_def, eLpNorm_exponent_zero, ENNReal.toReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ f = 0 ↔ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have rw : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E) ↔ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: rw [Lp.ext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
⊢ ‖f‖₊ = 0 ↔ f = 0
have refine : ∀ (hf : ‖f‖₊ = 0), f = 0
Tactic: refine ⟨fun hf => ?_, fun hf => by simp [hf]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : ‖f‖₊ = 0
⊢ f = 0
have hf₁ : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0
Tactic: simp_rw [nnnorm_def, ENNReal.toNNReal_eq_zero_iff, eLpNorm_ne_top, or_false] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0
⊢ f = 0
have simp_rw : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: simp_rw [eq_zero_iff_ae_eq_zero, ← eLpNorm_eq_zero_iff (Lp.aestronglyMeasurable f) hp.ne.symm, hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ ‖-f‖₊ = ‖f‖₊
have rw : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = ‖f‖₊
Tactic: rw [nnnorm_def, nnnorm_def, eLpNorm_congr_ae (coeFn_neg _), eLpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
rw : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = ‖f‖₊
⊢ ‖-f‖₊ = ‖f‖₊
have rw₁ : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
Tactic: rw [nnnorm_def, nnnorm_def, eLpNorm_congr_ae (coeFn_neg _), eLpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
rw : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = ‖f‖₊
rw₁ : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
⊢ ‖-f‖₊ = ‖f‖₊
have rw₂ : (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E)) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
Tactic: rw [nnnorm_def, nnnorm_def, eLpNorm_congr_ae (coeFn_neg _), eLpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
rw : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = ‖f‖₊
rw₁ : (eLpNorm (↑(↑(-f) : α →ₘ[μ] E) : α → E) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
rw₂ : (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E)) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
⊢ ‖-f‖₊ = ‖f‖₊
have rw₃ : (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
Tactic: rw [nnnorm_def, nnnorm_def, eLpNorm_congr_ae (coeFn_neg _), eLpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖₊
⊢ ‖f‖₊ ≤ c * ‖g‖₊
have simp : (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toNNReal
Tactic: simp only [nnnorm_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖₊
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toNNReal
have this : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ
Tactic: have := eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul h p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖₊
this : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toNNReal
have ha : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≠ ∞
Tactic: rwa [← ENNReal.toNNReal_le_toNNReal, ENNReal.smul_def, smul_eq_mul, ENNReal.toNNReal_mul,
    ENNReal.toNNReal_coe] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖₊
this : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ
ha : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≠ ∞
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toNNReal
have hb : c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ ≠ ∞
Tactic: rwa [← ENNReal.toNNReal_le_toNNReal, ENNReal.smul_def, smul_eq_mul, ENNReal.toNNReal_mul,
    ENNReal.toNNReal_coe] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ ‖f‖ ≤ c * ‖g‖
have inl : ∀ (hc : 0 ≤ c), ‖f‖ ≤ c * ‖g‖
Tactic: rcases le_or_gt 0 c with hc | hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
inl : ∀ (hc : 0 ≤ c), ‖f‖ ≤ c * ‖g‖
⊢ ‖f‖ ≤ c * ‖g‖
have inr : ∀ (hc : c < 0), ‖f‖ ≤ c * ‖g‖
Tactic: rcases le_or_gt 0 c with hc | hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
hc : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖
have inl : ∀ (c : ℝ≥0) (h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑c : ℝ) * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖),
  ‖f‖ ≤ (↑c : ℝ) * ‖g‖
Tactic: lift c to ℝ≥0 using hc
Cleared hypotheses: c, h, hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
hc : c < 0
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toReal
have this : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0 ∧ eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ = 0
Tactic: have := eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg h hc p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
have pos : ∀ (hμ : μ = 0), ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
pos : ∀ (hμ : μ = 0), ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
have neg : ∀ (hμ : ¬μ = 0), ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
have neg : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (eLpNorm_ne_top _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg : C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
  (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
Tactic: refine (eLpNorm_le_of_ae_nnnorm_bound hfC).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
Tactic: rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg₁ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
Tactic: rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₁ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg₂ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) * (↑C : ℝ≥0∞)
Tactic: rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₁ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₂ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) * (↑C : ℝ≥0∞)
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg₃ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
Tactic: rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₁ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₂ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) * (↑C : ℝ≥0∞)
neg₃ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg₄ : (↑C : ℝ≥0∞) • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
Tactic: rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₁ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₂ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) * (↑C : ℝ≥0∞)
neg₃ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
neg₄ :
  (↑C : ℝ≥0∞) • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) =
    (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
have neg₅ : (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
Tactic: rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ
hC : 0 ≤ C
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ C
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * C
have lift : ∀ (C : ℝ≥0) (hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)),
  ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
Tactic: lift C to ℝ≥0 using hC
Cleared hypotheses: C, hC, hfC
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
have this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
Tactic: have := nnnorm_le_of_ae_bound hfC
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
have rwa : ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ)),
  ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
rwa :
  ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
have rwa₁ : ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ) * (↑C : ℝ)),
  ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
rwa :
  ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
rwa₁ :
  ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ) * (↑C : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
have rwa₂ : ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)),
  ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have suffices : ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ
Tactic: suffices ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ by
            -- Squeezed for performance reasons
            simpa only [ge_iff_le, enorm, ← ENNReal.coe_add, ENNReal.coe_le_coe] using this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ
have simp : eLpNorm (↑(↑(f + g) : α →ₘ[μ] E) : α → E) p μ ≤
  eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ + eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ
Tactic: simp only [Lp.enorm_def]