awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (↑(↑(f + g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_add _ _

Premises used: MeasureTheory.AEEqFun.coeFn_add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (↑(↑(f - g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_sub _ _

Premises used: MeasureTheory.AEEqFun.coeFn_sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
E : Type u_4
p : ℝ≥0∞
inst : NormedAddCommGroup E
α : Type u_6
x : MeasurableSpace α
μ : Measure α
c : E
inst_1 : IsFiniteMeasure μ
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (AEEqFun.const α c)

Tactic:
(memLp_const c).eLpNorm_mk_lt_top

Premises used: Set.Mem, setOf, MeasureTheory.MemLp.eLpNorm_mk_lt_top, MeasureTheory.AEEqFun.const, MeasureTheory.memLp_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ ‖f‖ = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ ‖f‖₊ = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal

Tactic:
rfl

Premises used: NNReal.mk, NNReal, ENNReal.toNNReal, ENNReal.toReal, WithTop.untopD, WithTop.recTopCoe, NNReal.toReal, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ (↑‖f‖₊ : ℝ) = ‖f‖

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ ‖f‖ₑ = eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ

Tactic:
ENNReal.coe_toNNReal <| Lp.eLpNorm_ne_top f

Premises used: ENNReal.coe_toNNReal, NNReal.mk, NNReal, ENNReal.toNNReal, ENNReal.toReal, WithTop.untopD, WithTop.recTopCoe, NNReal.toReal, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
rw₁ rw₂ : (eLpNorm f p μ).toReal = (eLpNorm f p μ).toReal
⊢ ‖MemLp.toLp f hf‖ = (eLpNorm f p μ).toReal

Tactic:
rw [norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp hf)]

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.eLpNorm_congr_ae, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ).toNNReal

Tactic:
NNReal.eq <| norm_toLp f hf

Premises used: MeasureTheory.Lp.norm_toLp, NNReal.eq
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ
simp_rw₁ : (↑(eLpNorm f p μ).toNNReal : ℝ≥0∞) = eLpNorm f p μ
⊢ ‖MemLp.toLp f hf‖ₑ = eLpNorm f p μ

Tactic:
simp_rw [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]

Premises used: ENNReal.coe_toNNReal, MeasureTheory.Lp.nnnorm_toLp, ENorm.enorm, And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
e_a :
  eLpNorm (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) p μ =
    eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ
⊢ (eLpNorm (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) p μ).toReal =
    (eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ).toReal

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
e_a : (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] -(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ eLpNorm (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) p μ =
    eLpNorm (-(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) p μ

Tactic:
apply eLpNorm_congr_ae

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] -(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
(coeFn_add _ _).trans ((coeFn_neg f).add ae_eq_rfl)

Premises used: MeasureTheory.ae_eq_rfl, MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq.trans, Filter.EventuallyEq.add, MeasureTheory.Lp.coeFn_neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (↑(↑(-f + g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] -(↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
exact (coeFn_add _ _).trans ((coeFn_neg f).add ae_eq_rfl)

Premises used: MeasureTheory.ae_eq_rfl, MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq.trans, Filter.EventuallyEq.add, MeasureTheory.Lp.coeFn_neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
rw₄ 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

Tactic:
rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, MeasureTheory.Lp.dist_eq_eLpNorm_neg_add, neg_add, neg_neg, MeasureTheory.eLpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ
rw₄ 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 μ

Tactic:
rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

Premises used: MeasureTheory.Lp.edist_eq_eLpNorm_neg_add, sub_eq_add_neg, neg_add, neg_neg, MeasureTheory.eLpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
rw₃ rw₄ : eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ = eLpNorm (↑(↑(f - g) : α →ₘ[μ] E) : α → E) p μ
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
rw [edist_def, dist_def, ← eLpNorm_congr_ae (coeFn_sub _ _),
    ENNReal.ofReal_toReal (eLpNorm_ne_top (f - g))]

Premises used: MeasureTheory.Lp.edist_def, MeasureTheory.Lp.dist_def, HSub.hSub, ENNReal.ofReal_toReal, MeasureTheory.Lp.coeFn_sub, MeasureTheory.eLpNorm_congr_ae, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ dist f g = (edist f g).toReal

Tactic:
MeasureTheory.Lp.dist_eq_eLpNorm_neg_add ..

Premises used: MeasureTheory.Lp.dist_eq_eLpNorm_neg_add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ dist f g = ‖-f + g‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ
rw :
  eLpNorm ((↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp g hg) : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm (f - g) p μ
⊢ edist (MemLp.toLp f hf) (MemLp.toLp g hg) = eLpNorm (f - g) p μ

Tactic:
rw [edist_def]

Premises used: MeasureTheory.Lp.edist_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ
⊢ eLpNorm ((↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp g hg) : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm (f - g) p μ

Tactic:
eLpNorm_congr_ae (hf.coeFn_toLp.sub hg.coeFn_toLp)

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ
⊢ eLpNorm ((↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) - (↑(↑(MemLp.toLp g hg) : α →ₘ[μ] E) : α → E)) p μ =
    eLpNorm (f - g) p μ

Tactic:
exact eLpNorm_congr_ae (hf.coeFn_toLp.sub hg.coeFn_toLp)

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ edist (MemLp.toLp f hf) 0 = eLpNorm f p μ

Tactic:
simpa using edist_toLp_toLp f 0 hf .zero

Premises used: MeasureTheory.MemLp.zero, MeasureTheory.Lp.edist_toLp_toLp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
rw : (eLpNorm.{u_1, u_4} (ε := E) (↑0 : α → E) p μ).toNNReal = 0
⊢ nnnorm (E := ↥(Lp E p μ)) 0 = 0

Tactic:
rw [nnnorm_def, ZeroMemClass.coe_zero]

Premises used: MeasureTheory.Lp.nnnorm_def, ZeroMemClass.coe_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
⊢ (eLpNorm.{u_1, u_4} (ε := E) (↑0 : α → E) p μ).toNNReal = 0

Tactic:
simp [eLpNorm_congr_ae AEEqFun.coeFn_zero, eLpNorm_zero]

Premises used: MeasureTheory.eLpNorm_zero, MeasureTheory.AEEqFun.coeFn_zero, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
⊢ norm (E := ↥(Lp E p μ)) 0 = 0

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) nnnorm_zero

Premises used: congr_arg, NNReal.toReal, MeasureTheory.Lp.nnnorm_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
simp_rw₁ : ENNReal.toReal 0 = 0
⊢ ‖f‖ = 0

Tactic:
simp_rw [norm_def, eLpNorm_measure_zero, ENNReal.toReal_zero]

Premises used: ENNReal.toReal_zero, MeasureTheory.eLpNorm_measure_zero, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
simp_rw₁ : ENNReal.toReal 0 = 0
⊢ ‖f‖ = 0

Tactic:
simp_rw [norm_def, eLpNorm_exponent_zero, ENNReal.toReal_zero]

Premises used: MeasureTheory.eLpNorm_exponent_zero, ENNReal.toReal_zero, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
rw : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E) ↔ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
⊢ f = 0 ↔ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
rw [Lp.ext_iff]

Premises used: MeasureTheory.Lp.ext_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E) ↔ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
EventuallyEq.congr_right AEEqFun.coeFn_zero

Premises used: Filter.EventuallyEq.congr_right, MeasureTheory.AEEqFun.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E) ↔ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
exact EventuallyEq.congr_right AEEqFun.coeFn_zero

Premises used: Filter.EventuallyEq.congr_right, MeasureTheory.AEEqFun.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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

Tactic:
simp [hf]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
refine : ∀ (hf : ‖f‖₊ = 0), f = 0
⊢ ‖f‖₊ = 0 ↔ f = 0

Tactic:
refine ⟨fun hf => ?_, fun hf => by simp [hf]⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0

Tactic:
simp_rw [nnnorm_def, ENNReal.toNNReal_eq_zero_iff, eLpNorm_ne_top, or_false] at hf

Premises used: ENNReal.toNNReal_eq_zero_iff, MeasureTheory.Lp.nnnorm_def, or_false, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
simp_rw : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
simp_rw₁ : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0
⊢ f = 0

Tactic:
simp_rw [eq_zero_iff_ae_eq_zero, ← eLpNorm_eq_zero_iff (Lp.aestronglyMeasurable f) hp.ne.symm, hf]

Premises used: MeasureTheory.Lp.eq_zero_iff_ae_eq_zero, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.eLpNorm_eq_zero_iff, Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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

Tactic:
NNReal.coe_eq_zero.trans (nnnorm_eq_zero_iff hp)

Premises used: MeasureTheory.Lp.nnnorm_eq_zero_iff, NNReal.coe_eq_zero, ENNReal.toReal, Iff.trans, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
rw₃ rw₄ : (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal = (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal
⊢ ‖-f‖₊ = ‖f‖₊

Tactic:
rw [nnnorm_def, nnnorm_def, eLpNorm_congr_ae (coeFn_neg _), eLpNorm_neg]

Premises used: MeasureTheory.Lp.nnnorm_def, MeasureTheory.eLpNorm_neg, MeasureTheory.Lp.coeFn_neg, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ ‖-f‖ = ‖f‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) (nnnorm_neg f)

Premises used: MeasureTheory.Lp.nnnorm_neg, congr_arg, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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‖₊
simp : (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toNNReal
⊢ ‖f‖₊ ≤ c * ‖g‖₊

Tactic:
simp only [nnnorm_def]

Premises used: MeasureTheory.Lp.nnnorm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ ≤ c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ

Tactic:
have := eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul h p
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ ≠ ∞
hb : c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ ≠ ∞
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toNNReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toNNReal

Tactic:
rwa [← ENNReal.toNNReal_le_toNNReal, ENNReal.smul_def, smul_eq_mul, ENNReal.toNNReal_mul,
    ENNReal.toNNReal_coe] at this

Premises used: ENNReal.smul_def, ENNReal.toNNReal_le_toNNReal, ENNReal.toNNReal_coe, ENNReal.toNNReal_mul, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 (↑(↑g : α →ₘ[μ] F) : α → F) p μ ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ
⊢ c • eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ ≠ ∞

Tactic:
exact ENNReal.mul_ne_top ENNReal.coe_ne_top (by finiteness)

Premises used: ENNReal.mul_ne_top, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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‖
inr : ∀ (hc : c < 0), ‖f‖ ≤ c * ‖g‖
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
rcases le_or_gt 0 c with hc | hc

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
⊢ 0 ≤ c

Tactic:
hc
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
inl :
  ∀ (c : ℝ≥0) (h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑c : ℝ) * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖),
    ‖f‖ ≤ (↑c : ℝ) * ‖g‖
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
lift c to ℝ≥0 using hc
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑c : ℝ) * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ ‖f‖ ≤ (↑c : ℝ) * ‖g‖

Tactic:
NNReal.coe_le_coe.mpr (nnnorm_le_mul_nnnorm_of_ae_le_mul h)

Premises used: Iff.mpr, MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul, NNReal.toReal, NNReal.coe_le_coe