awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (∑ i ∈ s, f i) p μ
have h : Eq (α := α → ε') (∑ i ∈ s, f i) fun (a : α) ↦ ∑ i ∈ s, f i a
Tactic: convert! memLp_finsetSum s hf using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ Eq (α := α → ε') (∑ i ∈ s, f i) fun (a : α) ↦ ∑ i ∈ s, f i a
have h : ∀ (x : α), Eq.{u_4 + 1} (α := ε') ((∑ i ∈ s, f i) x) (∑ i ∈ s, f i x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm) ^ (1 / q) = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
have e_a : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm = ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)
have simp_rw : Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})
Tactic: simp_rw [limsup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
h_set_eq : Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a}
⊢ Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})
have rw : Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})
Tactic: rw [h_set_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})
have suffices : Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a}
Tactic: suffices h_set_eq : { a : ℝ≥0∞ | ∀ᵐ n ∂μ.trim hm, f n ≤ a } = { a : ℝ≥0∞ | ∀ᵐ n ∂μ, f n ≤ a } by
    rw [h_set_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a}
have h : ∀ (a : ℝ≥0∞),
  Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} a ↔
    Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a} a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
    ((μ.trim hm : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} a ↔
    Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a} a
have simp_rw : (∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a) ↔ ∀ᵐ (n : α) ∂μ, f n ≤ a
Tactic: simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
    ((μ.trim hm : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
simp_rw : (∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a) ↔ ∀ᵐ (n : α) ∂μ, f n ≤ a
⊢ Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} a ↔
    Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a} a
