awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
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 μ
h : Eq (α := α → ε') (∑ i ∈ s, f i) fun (a : α) ↦ ∑ i ∈ s, f i a
⊢ MemLp.{u_1, u_4} (ε := ε') (∑ i ∈ s, f i) p μ

Tactic:
convert! memLp_finsetSum s hf using 1

Premises used: MeasureTheory.memLp_finsetSum
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
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 μ
h : ∀ (x : α), Eq.{u_4 + 1} (α := ε') ((∑ i ∈ s, f i) x) (∑ i ∈ s, f i x)
⊢ Eq (α := α → ε') (∑ i ∈ s, f i) fun (a : α) ↦ ∑ i ∈ s, f i a

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
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 μ
x : α
⊢ Eq.{u_4 + 1} (α := ε') ((∑ i ∈ s, f i) x) (∑ i ∈ s, f i x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
e_a : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm = ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm) ^ (1 / q) = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ‖f a‖ₑ ^ q

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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 = ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ

Tactic:
exact lintegral_trim hm (by fun_prop)

Premises used: MeasureTheory.lintegral_trim
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
simp_rw : Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Tactic:
simp_rw [limsup_eq]

Premises used: Filter.limsup_eq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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}
rw rw₁ : Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})
⊢ Eq (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a}) (sInf {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a})

Tactic:
rw [h_set_eq]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
suffices : 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})

Tactic:
suffices h_set_eq : { a : ℝ≥0∞ | ∀ᵐ n ∂μ.trim hm, f n ≤ a } = { a : ℝ≥0∞ | ∀ᵐ n ∂μ, f n ≤ a } by
    rw [h_set_eq]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
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
⊢ Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
ext1 a
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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
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∞)
⊢ 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:
simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]

Premises used: Set.mem_setOf_eq, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h :
  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

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]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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∞)

Tactic:
(trim_measurableSet_eq hm ?_).symm

Premises used: MeasureTheory.trim_measurableSet_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h : MeasurableSet.{u_1} (α := α) {x : α | ¬f x ≤ a}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)
    ((μ.trim hm : (a : Set α) → ℝ≥0∞) {x : α | ¬f x ≤ a} : ℝ≥0∞)

Tactic:
refine (trim_measurableSet_eq hm ?_).symm

Premises used: MeasureTheory.trim_measurableSet_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ MeasurableSet.{u_1} (α := α) {x : α | ¬f x ≤ a}

Tactic:
(measurableSet_le hf measurable_const).compl

Premises used: measurableSet_le, Set.Mem, setOf, MeasurableSet.compl, measurable_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ MeasurableSet.{u_1} (α := α) {x : α | ¬f x ≤ a}

Tactic:
exact (measurableSet_le hf measurable_const).compl

Premises used: measurableSet_le, MeasurableSet.compl, measurable_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Tactic:
limsup_trim hm hf

Premises used: MeasureTheory.limsup_trim
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Tactic:
exact limsup_trim hm hf

Premises used: MeasureTheory.limsup_trim
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ eLpNormEssSup f (μ.trim hm) = eLpNormEssSup f μ

Tactic:
essSup_trim _ (@StronglyMeasurable.enorm _ m _ _ _ _ hf)

Premises used: MeasureTheory.StronglyMeasurable.enorm, MeasureTheory.essSup_trim, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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 μ
neg : ∀ (h0 : ¬p = 0), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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 μ

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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 μ
neg : ∀ (h_top : ¬p = ∞), eLpNorm f p (μ.trim hm) = eLpNorm f p μ
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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
h_top : p = ∞
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
simpa only [h_top, eLpNorm_exponent_top] using eLpNormEssSup_trim hm hf

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_trim
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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
h_top : ¬p = ∞
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
simpa only [eLpNorm_eq_eLpNorm' h0 h_top] using eLpNorm'_trim hm hf

Premises used: MeasureTheory.eLpNorm'_trim, MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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)
rw : eLpNorm (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
rw [eLpNorm_congr_ae hf.ae_eq_mk, eLpNorm_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk)]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_eq_of_ae_eq_trim, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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 (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ

Tactic:
eLpNorm_trim hm hf.stronglyMeasurable_mk

Premises used: MeasureTheory.eLpNorm_trim, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
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 (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ

Tactic:
exact eLpNorm_trim hm hf.stronglyMeasurable_mk

Premises used: MeasureTheory.eLpNorm_trim, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim
Goal:
α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : MemLp f p (μ.trim hm)
⊢ MemLp f p μ

Tactic:
⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf.1,
    (le_of_eq (eLpNorm_trim_ae hm hf.1).symm).trans_lt hf.2⟩

Premises used: MeasureTheory.MemLp, MeasureTheory.eLpNorm_trim_ae, And.right, And.left, And.intro, le_of_eq, aestronglyMeasurable_of_aestronglyMeasurable_trim, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_6
E : Type u_7
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
⊢ eLpNorm (↑(AEEqFun.mk f hf) : α → E) p μ = eLpNorm f p μ

Tactic:
eLpNorm_congr_ae (AEEqFun.coeFn_mk _ _)

Premises used: MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_6
E : Type u_7
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
hfp : MemLp f p μ
⊢ eLpNorm (↑(AEEqFun.mk f ⋯) : α → E) p μ < ∞

Tactic:
simp [hfp.2]

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 g : α →ₘ[μ] E
hf : Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} f
hg : Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} g
⊢ Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} (f + g)

