awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp.{u_1, u_4} (ε := E) (⇑(piecewise s hs (const α c) (const α 0)) : (a : α) → E) p μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : Eq.{u_1 + 1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑(const α c) : (a : α) → E)) Set.univ
Tactic: have : Function.support (const α c) = Set.univ := Function.support_const hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 α
f g : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
t : α →ₛ E
ht : AEEqFun.mk (⇑t : (a : α) → E) ⋯ = (↑g : α →ₘ[μ] E)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {f : ↥(Lp E p μ) | ∃ (s : α →ₛ E), AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)} (f + g)
have h : AEEqFun.mk (⇑(s + t) : (a : α) → E) sorry = (↑(f + g) : α →ₘ[μ] E)
Tactic: use s + t
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 α
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {f : ↥(Lp E p μ) | ∃ (s : α →ₛ E), AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)} (-f)
have h : AEEqFun.mk (⇑(-s) : (a : α) → E) sorry = (↑(-f) : α →ₘ[μ] E)
Tactic: use -s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(simpleFunc E p μ)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) (k • (↑f : ↥(Lp E p μ)))
have rcases : ∀ (f : ↥(Lp E p μ)) (s : α →ₛ E) (hs : AEEqFun.mk (⇑s : (a : α) → E) sorry = (↑f : α →ₘ[μ] E)),
  Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ)
    (k •
      (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f
            sorry) :
        ↥(Lp E p μ)))
Tactic: rcases f with ⟨f, ⟨s, hs⟩⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ)
    (k •
      (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f
            ⋯) :
        ↥(Lp E p μ)))
have h : AEEqFun.mk (⇑(k • s) : (a : α) → E) sorry =
  (↑(k •
        (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)
              f sorry) :
          ↥(Lp E p μ))) :
    α →ₘ[μ] E)
Tactic: use k • s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
⊢ AEEqFun.mk (⇑(k • s) : (a : α) → E) ⋯ =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)
have apply : HSMul.hSMul (β := α →ₘ[μ] E) k (AEEqFun.mk (⇑s : (a : α) → E) sorry) =
  (↑(k •
        (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)
              f sorry) :
          ↥(Lp E p μ))) :
    α →ₘ[μ] E)
Tactic: apply Eq.trans (AEEqFun.smul_mk k s s.aestronglyMeasurable).symm _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(Lp E p μ)
s : α →ₛ E
hs : AEEqFun.mk (⇑s : (a : α) → E) ⋯ = (↑f : α →ₘ[μ] E)
⊢ HSMul.hSMul (β := α →ₘ[μ] E) k (AEEqFun.mk (⇑s : (a : α) → E) ⋯) =
    (↑(k •
          (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x) f ⋯) :
            ↥(Lp E p μ))) :
      α →ₘ[μ] E)
have rw : k • (↑f : α →ₘ[μ] E) =
  (↑(k •
        (↑(Subtype.mk (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)
              f sorry) :
          ↥(Lp E p μ))) :
    α →ₘ[μ] E)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 = x • y • f
have a : (↑((x * y) • f) : ↥(Lp E p μ)) = (↑(x • y • f) : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 = f
have a : (↑(HSMul.hSMul (α := 𝕜) 1 f) : ↥(Lp E p μ)) = (↑f : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 = 0
have a : (↑(HSMul.hSMul (β := ↥(simpleFunc E p μ)) x 0) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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) = x • f + x • g
have a : (↑(x • (f + g)) : ↥(Lp E p μ)) = (↑(x • f + x • g) : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 = x • f + y • f
have a : (↑((x + y) • f) : ↥(Lp E p μ)) = (↑(x • f + y • f) : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 = 0
have a : (↑(HSMul.hSMul (α := 𝕜) 0 f) : ↥(Lp E p μ)) = (↑0 : ↥(Lp E p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ] (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)
have h : (↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) = AEEqFun.mk (⇑(toSimpleFunc f) : (a : α) → E) sorry
Tactic: convert! (AEEqFun.coeFn_mk (toSimpleFunc f) (toSimpleFunc f).aestronglyMeasurable).symm using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) (⇑f : (a : α) → E)
have rw : AEEqFun.mk (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) sorry = AEEqFun.mk (⇑f : (a : α) → E) sorry
Tactic: rw [← AEEqFun.mk_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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) ⋯
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) (⇑f : (a : α) → E)
have rw₁ : AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) μ
Tactic: rw [← AEEqFun.mk_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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) μ
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (f.toLp hfi)) : (a : α) → E) (⇑f : (a : α) → E)
have rw₂ : AEStronglyMeasurable.{u_1, u_4} (β := E) (⇑f : (a : α) → E) μ
Tactic: rw [← AEEqFun.mk_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (p := p) (μ := μ) 0) : (a : α) → E) 0
have 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)
Tactic: filter_upwards [toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ),
    Lp.coeFn_zero E 1 μ] with _ h₁ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