have simp_rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) {a_1 : α | ¬f a_1 ≤ a} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | ¬f a_1 ≤ a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} a ↔
    Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a} a
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
  ((μ.trim hm : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
Tactic: suffices h_meas_eq : μ { x | ¬f x ≤ a } = μ.trim hm { x | ¬f x ≤ a } by
    simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
    ((μ.trim hm : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
have h : MeasurableSet.{u_1} (α := α) {x : α | ¬f x ≤ a}
Tactic: refine (trim_measurableSet_eq hm ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ
have pos : ∀ (h0 : p = 0), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
pos : ∀ (h0 : p = 0), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ
have neg : ∀ (h0 : ¬p = 0), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
h0 : ¬p = 0
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ
have pos : ∀ (h_top : p = ∞), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ
have neg : ∀ (h_top : ¬p = ∞), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Trim (goal)
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ
have rw : eLpNorm (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ
Tactic: rw [eLpNorm_congr_ae hf.ae_eq_mk, eLpNorm_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α_1 : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E_1 : Type u_4
F : Type u_5
m_1 : MeasurableSpace α_1
p_1 : ℝ≥0∞
μ_1 : Measure α_1
inst : NormedAddCommGroup E_1
inst_1 : NormedAddCommGroup F
α : Type u_7
E : Type u_6
m : MeasurableSpace α
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} f
⊢ Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} (-f)
have rwa : eLpNorm (↑(-f) : α → E) p μ < ∞
Tactic: rwa [Set.mem_setOf_eq, eLpNorm_congr_ae (AEEqFun.coeFn_neg f), eLpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α_1 : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E_1 : Type u_4
F : Type u_5
m_1 : MeasurableSpace α_1
p_1 : ℝ≥0∞
μ_1 : Measure α_1
inst : NormedAddCommGroup E_1
inst_1 : NormedAddCommGroup F
α : Type u_7
E : Type u_6
m : MeasurableSpace α
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} f
rwa : eLpNorm (↑(-f) : α → E) p μ < ∞
⊢ Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} (-f)
have rwa₁ : eLpNorm (-(↑f : α → E)) p μ < ∞
Tactic: rwa [Set.mem_setOf_eq, eLpNorm_congr_ae (AEEqFun.coeFn_neg f), eLpNorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α_1 : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E_1 : Type u_4
F : Type u_5
m_1 : MeasurableSpace α_1
p_1 : ℝ≥0∞
μ_1 : Measure α_1
inst : NormedAddCommGroup E_1
inst_1 : NormedAddCommGroup F
α : Type u_7
E : Type u_6
m : MeasurableSpace α
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} f
rwa : eLpNorm (↑(-f) : α → E) p μ < ∞
rwa₁ : eLpNorm (-(↑f : α → E)) p μ < ∞
⊢ Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} (-f)
have rwa₂ : eLpNorm (↑f : α → E) p μ < ∞
Tactic: rwa [Set.mem_setOf_eq, eLpNorm_congr_ae (AEEqFun.coeFn_neg f), 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 : α → E
hf : MemLp f p μ
⊢ ‖MemLp.toLp f hf‖ = (eLpNorm f p μ).toReal
have rw : (eLpNorm (↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) p μ).toReal = (eLpNorm f p μ).toReal
Tactic: rw [norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp 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 : α → E
hf : MemLp f p μ
rw : (eLpNorm (↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) p μ).toReal = (eLpNorm f p μ).toReal
⊢ ‖MemLp.toLp f hf‖ = (eLpNorm f p μ).toReal
have rw₁ : (eLpNorm f p μ).toReal = (eLpNorm f p μ).toReal
Tactic: rw [norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp 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 : α → E
hf : MemLp f p μ
⊢ ‖MemLp.toLp f hf‖ₑ = eLpNorm f p μ
have simp_rw : (↑‖MemLp.toLp f hf‖₊ : ℝ≥0∞) = eLpNorm f p μ
Tactic: simp_rw [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]
-- 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 : α → E
hf : MemLp f p μ
simp_rw : (↑‖MemLp.toLp f hf‖₊ : ℝ≥0∞) = eLpNorm f p μ
⊢ ‖MemLp.toLp f hf‖ₑ = eLpNorm f p μ
have simp_rw₁ : (↑(eLpNorm f p μ).toNNReal : ℝ≥0∞) = eLpNorm f p μ
Tactic: simp_rw [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]
-- 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 μ)
⊢ (eLpNorm (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) p μ).toReal =
    (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
have e_a : eLpNorm (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) p μ =
  eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
Tactic: congr 1
-- 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 μ)
⊢ eLpNorm (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) p μ =
    eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
have e_a : (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] -(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)
Tactic: apply eLpNorm_congr_ae
-- 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 μ)
⊢ dist f g = (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
have rw : (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
  (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
Tactic: rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
⊢ dist f g = (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
have rw₁ : (eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ).toReal =
  (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
Tactic: rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₁ :
  (eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
⊢ dist f g = (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
have rw₂ : (eLpNorm (- -(↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
  (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
Tactic: rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₁ :
  (eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₂ :
  (eLpNorm (- -(↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
⊢ dist f g = (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
have rw₃ : (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
  (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
Tactic: rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₁ :
  (eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₂ :
  (eLpNorm (- -(↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
rw₃ :
  (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
    (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
⊢ dist f g = (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
have rw₄ : (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal =
  (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
Tactic: rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
⊢ edist f g = eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
have rw : eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
Tactic: rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
⊢ edist f g = eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
have rw₁ : eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ =
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
Tactic: rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
rw₁ :
  eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
⊢ edist f g = eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
have rw₂ : eLpNorm (- -(↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
Tactic: rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
rw₁ :
  eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
rw₂ :
  eLpNorm (- -(↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
⊢ edist f g = eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
have rw₃ : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
Tactic: rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
rw :
  eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
rw₁ :
  eLpNorm (-(-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E))) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
rw₂ :
  eLpNorm (- -(↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
rw₃ :
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
⊢ edist f g = eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
have rw₄ : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
  eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) + -(↑(↑g : α →ₘ[μ] E) : α → E)) p μ
Tactic: rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_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 g : ↥(Lp E p μ)
⊢ edist f g = ENNReal.ofReal (dist f g)
have rw : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ = ENNReal.ofReal (dist f g)
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 : ↥(Lp E p μ)
rw : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ = ENNReal.ofReal (dist f g)
⊢ edist f g = ENNReal.ofReal (dist f g)
have rw₁ : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ =
  ENNReal.ofReal (eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal
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 : ↥(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
⊢ edist f g = ENNReal.ofReal (dist f g)
have rw₂ : eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ = ENNReal.ofReal (eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ).toReal
Tactic: rw [edist_def, dist_def, ← eLpNorm_congr_ae (coeFn_sub _ _),
    ENNReal.ofReal_toReal (eLpNorm_ne_top (f - g))]