Tactic:
simp [eLpNorm_congr_ae (AEEqFun.coeFn_add f g),
      eLpNorm_add_lt_top ⟨f.aestronglyMeasurable, hf⟩ ⟨g.aestronglyMeasurable, hg⟩]

Premises used: MeasureTheory.eLpNorm_add_lt_top, MeasureTheory.AEEqFun.coeFn_add, And.intro, MeasureTheory.AEEqFun.aestronglyMeasurable, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 α
⊢ Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} 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:
α_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 μ < ∞
rwa₂ rwa₃ rwa₄ rwa₅ : eLpNorm (↑f : α → E) p μ < ∞
⊢ Membership.mem (γ := Set (α →ₘ[μ] E)) {f : α →ₘ[μ] E | eLpNorm (↑f : α → E) p μ < ∞} (-f)

Tactic:
rwa [Set.mem_setOf_eq, eLpNorm_congr_ae (AEEqFun.coeFn_neg f), eLpNorm_neg]

Premises used: MeasureTheory.AEEqFun.coeFn_neg, Set.mem_setOf_eq, MeasureTheory.eLpNorm_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 : α → E
h : MemLp f p μ
⊢ (↑(toLp f h) : α →ₘ[μ] E) = AEEqFun.mk f ⋯

Tactic:
rfl

Premises used: rfl, MeasureTheory.AEEqFun.mk
-- 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 μ
⊢ (↑(↑(toLp f hf) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] f

Tactic:
AEEqFun.coeFn_mk _ _

Premises used: MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.AEEqFun.mk
-- 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 μ
hfg : f =ᶠ[ae μ] g
⊢ toLp f hf = toLp g hg

Tactic:
simp [toLp, hfg]

Premises used: MeasureTheory.MemLp.toLp
-- 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 μ
⊢ toLp f hf = toLp g hg ↔ f =ᶠ[ae μ] g

Tactic:
simp [toLp]

Premises used: MeasureTheory.MemLp.toLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
h : MemLp.{u_1, u_4} (ε := E) 0 p μ
⊢ toLp 0 h = 0

Tactic:
rfl

Premises used: Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- 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 μ
⊢ toLp (f + g) ⋯ = toLp f hf + toLp g hg

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.comp₂, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- 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 μ
⊢ toLp (-f) ⋯ = -toLp f hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- 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 μ
⊢ toLp (f - g) ⋯ = toLp f hf - toLp g hg

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.comp₂, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- 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 μ)
h : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)
a : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ f = g

Tactic:
ext
-- 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 μ)
h : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
h
-- 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 μ)
h : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α →ₘ[μ] E
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f ↔ eLpNorm (↑f : α → E) p μ < ∞

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α →ₘ[μ] E
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f ↔ MemLp (↑f : α → E) p μ

Tactic:
simp [mem_Lp_iff_eLpNorm_lt_top, MemLp, f.stronglyMeasurable.aestronglyMeasurable]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.MemLp, MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top, MeasureTheory.AEEqFun.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
p q : ℝ≥0∞
hpq : p ≤ q
⊢ LE.le (α := AddSubgroup (α →ₘ[μ] E)) (Lp E q μ) (Lp E p μ)

Tactic:
fun f hf => (MemLp.mono_exponent ⟨f.aestronglyMeasurable, hf⟩ hpq).2

Premises used: Set.Mem, setOf, MeasureTheory.MemLp.mono_exponent, And.right, And.intro, MeasureTheory.AEEqFun.aestronglyMeasurable
-- 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 : eLpNorm (↑f : α → E) p μ < ∞
⊢ (↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x) f hf) :
          α →ₘ[μ] E) :
      α → E) =
    (↑f : α → E)

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 : α →ₘ[μ] E
hf : eLpNorm (↑f : α → E) p μ < ∞
⊢ (↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x) f hf) :
      α →ₘ[μ] E) =
    f

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 μ)
hf : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
⊢ MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) hf = f

Tactic:
simp [MemLp.toLp]

Premises used: MeasureTheory.MemLp.toLp
-- 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 μ)
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ < ∞

Tactic:
f.prop

Premises used: Set.Mem, setOf, Subtype.prop
-- 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 μ)
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≠ ∞

Tactic:
(eLpNorm_lt_top f).ne

Premises used: MeasureTheory.Lp.eLpNorm_lt_top, 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 μ)
⊢ StronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
f.val.stronglyMeasurable

Premises used: MeasureTheory.AEEqFun.stronglyMeasurable, Subtype.val
-- 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 μ)
⊢ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ

Tactic:
f.val.aestronglyMeasurable

Premises used: MeasureTheory.AEEqFun.aestronglyMeasurable, Subtype.val
-- 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 μ)
⊢ MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ

Tactic:
⟨Lp.aestronglyMeasurable f, f.prop⟩

Premises used: MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.MemLp, Subtype.prop, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0

Tactic:
AEEqFun.coeFn_zero

Premises used: 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 μ] -(↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_neg _

Premises used: MeasureTheory.AEEqFun.coeFn_neg