awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (↑((x * y) • f) : ↥(Lp E p μ)) = (↑(x • y • f) : ↥(Lp E p μ))

Tactic:
mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (↑((x * y) • f) : ↥(Lp E p μ)) = (↑(x • y • f) : ↥(Lp E p μ))

Tactic:
exact mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
a : (↑(HSMul.hSMul (α := 𝕜) 1 f) : ↥(Lp E p μ)) = (↑f : ↥(Lp E p μ))
⊢ HSMul.hSMul (α := 𝕜) 1 f = f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
⊢ (↑(HSMul.hSMul (α := 𝕜) 1 f) : ↥(Lp E p μ)) = (↑f : ↥(Lp E p μ))

Tactic:
one_smul _ _

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
⊢ (↑(HSMul.hSMul (α := 𝕜) 1 f) : ↥(Lp E p μ)) = (↑f : ↥(Lp E p μ))

Tactic:
exact one_smul _ _

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x : 𝕜
a : (↑(HSMul.hSMul (β := ↥(simpleFunc E p μ)) x 0) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))
⊢ HSMul.hSMul (β := ↥(simpleFunc E p μ)) x 0 = 0

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x : 𝕜
⊢ (↑(HSMul.hSMul (β := ↥(simpleFunc E p μ)) x 0) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x : 𝕜
⊢ (↑(HSMul.hSMul (β := ↥(simpleFunc E p μ)) x 0) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x : 𝕜
f g : ↥(simpleFunc E p μ)
a : (↑(x • (f + g)) : ↥(Lp E p μ)) = (↑(x • f + x • g) : ↥(Lp E p μ))
⊢ x • (f + g) = x • f + x • g

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x : 𝕜
f g : ↥(simpleFunc E p μ)
⊢ (↑(x • (f + g)) : ↥(Lp E p μ)) = (↑(x • f + x • g) : ↥(Lp E p μ))

Tactic:
smul_add _ _ _

Premises used: Set.Mem, smul_add
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x : 𝕜
f g : ↥(simpleFunc E p μ)
⊢ (↑(x • (f + g)) : ↥(Lp E p μ)) = (↑(x • f + x • g) : ↥(Lp E p μ))

Tactic:
exact smul_add _ _ _

Premises used: smul_add
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
a : (↑((x + y) • f) : ↥(Lp E p μ)) = (↑(x • f + y • f) : ↥(Lp E p μ))
⊢ (x + y) • f = x • f + y • f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (↑((x + y) • f) : ↥(Lp E p μ)) = (↑(x • f + y • f) : ↥(Lp E p μ))

Tactic:
add_smul _ _ _

Premises used: add_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (↑((x + y) • f) : ↥(Lp E p μ)) = (↑(x • f + y • f) : ↥(Lp E p μ))

Tactic:
exact add_smul _ _ _

Premises used: add_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
a : (↑(HSMul.hSMul (α := 𝕜) 0 f) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))
⊢ HSMul.hSMul (α := 𝕜) 0 f = 0

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
⊢ (↑(HSMul.hSMul (α := 𝕜) 0 f) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))

Tactic:
zero_smul _ _

Premises used: Set.Mem, zero_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
⊢ (↑(HSMul.hSMul (α := 𝕜) 0 f) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))

Tactic:
exact zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : Fact (1 ≤ p)
⊢ IsBoundedSMul 𝕜 ↥(simpleFunc E p μ)

Tactic:
IsBoundedSMul.of_norm_smul_le fun r f => (norm_smul_le r (f : Lp E p μ) :)

Premises used: norm_smul_le, Set.Mem, IsBoundedSMul.of_norm_smul_le, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ (↑(f.toLp hf) : ↥(Lp E p μ)) = MemLp.toLp (⇑f : (a : α) → E) hf

Tactic:
rfl

Premises used: MeasureTheory.MemLp.toLp, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ (↑(↑(f.toLp hf) : ↥(Lp E p μ)) : α →ₘ[μ] E) = AEEqFun.mk (⇑f : (a : α) → E) ⋯