have h : Eq.{u_4 + 1} (α := E) ((↑(↑(↑0 : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a) (0 a)
Tactic: rwa [h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (-f)) : (a : α) → E) (-(⇑(toSimpleFunc f) : (a : α) → E))
have 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)
Tactic: filter_upwards [toSimpleFunc_eq_toFun (-f), toSimpleFunc_eq_toFun f,
    Lp.coeFn_neg (f : Lp E p μ)] with _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
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)
have 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)
Tactic: simp only [Pi.neg_apply, AddSubgroup.coe_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
have 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
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ (↑(-(↑(↑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
have 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
have h₁ : -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a : α
h h₁ :
  ∀ (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)
have h₂ : ∀ (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 →
      (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(toSimpleFunc f : (a : α) → E) a
Tactic: repeat intro h; rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a : α
h h₁ :
  ∀ (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)
h₂ :
  ∀ (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 →
        (↑(-(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a = -(toSimpleFunc f : (a : α) → E) 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)
have h₃ : ∀ (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 = -(↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
Tactic: repeat intro h; rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
⊢ (⇑(toSimpleFunc (f - g)) : (a : α) → E) =ᶠ[ae μ]
    HSub.hSub (α := (a : α) → E) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc g) : (a : α) → E)
have h : ∀ (a : α),
  (toSimpleFunc (f - g) : (a : α) → E) a = (↑(↑(↑(f - g) : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑(↑((↑f : ↥(Lp E p μ)) - (↑g : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a =
            ((↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)) a →
          (toSimpleFunc (f - g) : (a : α) → E) a =
            HSub.hSub (α := (a : α) → E) (β := (a : α) → E) (⇑(toSimpleFunc f) : (a : α) → E)
              (⇑(toSimpleFunc g) : (a : α) → E) a
Tactic: filter_upwards [toSimpleFunc_eq_toFun (f - g), toSimpleFunc_eq_toFun f,
    toSimpleFunc_eq_toFun g, Lp.coeFn_sub (f : Lp E p μ) g] with _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a : α
⊢ (toSimpleFunc (f - g) : (a : α) → E) a = (↑(↑(↑(f - g) : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑(↑((↑f : ↥(Lp E p μ)) - (↑g : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a =
            ((↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)) a →
          (toSimpleFunc (f - g) : (a : α) → E) a =
            HSub.hSub (α := (a : α) → E) (β := (a : α) → E) (⇑(toSimpleFunc f) : (a : α) → E)
              (⇑(toSimpleFunc g) : (a : α) → E) a
have h : (toSimpleFunc (f - g) : (a : α) → E) a =
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a →
  (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
          (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (toSimpleFunc (f - g) : (a : α) → E) a =
          HSub.hSub (α := E) (β := E) ((toSimpleFunc f : (a : α) → E) a : E) ((toSimpleFunc g : (a : α) → E) a : E)
Tactic: simp only [AddSubgroup.coe_sub, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a : α
h :
  (toSimpleFunc (f - g) : (a : α) → E) a =
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
⊢ (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
          (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (toSimpleFunc (f - g) : (a : α) → E) a =
          HSub.hSub (α := E) (β := E) ((toSimpleFunc f : (a : α) → E) a : E) ((toSimpleFunc g : (a : α) → E) a : E)
have h₁ : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
  (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
        (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
        HSub.hSub (α := E) (β := E) ((toSimpleFunc f : (a : α) → E) a : E) ((toSimpleFunc g : (a : α) → E) a : E)
Tactic: rw [h]