awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
obtain :
  ∀ (f' : SimpleFunc α G'') (hf' : 0 ≤ f')
    (hff' : (↑(↑(↑f : ↥(Lp G'' 1 μ)) : α →ₘ[μ] G'') : α → G'') =ᶠ[ae μ] (⇑f' : (a : α) → G'')),
    0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
obtain ⟨f', hf', hff'⟩ := exists_simpleFunc_nonneg_ae_eq hf

Premises used: MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq
-- 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
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : (↑(↑(↑f : ↥(Lp G'' 1 μ)) : α →ₘ[μ] G'') : α → G'') =ᶠ[ae μ] (⇑f' : (a : α) → G'')
⊢ EventuallyEq.{u_1, u_7} (β := G'') (ae μ) (⇑(toSimpleFunc f) : (a : α) → G'') (⇑f' : (a : α) → G'')

Tactic:
replace hff' : simpleFunc.toSimpleFunc f =ᵐ[μ] f' :=
    (Lp.simpleFunc.toSimpleFunc_eq_toFun f).trans hff'
-- 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
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : EventuallyEq.{u_1, u_7} (β := G'') (ae μ) (⇑(toSimpleFunc f) : (a : α) → G'') (⇑f' : (a : α) → G'')
rw : 0 ≤ SimpleFunc.setToSimpleFunc T f'
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rw [SimpleFunc.setToSimpleFunc_congr _ h_zero h_add (SimpleFunc.integrable _) hff']

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- 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
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : EventuallyEq.{u_1, u_7} (β := G'') (ae μ) (⇑(toSimpleFunc f) : (a : α) → G'') (⇑f' : (a : α) → G'')
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T f'

Tactic:
SimpleFunc.setToSimpleFunc_nonneg' T hT_nonneg _ hf' ((SimpleFunc.integrable f).congr hff')

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.Integrable.congr, MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'
-- 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
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : EventuallyEq.{u_1, u_7} (β := G'') (ae μ) (⇑(toSimpleFunc f) : (a : α) → G'') (⇑f' : (a : α) → G'')
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T f'

Tactic:
exact
    SimpleFunc.setToSimpleFunc_nonneg' T hT_nonneg _ hf' ((SimpleFunc.integrable f).congr hff')

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.Integrable.congr, MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'
-- 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 : IsOrderedAddMonoid G''
inst_7 : 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 g : ↥(simpleFunc G'' 1 μ)
hfg : f ≤ g
rw : ∀ (hfg : 0 ≤ g - f), 0 ≤ setToL1S T g - setToL1S T f
⊢ setToL1S T f ≤ setToL1S T g

Tactic:
rw [← sub_nonneg] at hfg ⊢

Premises used: sub_nonneg
-- 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 : IsOrderedAddMonoid G''
inst_7 : 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 g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
rw : 0 ≤ setToL1S T (g - f)
⊢ 0 ≤ setToL1S T g - setToL1S T f

Tactic:
rw [← setToL1S_sub h_zero h_add]

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S_sub
-- 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 : IsOrderedAddMonoid G''
inst_7 : 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 g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T (g - f)

Tactic:
setToL1S_nonneg h_zero h_add hT_nonneg hfg

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S_nonneg
-- 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 : IsOrderedAddMonoid G''
inst_7 : 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 g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T (g - f)

Tactic:
exact setToL1S_nonneg h_zero h_add hT_nonneg hfg

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S_nonneg
-- 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 α
C : ℝ
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F) (0 : F)

Tactic:
setToL1S_zero_left _

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_zero_left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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 : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F) (0 : F)

Tactic:
setToL1S_zero_left' h_zero f

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_zero_left', MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(simpleFunc E 1 μ)
x : Set α
h_1 : MeasurableSet x
h_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ : T' x = T' x
⊢ T x = T' x

Tactic:
rw [h]
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1S_congr_left T T' h f

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_congr_left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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 C' : ℝ
μ' : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : (↑(↑(↑f : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑f' : ↥(Lp E 1 μ')) : α →ₘ[μ'] E) : α → E)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((setToL1SCLM α E μ' hT' : (a : ↥(simpleFunc E 1 μ')) → F) f' : F)

Tactic:
setToL1S_congr_measure T (fun _ => hT.eq_zero_of_measure_zero) hT.1 hμ _ _ h

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure, Finset.sum
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(simpleFunc E 1 μ)
⊢ (setToL1SCLM α E μ ⋯ : (a : ↥(simpleFunc E 1 μ)) → F) f =
    HAdd.hAdd (α := F) (β := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1S_add_left T T' f

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_add_left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
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 μ)
⊢ (setToL1SCLM α E μ hT'' : (a : ↥(simpleFunc E 1 μ)) → F) f =
    HAdd.hAdd (α := F) (β := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1S_add_left' T T' T'' h_add f

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_add_left', MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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 c : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(simpleFunc E 1 μ)
⊢ (setToL1SCLM α E μ (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) ⋯ : (a : ↥(simpleFunc E 1 μ)) → F) f =
    HSMul.hSMul (β := F) c ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1S_smul_left T c f

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum, MeasureTheory.L1.SimpleFunc.setToL1S_smul_left
-- 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 C' c : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' 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 μ)
⊢ (setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → F) f =
    HSMul.hSMul (β := F) c ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1S_smul_left' T T' c h_smul f

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.L1.SimpleFunc.setToL1S_smul_left', Finset.sum
-- 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 : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ ‖setToL1SCLM α E μ hT‖ ≤ C

Tactic:
LinearMap.mkContinuous_norm_le _ hC _

Premises used: Set.Mem, LinearMap.mkContinuous_norm_le, MeasureTheory.L1.SimpleFunc.setToL1SCLM
-- 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 : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1SCLM α E μ hT‖ ≤ max C 0

Tactic:
LinearMap.mkContinuous_norm_le' _ _

Premises used: Set.Mem, LinearMap.mkContinuous_norm_le', MeasureTheory.L1.SimpleFunc.setToL1SCLM
-- 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
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : E
⊢ Eq.{u_3 + 1} (α := F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) (indicatorConst 1 (s := univ) ⋯ ⋯ x) : F)
    ((T univ : (a : E) → F) x : F)

Tactic:
setToL1S_const (fun _ => hT.eq_zero_of_measure_zero) hT.1 x

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, MeasureTheory.L1.SimpleFunc.setToL1S_const, And.left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α) (x : E), LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : ↥(simpleFunc E 1 μ)
⊢ LE.le.{u_8} (α := G'') ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → G'') f : G'')
    ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → G'') f : G'')

Tactic:
SimpleFunc.setToSimpleFunc_mono_left T T' hTT' _

Premises used: Multiset.sum, MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E), LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : ↥(simpleFunc E 1 μ)
⊢ LE.le.{u_8} (α := G'') ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → G'') f : G'')
    ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → G'') f : G'')

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

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum, 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''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') f : G'')

Tactic:
setToL1S_nonneg (fun _ => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg hf

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_nonneg, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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 : IsOrderedAddMonoid G'
inst_7 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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 g : ↥(simpleFunc G' 1 μ)
hfg : f ≤ g
⊢ LE.le.{u_8} (α := G'') ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') f : G'')
    ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') g : G'')

Tactic:
setToL1S_mono (fun _ => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg hfg

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.L1.SimpleFunc.setToL1S_mono, Finset.sum
-- 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 : Module 𝕜 F
inst_7 : IsBoundedSMul 𝕜 E
inst_8 : IsBoundedSMul 𝕜 F
inst_9 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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)
f : ↥(simpleFunc E 1 μ)
apply :
  DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
⊢ Eq.{u_3 + 1} (α := F) ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing

Premises used: ContinuousLinearMap.extend_eq