awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
⊢ Eq.{u_5 + 1} (α := G → ℝ)
    (fun (a : G) ↦
      (HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞)).toReal)
    fun (x : G) ↦
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have e_f : ∀ (x : G),
  (HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
⊢ (HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have e_f : ‖x‖ₑ.toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) =
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
Tactic: rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm,
      ENNReal.toReal_ofReal (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
e_f :
  ‖x‖ₑ.toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
⊢ (HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have e_f₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖ₑ.toReal =
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
Tactic: rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm,
      ENNReal.toReal_ofReal (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
e_f :
  ‖x‖ₑ.toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
e_f₁ :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖ₑ.toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
⊢ (HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have e_f₂ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) *
    (ENNReal.ofReal ‖x‖).toReal =
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
Tactic: rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm,
      ENNReal.toReal_ofReal (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
e_f :
  ‖x‖ₑ.toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
e_f₁ :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖ₑ.toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
e_f₂ :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) *
      (ENNReal.ofReal ‖x‖).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
⊢ (HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have e_f₃ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖ =
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
Tactic: rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm,
      ENNReal.toReal_ofReal (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
h : x ∈ (toSimpleFunc f).range
⊢ HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
have pos : ∀ (hx0 : x = 0),
  HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
h : x ∈ (toSimpleFunc f).range
pos :
  ∀ (hx0 : x = 0),
    HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
      ∞
⊢ HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
have neg : ∀ (hx0 : ¬x = 0),
  HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
h : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
have pos : HMul.hMul (β := ℝ≥0∞) (enorm.{u_5} (E := G) 0)
    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {0}) : ℝ≥0∞) ≠
  ∞
Tactic: rw [hx0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
x : G
h : x ∈ (toSimpleFunc f).range
hx0 : ¬x = 0
⊢ HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
have neg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)
    (∞ : ℝ≥0∞) →
  HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞
Tactic: finiteness [SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E)
⊢ setToL1S T f = setToL1S T f'
have refine : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc f') : (a : α) → E)
Tactic: refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc f') : (a : α) → E)
have refine : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)
Tactic: refine (toSimpleFunc_eq_toFun f).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E)
⊢ (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)
have suffices : (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)
Tactic: suffices (f' : α → E) =ᵐ[μ] simpleFunc.toSimpleFunc f' from h.trans this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E)
⊢ (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)
have goal' : (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ'] (⇑(toSimpleFunc f') : (a : α) → E)
Tactic: have goal' : (f' : α → E) =ᵐ[μ'] simpleFunc.toSimpleFunc f' := (toSimpleFunc_eq_toFun f').symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (f + g) = setToL1S T f + setToL1S T g
have simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
  SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)
Tactic: simp_rw [setToL1S]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)
have rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)
Tactic: rw [← SimpleFunc.setToSimpleFunc_add T h_add (SimpleFunc.integrable f)
      (SimpleFunc.integrable g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (-f) = -setToL1S T f
have simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Tactic: simp_rw [setToL1S]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have this : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (-f)) : (a : α) → E) (⇑(-toSimpleFunc f) : (a : α) → E)
Tactic: have : simpleFunc.toSimpleFunc (-f) =ᵐ[μ] ⇑(-simpleFunc.toSimpleFunc f) :=
    neg_toSimpleFunc f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
this : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (-f)) : (a : α) → E) (⇑(-toSimpleFunc f) : (a : α) → E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have rw : SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Tactic: rw [SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (f - g) = setToL1S T f - setToL1S T g
have rw : setToL1S T (f + -g) = setToL1S T f - setToL1S T g
Tactic: rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
rw : setToL1S T (f + -g) = setToL1S T f - setToL1S T g
⊢ setToL1S T (f - g) = setToL1S T f - setToL1S T g
have rw₁ : setToL1S T f + setToL1S T (-g) = setToL1S T f - setToL1S T g
Tactic: rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
rw : setToL1S T (f + -g) = setToL1S T f - setToL1S T g
rw₁ : setToL1S T f + setToL1S T (-g) = setToL1S T f - setToL1S T g
⊢ setToL1S T (f - g) = setToL1S T f - setToL1S T g
have rw₂ : setToL1S T f + -setToL1S T g = setToL1S T f - setToL1S T g
Tactic: rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
rw : setToL1S T (f + -g) = setToL1S T f - setToL1S T g
rw₁ : setToL1S T f + setToL1S T (-g) = setToL1S T f - setToL1S T g
rw₂ : setToL1S T f + -setToL1S T g = setToL1S T f - setToL1S T g
⊢ setToL1S T (f - g) = setToL1S T f - setToL1S T g
have rw₃ : setToL1S T f + -setToL1S T g = setToL1S T f + -setToL1S T g
Tactic: rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (c • f) = c • setToL1S T f
have simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Tactic: simp_rw [setToL1S]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
Tactic: rw [← SimpleFunc.setToSimpleFunc_smul_real T h_add c (SimpleFunc.integrable f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
have refine : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)
Tactic: refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : IsBoundedSMul 𝕜 E
inst_7 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (c • f) = c • setToL1S T f
have simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Tactic: simp_rw [setToL1S]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : IsBoundedSMul 𝕜 E
inst_7 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
Tactic: rw [← SimpleFunc.setToSimpleFunc_smul T h_add h_smul c (SimpleFunc.integrable f)]