awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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
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
⊢ (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:
repeat intro h; 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 g : ↥(simpleFunc E p μ)
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
⊢ (⇑(toSimpleFunc (f - g)) : (a : α) → E) =ᶠ[ae μ]
    HSub.hSub (α := (a : α) → E) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc g) : (a : α) → E)

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 _

Premises used: HSub.hSub, MeasureTheory.Lp.coeFn_sub, Subtype.val, 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 α
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)
⊢ (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:
simp only [AddSubgroup.coe_sub, Pi.sub_apply]

Premises used: AddSubgroup.coe_sub, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
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)
⊢ (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:
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 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
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)
⊢ (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]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
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
⊢ (↑((↑(↑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]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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
h₁ 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
⊢ (↑((↑(↑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]
-- 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
k : 𝕜
f : ↥(simpleFunc E p μ)
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
⊢ (⇑(toSimpleFunc (k • f)) : (a : α) → E) =ᶠ[ae μ] HSMul.hSMul (β := (a : α) → E) k (⇑(toSimpleFunc f) : (a : α) → E)

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (k • f), toSimpleFunc_eq_toFun f,
    Lp.coeFn_smul k (f : Lp E p μ)] with _

Premises used: MeasureTheory.Lp.coeFn_smul, HSMul.hSMul, Subtype.val, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- 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
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)
⊢ (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:
simp only [Pi.smul_apply, coe_smul]

Premises used: MeasureTheory.Lp.simpleFunc.coe_smul, Pi.smul_apply
-- 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
k : 𝕜
f : ↥(simpleFunc E p μ)
a : α
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 =
        HSMul.hSMul (β := E) k ((toSimpleFunc f : (a : α) → E) a : E)
⊢ (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:
rw [h]
-- 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
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
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
⊢ (↑(↑(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]
-- 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
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
h₁ 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]
-- 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
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)
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
⊢ (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:
repeat intro h; rw [h]
-- 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 : ↥(simpleFunc E p μ)
⊢ ‖f‖ = (eLpNorm.{u_1, u_4} (ε := E) (⇑(toSimpleFunc f) : (a : α) → E) p μ).toReal

Tactic:
simpa [toLp_toSimpleFunc] using norm_toLp (toSimpleFunc f) (simpleFunc.memLp f)

Premises used: MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc, MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.Lp.simpleFunc.memLp, MeasureTheory.Lp.simpleFunc.norm_toLp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ Eq (α := ↥(Lp E p μ)) (↑(indicatorConst p (s := s) hs hμs c) : ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c)

Tactic:
rfl

Premises used: Set.indicator, MeasureTheory.indicatorConstLp, MeasureTheory.MemLp.toLp, Set.piecewise, rfl, ite
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (⇑(toSimpleFunc (indicatorConst p (s := s) hs hμs c)) : (a : α) → E)
    (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
Lp.simpleFunc.toSimpleFunc_toLp _ _

Premises used: MeasureTheory.Lp.simpleFunc.indicatorConst, MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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)
rw : P ((toSimpleFunc f).toLp ⋯)
⊢ P f

Tactic:
rw [← toLp_toSimpleFunc f]

Premises used: MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 ((toSimpleFunc f).toLp ⋯)

Tactic:
apply this
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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 μ)
suffices : ∀ (f : α →ₛ E) (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
⊢ P f

Tactic:
suffices ∀ f : α →ₛ E, ∀ hf : MemLp f p μ, P (toLp f hf) by
    rw [← toLp_toSimpleFunc f]
    apply this
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
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)
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)
⊢ ∀ (f : α →ₛ E) (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)

Tactic:
apply SimpleFunc.induction