awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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''
inst_6 : OrderClosedTopology 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 : α → E
hG'' : CompleteSpace G''
hf : Integrable f μ
pos :
  LE.le.{u_8} (α := G'') ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (Integrable.toL1 f hf) : G'')
    ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (Integrable.toL1 f hf) : G'')
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf]

Premises used: MeasureTheory.setToFun_eq
-- 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''
inst_6 : OrderClosedTopology 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 : α → E
hG'' : CompleteSpace G''
hf : Integrable f μ
⊢ LE.le.{u_8} (α := G'') ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (Integrable.toL1 f hf) : G'')
    ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (Integrable.toL1 f hf) : G'')

Tactic:
L1.setToL1_mono_left' hT hT' hTT' _

Premises used: MeasureTheory.L1.setToL1_mono_left'
-- 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''
inst_6 : OrderClosedTopology 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 : α → E
hG'' : CompleteSpace G''
hf : Integrable f μ
⊢ LE.le.{u_8} (α := G'') ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (Integrable.toL1 f hf) : G'')
    ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (Integrable.toL1 f hf) : G'')

Tactic:
exact L1.setToL1_mono_left' hT hT' hTT' _

Premises used: MeasureTheory.L1.setToL1_mono_left'
-- 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''
inst_6 : OrderClosedTopology 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 : α → E
hG'' : CompleteSpace G''
hf : ¬Integrable f μ
neg : LE.le.{u_8} (α := G'') 0 0
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf, le_rfl]