Tactic:
rfl

Premises used: rfl, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ Eq (α := ↥(simpleFunc E p μ)) (toLp 0 ⋯) 0

Tactic:
rfl

Premises used: Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
⊢ (f + g).toLp ⋯ = f.toLp hf + g.toLp 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.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ (-f).toLp ⋯ = -f.toLp hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
⊢ (f - g).toLp ⋯ = f.toLp hf - g.toLp hg

Tactic:
simp only [sub_eq_add_neg, ← toLp_neg, ← toLp_add]

Premises used: sub_eq_add_neg, MeasureTheory.Lp.simpleFunc.toLp_neg, MeasureTheory.Lp.simpleFunc.toLp_add
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
c : 𝕜
⊢ (c • f).toLp ⋯ = c • f.toLp hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
f : α →ₛ E
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ ‖f.toLp hf‖ = (eLpNorm.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ).toReal

Tactic:
norm_toLp f hf

Premises used: MeasureTheory.Lp.norm_toLp, ENNReal.toReal, DFunLike.coe, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : MeasurableSpace E
f : ↥(simpleFunc E p μ)
⊢ Measurable.{u_1, u_4} (α := α) (β := E) (⇑(toSimpleFunc f) : (a : α) → E)

Tactic:
(toSimpleFunc f).measurable

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.SimpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ StronglyMeasurable.{u_1, u_4} (α := α) (β := E) (⇑(toSimpleFunc f) : (a : α) → E)

Tactic:
(toSimpleFunc f).stronglyMeasurable

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : MeasurableSpace E
f : ↥(simpleFunc E p μ)
⊢ AEMeasurable.{u_1, u_4} (β := E) (⇑(toSimpleFunc f) : (a : α) → E) μ

Tactic:
(simpleFunc.measurable f).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Lp.simpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑(toSimpleFunc f) : (a : α) → E) μ

Tactic:
(simpleFunc.stronglyMeasurable f).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Lp.simpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ (⇑(toSimpleFunc f) : (a : α) → E) =ᶠ[ae μ] (↑(AEEqFun.mk (⇑(toSimpleFunc f) : (a : α) → E) ⋯) : α → E)

Tactic:
(AEEqFun.coeFn_mk (toSimpleFunc f) (toSimpleFunc f).aestronglyMeasurable).symm

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.SimpleFunc.aestronglyMeasurable, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
h : (↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) = AEEqFun.mk (⇑(toSimpleFunc f) : (a : α) → E) ⋯
⊢ (⇑(toSimpleFunc f) : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)

Tactic:
convert! (AEEqFun.coeFn_mk (toSimpleFunc f) (toSimpleFunc f).aestronglyMeasurable).symm using 2

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.SimpleFunc.aestronglyMeasurable, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ (↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) = AEEqFun.mk (⇑(toSimpleFunc f) : (a : α) → E) ⋯

Tactic:
(Classical.choose_spec f.2).symm

Premises used: Classical.choose_spec, Eq.symm, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ (↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) = AEEqFun.mk (⇑(toSimpleFunc f) : (a : α) → E) ⋯

Tactic:
exact (Classical.choose_spec f.2).symm

Premises used: Classical.choose_spec, Eq.symm, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ MemLp.{u_1, u_4} (ε := E) (⇑(toSimpleFunc f) : (a : α) → E) p μ

Tactic:
MemLp.ae_eq (toSimpleFunc_eq_toFun f).symm <| mem_Lp_iff_memLp.mp (f : Lp E p μ).2

Premises used: MeasureTheory.Lp.mem_Lp_iff_memLp, Iff.mp, MeasureTheory.MemLp.ae_eq, Subtype.val, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun, Filter.EventuallyEq.symm, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ (toSimpleFunc f).toLp ⋯ = f

Tactic:
simpleFunc.eq' (Classical.choose_spec f.2)

