awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 :
  (toSimpleFunc (f - g) : (a : α) → E) a =
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
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)
have h₁ : (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) ((↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a) ((toSimpleFunc g : (a : α) → E) a : E)
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 g : ↥(simpleFunc E p μ)
a : α
h_1 :
  (toSimpleFunc (f - g) : (a : α) → E) a =
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
h_2 : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h : (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) ((↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a) ((toSimpleFunc g : (a : α) → E) a : E)
have h₁ : (↑((↑(↑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 =
    (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(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 g : ↥(simpleFunc E p μ)
a : α
h_1 :
  (toSimpleFunc (f - g) : (a : α) → E) a =
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a
h_2 : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h_3 : (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h :
  (↑((↑(↑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 =
    (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
have h₁ : (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a =
  (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(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 g : ↥(simpleFunc E p μ)
a : α
h h₁ :
  ∀
    (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)
⊢ (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₂ : ∀
  (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 →
        (↑((↑(↑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: 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 μ)
a : α
h h₁ :
  ∀
    (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)
h₂ :
  ∀
    (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 →
          (↑((↑(↑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)
⊢ (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₃ : ∀
  (h :
    (toSimpleFunc (f - g) : (a : α) → E) a =
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a)
  (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) ((↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a) ((toSimpleFunc g : (a : α) → E) a : E)
Tactic: repeat' intro h; rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(simpleFunc E p μ)
⊢ (⇑(toSimpleFunc (k • f)) : (a : α) → E) =ᶠ[ae μ] HSMul.hSMul (β := (a : α) → E) k (⇑(toSimpleFunc f) : (a : α) → E)
have h : ∀ (a : α),
  (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(↑(k • f) : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = (k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)) a →
        (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := (a : α) → E) k (⇑(toSimpleFunc f) : (a : α) → E) a
Tactic: filter_upwards [toSimpleFunc_eq_toFun (k • f), toSimpleFunc_eq_toFun f,
    Lp.coeFn_smul k (f : Lp E p μ)] with _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
⊢ (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(↑(k • f) : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = (k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)) a →
        (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := (a : α) → E) k (⇑(toSimpleFunc f) : (a : α) → E) a
have h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a →
  (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
Tactic: simp only [Pi.smul_apply, coe_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a
⊢ (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
have h₁ : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
  (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
h_1 : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a
h : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
have h₁ : (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
  (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑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
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
h_1 : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a
h_2 : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
h : (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
have h₁ : k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑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
𝕜 : Type u_6
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
h h₁ :
  ∀ (h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a),
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
⊢ (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
have h₂ : ∀ (h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a),
  (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a =
        HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
Tactic: repeat intro h; rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
h h₁ :
  ∀ (h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a),
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
h₂ :
  ∀ (h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a),
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a =
          HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
⊢ (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (toSimpleFunc (k • f) : (a : α) → E) a = HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
have h₃ : ∀ (h : (toSimpleFunc (k • f) : (a : α) → E) a = (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a)
  (h : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a),
  (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
    (↑(↑(k • (↑f : ↥(Lp E p μ))) : α →ₘ[μ] E) : α → E) a = k • (↑(↑(↑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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃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 μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
⊢ P f
have rw : P ((toSimpleFunc f).toLp sorry)
Tactic: rw [← toLp_toSimpleFunc f]
-- 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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃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 μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
⊢ P f
have suffices : ∀ (f : α →ₛ E) (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
Tactic: suffices ∀ f : α →ₛ E, ∀ hf : MemLp f p μ, P (toLp f hf) by
    rw [← toLp_toSimpleFunc f]
    apply this
-- 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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃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 μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
⊢ ∀ (f : α →ₛ E) (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
have const : ∀ (c : E) {s : Set α} (hs : MeasurableSet s)
  (hf :
    MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
      p μ),
  P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
Tactic: apply SimpleFunc.induction
-- 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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃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 μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
const :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s)
    (hf :
      MemLp.{u_1, u_4} (ε := E)
        (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p μ),
    P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
⊢ ∀ (f : α →ₛ E) (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
have add₁ : ∀ ⦃f g : α →ₛ E⦄,
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
      (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
    (∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)) →
      (∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)) →
        ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ), P ((f + g).toLp hf)
Tactic: apply SimpleFunc.induction
-- 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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃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 μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
have pos : ∀ (hc : c = 0), P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
Tactic: by_cases hc : c = 0