awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact SimpleFunc.setToSimpleFunc_neg T h_add (SimpleFunc.integrable f)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_neg, 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 μ)
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
rw₃ rw₄ : setToL1S T f + -setToL1S T g = setToL1S T f + -setToL1S T g
⊢ 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]

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S_neg, sub_eq_add_neg, MeasureTheory.L1.SimpleFunc.setToL1S_add
-- 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
c : ℝ
f : ↥(simpleFunc E 1 μ)
simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
⊢ setToL1S T (c • f) = c • 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
c : ℝ
f : ↥(simpleFunc E 1 μ)
rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rw [← SimpleFunc.setToSimpleFunc_smul_real T h_add c (SimpleFunc.integrable f)]

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real
-- 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
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

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

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
c : ℝ
f : ↥(simpleFunc E 1 μ)
refine :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

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

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
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)

Tactic:
smul_toSimpleFunc c f

Premises used: MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc
-- 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
c : ℝ
f : ↥(simpleFunc E 1 μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)

Tactic:
exact smul_toSimpleFunc c f

Premises used: MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
simp_rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
⊢ setToL1S T (c • f) = c • 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
𝕜 : 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 μ)
rw : SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rw [← SimpleFunc.setToSimpleFunc_smul T h_add h_smul c (SimpleFunc.integrable f)]

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_smul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

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

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
𝕜 : 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 μ)
refine :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

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

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
𝕜 : 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 μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)

Tactic:
smul_toSimpleFunc c f

Premises used: MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)

Tactic:
exact smul_toSimpleFunc c f

Premises used: MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc
-- 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 : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : ↥(simpleFunc E 1 μ)
rw :
  ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖
⊢ ‖setToL1S T f‖ ≤ C * ‖f‖

Tactic:
rw [setToL1S, norm_eq_sum_mul f]

Premises used: MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul, 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 : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : ↥(simpleFunc E 1 μ)
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖

Tactic:
SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm _
      (SimpleFunc.integrable f)

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_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
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : ↥(simpleFunc E 1 μ)
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖

Tactic:
exact
    SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm _
      (SimpleFunc.integrable f)

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ T ∅ = 0

Tactic:
have h_empty : T ∅ = 0 := h_zero _ MeasurableSet.empty measure_empty
-- 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) = (T s : (a : E) → F) x

Tactic:
Eq.trans ?_ (SimpleFunc.setToSimpleFunc_indicator T h_empty hs x)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_indicator, Eq.trans
-- 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
refine :
  SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) =
    SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) = (T s : (a : E) → F) x

Tactic:
refine Eq.trans ?_ (SimpleFunc.setToSimpleFunc_indicator T h_empty hs x)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_indicator, Eq.trans
-- 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) =
    SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))

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

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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
refine :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) : (a : α) → E)
    (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0)) : (a : α) → E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) =
    SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))

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

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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) : (a : α) → E)
    (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
toSimpleFunc_indicatorConst hs hμs.ne x

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst, LT.lt.ne
-- 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) : (a : α) → E)
    (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
exact toSimpleFunc_indicatorConst hs hμs.ne x

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst, LT.lt.ne
-- 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 α
inst_4 : IsFiniteMeasure μ
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
x : E
⊢ setToL1S T (indicatorConst 1 (s := univ) ⋯ ⋯ x) = (T univ : (a : E) → F) x

Tactic:
setToL1S_indicatorConst h_zero h_add MeasurableSet.univ (measure_lt_top _ _) x

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : E), LE.le.{u_7} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T f ≤ setToL1S T' f

Tactic:
SimpleFunc.setToSimpleFunc_mono_left T T' hTT' _

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left, MeasureTheory.L1.SimpleFunc.setToL1S
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
T T' : Set α → E →L[ℝ] G''
hTT' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E), LE.le.{u_7} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T f ≤ setToL1S T' f

Tactic:
SimpleFunc.setToSimpleFunc_mono_left' T T' hTT' _ (SimpleFunc.integrable f)

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f : ↥(simpleFunc G'' 1 μ)
hf : 0 ≤ f
simp_rw : 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
⊢ 0 ≤ setToL1S T f

Tactic:
simp_rw [setToL1S]

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S