Premises used: le_rfl, MeasureTheory.setToFun_undef
-- 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''
inst_6 : OrderClosedTopology 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 : ↥(Lp E 1 μ)
⊢ setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E) ≤ setToFun μ T' hT' (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
setToFun_mono_left' hT hT' (fun s _ _ x => hTT' s x) f

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.setToFun_mono_left', Subtype.val
-- 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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
pos : ∀ (hG'' : CompleteSpace G''), 0 ≤ setToFun μ T hT f
neg : ∀ (hG'' : ¬CompleteSpace G''), 0 ≤ setToFun μ T hT f
⊢ 0 ≤ setToFun μ T hT f

Tactic:
by_cases hG'' : CompleteSpace G''

Premises used: CompleteSpace
-- 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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
hG'' : ¬CompleteSpace G''
⊢ 0 ≤ setToFun μ T hT f

Tactic:
simp [setToFun, hG'']

Premises used: MeasureTheory.setToFun
-- 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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
hG'' : CompleteSpace G''
pos : ∀ (hfi : Integrable f μ), 0 ≤ setToFun μ T hT f
neg : ∀ (hfi : ¬Integrable f μ), 0 ≤ setToFun μ T hT f
⊢ 0 ≤ setToFun μ T hT f

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- 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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
hG'' : CompleteSpace G''
hfi : Integrable f μ
pos : LE.le.{u_8} (α := G'') (0 : G'') ((L1.setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (Integrable.toL1 f hfi) : G'')
⊢ 0 ≤ setToFun μ T hT f

Tactic:
simp_rw [setToFun_eq _ hfi]

Premises used: MeasureTheory.setToFun_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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
hG'' : CompleteSpace G''
hfi : Integrable f μ
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((L1.setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (Integrable.toL1 f hfi) : G'')

Tactic:
L1.setToL1_nonneg hT hT_nonneg hf

Premises used: MeasureTheory.L1.setToL1_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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
hG'' : CompleteSpace G''
hfi : Integrable f μ
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((L1.setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (Integrable.toL1 f hfi) : G'')

Tactic:
exact L1.setToL1_nonneg hT hT_nonneg hf

Premises used: MeasureTheory.L1.setToL1_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'
inst_7 : ClosedIciTopology 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'
hf : 0 ≤ᶠ[ae μ] f
hG'' : CompleteSpace G''
hfi : ¬Integrable f μ
neg : LE.le.{u_8} (α := G'') 0 0
⊢ 0 ≤ setToFun μ T hT f

Tactic:
simp_rw [setToFun_undef _ hfi, le_rfl]

Premises used: le_rfl, MeasureTheory.setToFun_undef
-- 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'
inst_7 : ClosedIciTopology G''
inst_8 : IsOrderedAddMonoid 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 : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
rw : 0 ≤ setToFun μ T hT (g - f)
⊢ setToFun μ T hT f ≤ setToFun μ T hT g

Tactic:
rw [← sub_nonneg, ← setToFun_sub hT hg hf]

Premises used: MeasureTheory.setToFun_sub, 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 : NormedSpace ℝ G'
inst_7 : ClosedIciTopology G''
inst_8 : IsOrderedAddMonoid 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 : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ 0 ≤ setToFun μ T hT (g - f)

Tactic:
setToFun_nonneg hT hT_nonneg (hfg.mono fun a ha => ?_)

Premises used: MeasureTheory.setToFun_nonneg, Filter.Eventually.mono
-- 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'
inst_7 : ClosedIciTopology G''
inst_8 : IsOrderedAddMonoid 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 : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
refine : ∀ (a : α) (ha : f a ≤ g a), 0 a ≤ (g - f) a
⊢ 0 ≤ setToFun μ T hT (g - f)

Tactic:
refine setToFun_nonneg hT hT_nonneg (hfg.mono fun a ha => ?_)

Premises used: MeasureTheory.setToFun_nonneg, Filter.Eventually.mono
-- 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'
inst_7 : ClosedIciTopology G''
inst_8 : IsOrderedAddMonoid 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 : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
a : α
ha rw : f a ≤ g a
⊢ 0 a ≤ (g - f) a

Tactic:
rw [Pi.sub_apply, Pi.zero_apply, sub_nonneg]

Premises used: Pi.zero_apply, sub_nonneg, Pi.sub_apply
-- 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'
inst_7 : ClosedIciTopology G''
inst_8 : IsOrderedAddMonoid 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 : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
⊢ f a ≤ g a

Tactic:
ha
-- 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'
inst_7 : ClosedIciTopology G''
inst_8 : IsOrderedAddMonoid 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 : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
⊢ f a ≤ g a

Tactic:
exact ha
-- 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
pos :
  ∀ (hF : CompleteSpace F),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
      setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)
neg :
  ∀ (hF : ¬CompleteSpace F),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
      setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- 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
hF : ¬CompleteSpace F
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
simp [setToFun, hF, continuous_const]

Premises used: continuous_const, MeasureTheory.setToFun
-- 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
hF : CompleteSpace F
pos :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
simp_rw [L1.setToFun_eq_setToL1 hT]

Premises used: MeasureTheory.L1.setToFun_eq_setToL1
-- 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
hF : CompleteSpace F
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f

Tactic:
ContinuousLinearMap.continuous _

Premises used: ContinuousLinearMap.continuous
-- 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
hF : CompleteSpace F
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f

Tactic:
exact ContinuousLinearMap.continuous _

Premises used: ContinuousLinearMap.continuous
-- 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
inl :
  ∀ (hfsi : ∀ᶠ (i : ι) in ⊥, Integrable (fs i) μ)
    (hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) ⊥ (𝓝 0)),
    Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) ⊥ (𝓝 (setToFun μ T hT f))
inr : ∀ (hl : l.NeBot), Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
rcases eq_or_neBot l with rfl | hl

Premises used: Filter.eq_or_neBot, 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 α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
hfsi : ∀ᶠ (i : ι) in ⊥, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) ⊥ (𝓝 0)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) ⊥ (𝓝 (setToFun μ T hT f))

Tactic:
simp
-- 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
⊢ ∃ (i : ι), ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1 ∧ Integrable (fs i) μ

Tactic:
(((tendsto_order.1 hfs).2 _ zero_lt_one).and hfsi).exists

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, zero_lt_one, And.right, Iff.mp
-- 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
obtain : ∀ (i : ι) (hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1) (h'i : Integrable (fs i) μ), Integrable f μ
⊢ Integrable f μ

Tactic:
obtain ⟨i, hi, h'i⟩ : ∃ i, ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ < 1 ∧ Integrable (fs i) μ :=
      (((tendsto_order.1 hfs).2 _ zero_lt_one).and hfsi).exists

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, zero_lt_one, And.right, Iff.mp
-- 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
⊢ Integrable (fs i - f) μ

Tactic:
have : Integrable (fs i - f) μ := ⟨h'i.aestronglyMeasurable.sub hf, hi.trans one_lt_top⟩
-- 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ Integrable (fs i - (fs i - f)) μ

Tactic:
h'i.sub this

Premises used: MeasureTheory.Integrable.sub