Premises used: Classical.choose_spec, MeasureTheory.Lp.simpleFunc.eq', Subtype.property
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
rw : AEEqFun.mk (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) ⋯ = AEEqFun.mk (⇑f : (a : α) → E) ⋯
rw₁ : AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) μ
rw₂ : AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑f : (a : α) → E) μ
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) (⇑f : (a : α) → E)

Tactic:
rw [← AEEqFun.mk_eq_mk]

Premises used: MeasureTheory.AEEqFun.mk_eq_mk
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ AEEqFun.mk (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) ⋯ = AEEqFun.mk (⇑f : (a : α) → E) ⋯

Tactic:
Classical.choose_spec (toLp f hfi).2

Premises used: MeasureTheory.SimpleFunc.toLp, Classical.choose_spec, MeasureTheory.AEEqFun.mk, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a : α
h₁ :
  Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E)
    ((↑(↑(↑0 : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a : E)
h :
  Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) →
    Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E) (0 a : E)
⊢ Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) →
    Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E) (0 a : E)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
h :
  ∀ (a : α)
    (h₁ :
      Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E)
        ((↑(↑(↑0 : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a : E)),
    Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) →
      Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E) (0 a : E)
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (p := p) (μ := μ) 0) : (a : α) → E) 0

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ),
    Lp.coeFn_zero E 1 μ] with _ h₁ _

Premises used: MeasureTheory.Lp.coeFn_zero, OfNat.ofNat, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a : α
h₁ :
  Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E)
    ((↑(↑(↑0 : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a : E)
h_1 : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)
h h₂ h₃ h₄ : Eq.{u_4 + 1} (α := E) ((↑(↑(↑0 : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a) (0 a)
⊢ Eq.{u_4 + 1} (α := E) ((toSimpleFunc (p := p) (μ := μ) 0 : (a : α) → E) a : E) (0 a : E)

Tactic:
rwa [h₁]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
h :
  ∀ (a : α),
    (toSimpleFunc (-f) : (a : α) → E) a = (↑(↑(↑(-f) : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑(↑(-(↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = (-(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)) a →
          Eq.{u_4 + 1} (α := E) ((toSimpleFunc (-f) : (a : α) → E) a : E) ((-(⇑(toSimpleFunc f) : (a : α) → E)) a : E)
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (-f)) : (a : α) → E) (-(⇑(toSimpleFunc f) : (a : α) → E))

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (-f), toSimpleFunc_eq_toFun f,
    Lp.coeFn_neg (f : Lp E p μ)] with _

Premises used: MeasureTheory.Lp.coeFn_neg, Subtype.val, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun, Neg.neg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a : α
h :
  (toSimpleFunc (-f) : (a : α) → E) a = (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        Eq.{u_4 + 1} (α := E) ((toSimpleFunc (-f) : (a : α) → E) a : E) (-(toSimpleFunc f : (a : α) → E) a : E)
⊢ (toSimpleFunc (-f) : (a : α) → E) a = (↑(↑(↑(-f) : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(-(↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = (-(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)) a →
        Eq.{u_4 + 1} (α := E) ((toSimpleFunc (-f) : (a : α) → E) a : E) ((-(⇑(toSimpleFunc f) : (a : α) → E)) a : E)

Tactic:
simp only [Pi.neg_apply, AddSubgroup.coe_neg]

Premises used: AddSubgroup.coe_neg, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a : α
h : (toSimpleFunc (-f) : (a : α) → E) a = (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
h₁ :
  (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(toSimpleFunc f : (a : α) → E) a
⊢ (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      Eq.{u_4 + 1} (α := E) ((toSimpleFunc (-f) : (a : α) → E) a : E) (-(toSimpleFunc f : (a : α) → E) a : E)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a : α
h_1 : (toSimpleFunc (-f) : (a : α) → E) a = (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
h : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h₁ :
  (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
⊢ (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(toSimpleFunc f : (a : α) → E) a

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a : α
h_1 : (toSimpleFunc (-f) : (a : α) → E) a = (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
h_2 : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h : (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h₁ h₂ : -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
⊢ (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a

Tactic:
rw [h]