awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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‖
e_f₃ 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‖
⊢ (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:
rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm,
      ENNReal.toReal_ofReal (norm_nonneg _)]

Premises used: ENNReal.toReal_ofReal, ENNReal.toReal_mul, mul_comm, ofReal_norm, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
_ :
  x ∈ (toSimpleFunc f).range →
    HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
      ∞
⊢ x ∈ (toSimpleFunc f).range →
    HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
      ∞

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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∞) ≠
      ∞
neg :
  ∀ (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∞) ≠
    ∞

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
pos :
  HMul.hMul (β := ℝ≥0∞) (enorm.{u_5} (E := G) 0)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {0}) : ℝ≥0∞) ≠
    ∞
⊢ HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞) ≠
    ∞

Tactic:
rw [hx0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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∞) (enorm.{u_5} (E := G) 0)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {0}) : ℝ≥0∞) ≠
    ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
neg neg₁ neg₂ 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∞) ≠
      ∞
⊢ 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]

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, MeasureTheory.L1.SimpleFunc.integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T f = SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rfl

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S, rfl
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 α
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) (setToL1S 0 f) 0

Tactic:
SimpleFunc.setToSimpleFunc_zero _

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_zero, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T f = 0

Tactic:
SimpleFunc.setToSimpleFunc_zero' h_zero _ (SimpleFunc.integrable f)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_zero', MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc g) : (a : α) → E)
⊢ setToL1S T f = setToL1S T g

Tactic:
SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) h

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T f = setToL1S T' f

Tactic:
SimpleFunc.setToSimpleFunc_congr_left T T' h (simpleFunc.toSimpleFunc f) (SimpleFunc.integrable f)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left, MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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'

Tactic:
SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) ?_

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
refine : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc f') : (a : α) → E)
⊢ setToL1S T f = setToL1S T f'

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) ?_

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)

Tactic:
(toSimpleFunc_eq_toFun f).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
refine : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc f') : (a : α) → E)

Tactic:
refine (toSimpleFunc_eq_toFun f).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
suffices : (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)
⊢ (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)

Tactic:
suffices (f' : α → E) =ᵐ[μ] simpleFunc.toSimpleFunc f' from h.trans this
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)

Tactic:
have goal' : (f' : α → E) =ᵐ[μ'] simpleFunc.toSimpleFunc f' := (toSimpleFunc_eq_toFun f').symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
goal' : (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ'] (⇑(toSimpleFunc f') : (a : α) → E)
⊢ (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)

Tactic:
hμ.ae_eq goal'

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
goal' : (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ'] (⇑(toSimpleFunc f') : (a : α) → E)
⊢ (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E) =ᶠ[ae μ] (⇑(toSimpleFunc f') : (a : α) → E)

Tactic:
exact hμ.ae_eq goal'

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 T' : Set α → E →L[ℝ] F
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S (T + T') f = setToL1S T f + setToL1S T' f

Tactic:
SimpleFunc.setToSimpleFunc_add_left T T'

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_add_left, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T'' f = setToL1S T f + setToL1S T' f

Tactic:
SimpleFunc.setToSimpleFunc_add_left' T T' T'' h_add (SimpleFunc.integrable f)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_add_left', MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S (fun (s : Set α) ↦ c • T s) f = c • setToL1S T f

Tactic:
SimpleFunc.setToSimpleFunc_smul_left T c _

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 T' : Set α → E →L[ℝ] F
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T' f = c • setToL1S T f

Tactic:
SimpleFunc.setToSimpleFunc_smul_left' T T' c h_smul (SimpleFunc.integrable f)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left', MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
simp_rw :
  SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)
⊢ setToL1S T (f + g) = setToL1S T f + setToL1S T g

Tactic:
simp_rw [setToL1S]

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 :
  SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)

Tactic:
rw [← SimpleFunc.setToSimpleFunc_add T h_add (SimpleFunc.integrable f)
      (SimpleFunc.integrable g)]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_add, MeasureTheory.L1.SimpleFunc.integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 + toSimpleFunc g)

Tactic:
SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _)
      (add_toSimpleFunc f g)

Premises used: MeasureTheory.Lp.simpleFunc.add_toSimpleFunc, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 + toSimpleFunc g)

Tactic:
exact
    SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _)
      (add_toSimpleFunc f g)

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
⊢ setToL1S T (-f) = -setToL1S T f

Tactic:
simp_rw [setToL1S]

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
rw : SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rw [SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) this]

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)

Tactic:
SimpleFunc.setToSimpleFunc_neg T h_add (SimpleFunc.integrable f)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_neg, MeasureTheory.L1.SimpleFunc.integrable