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 : CompleteSpace G''
inst_7 : 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'')
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') c : G'') ((T' s : (a : E) → G'') c : G'')

Tactic:
exact hTT' s hs hμs c
-- 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 : CompleteSpace G''
inst_7 : 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 g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
hg_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
add :
  HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
      ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'') ≤
    HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')

Tactic:
rw [(setToL1 hT).map_add, (setToL1 hT').map_add]

Premises used: ContinuousLinearMap.map_add, MeasureTheory.L1.setToL1
-- 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 : CompleteSpace G''
inst_7 : 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 g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
hg_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
⊢ HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
      ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'') ≤
    HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')

Tactic:
add_le_add hf_le hg_le

Premises used: add_le_add
-- 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 : CompleteSpace G''
inst_7 : 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 g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
hg_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
⊢ HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
      ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'') ≤
    HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')

Tactic:
exact add_le_add hf_le hg_le

Premises used: add_le_add
-- 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 : CompleteSpace G''
inst_7 : 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'')
⊢ IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
        ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')}

Tactic:
isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Premises used: isClosed_le, ContinuousLinearMap.continuous, MeasureTheory.L1.setToL1
-- 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 : CompleteSpace G''
inst_7 : 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'')
⊢ IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
        ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')}

Tactic:
exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Premises used: isClosed_le, ContinuousLinearMap.continuous, MeasureTheory.L1.setToL1
-- 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 : CompleteSpace G''
inst_7 : 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 : ↥(Lp E 1 μ)
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le.{u_8} (α := G'')
      ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      ∀
        (hf_le :
          LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
            ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G''))
        (hg_le :
          LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
            ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')),
        LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
          ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
isClosed :
  IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
        ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')}
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')

Tactic:
induction f using Lp.induction (hp_ne_top := one_ne_top) with
  | @indicatorConst c s hs hμs =>
    rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
    exact hTT' s hs hμs c
  | @add f g hf hg _ hf_le hg_le =>
    rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
    exact add_le_add hf_le hg_le
  | isClosed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Premises used: MeasureTheory.Lp.simpleFunc.indicatorConst, isClosed_le, ContinuousLinearMap.map_add, ContinuousLinearMap.continuous, MeasureTheory.L1.setToL1
-- 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 : CompleteSpace G''
inst_7 : 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 μ)
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')

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

Premises used: MeasureTheory.L1.setToL1_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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
suffices :
  ∀ (f : { g : ↥(Lp G' 1 μ) // 0 ≤ g }),
    LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑f : ↥(Lp G' 1 μ)) : G'')
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') f : G'')

Tactic:
suffices ∀ f : { g : α →₁[μ] G' // 0 ≤ g }, 0 ≤ setToL1 hT f from
    this (⟨f, hf⟩ : { g : α →₁[μ] G' // 0 ≤ g })
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
⊢ ∀ (f : { g : ↥(Lp G' 1 μ) // 0 ≤ g }),
    LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑f : ↥(Lp G' 1 μ)) : G'')

Tactic:
fun g =>
    @isClosed_property { g : α →₁ₛ[μ] G' // 0 ≤ g } { g : α →₁[μ] G' // 0 ≤ g } _ _
      (fun g => 0 ≤ setToL1 hT g)
      (denseRange_coeSimpleFuncNonnegToLpNonneg 1 μ G' one_ne_top) ?_ ?_ g

Premises used: isClosed_property, MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg, OfNat.ofNat, ENNReal.one_ne_top
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
refine_1 :
  ∀ (g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }),
    IsClosed (X := { g : ↥(Lp G' 1 μ) // 0 ≤ g })
      {x : { g : ↥(Lp G' 1 μ) // 0 ≤ g } |
        (fun (g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }) ↦
            LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑g : ↥(Lp G' 1 μ)) : G''))
          x}
refine_2 :
  ∀ (g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }) (a : { g : ↥(simpleFunc G' 1 μ) // 0 ≤ g }),
    (fun (g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }) ↦
        LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑g : ↥(Lp G' 1 μ)) : G''))
      (coeSimpleFuncNonnegToLpNonneg 1 μ G' a)
⊢ ∀ (f : { g : ↥(Lp G' 1 μ) // 0 ≤ g }),
    LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑f : ↥(Lp G' 1 μ)) : G'')

Tactic:
refine fun g =>
    @isClosed_property { g : α →₁ₛ[μ] G' // 0 ≤ g } { g : α →₁[μ] G' // 0 ≤ g } _ _
      (fun g => 0 ≤ setToL1 hT g)
      (denseRange_coeSimpleFuncNonnegToLpNonneg 1 μ G' one_ne_top) ?_ ?_ g

Premises used: isClosed_property, MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg, OfNat.ofNat, ENNReal.one_ne_top
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }
⊢ IsClosed (X := { g : ↥(Lp G' 1 μ) // 0 ≤ g })
    {x : { g : ↥(Lp G' 1 μ) // 0 ≤ g } |
      (fun (g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }) ↦
          LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑g : ↥(Lp G' 1 μ)) : G''))
        x}

Tactic:
(isClosed_Ici (a := 0)).preimage ((setToL1 hT).continuous.comp continuous_induced_dom)

Premises used: Set.Ici, Set.Mem, Continuous.comp, setOf, ContinuousLinearMap.continuous, Set.preimage, continuous_induced_dom, IsClosed.preimage, MeasureTheory.L1.setToL1, isClosed_Ici
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }
⊢ IsClosed (X := { g : ↥(Lp G' 1 μ) // 0 ≤ g })
    {x : { g : ↥(Lp G' 1 μ) // 0 ≤ g } |
      (fun (g : { g : ↥(Lp G' 1 μ) // 0 ≤ g }) ↦
          LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑g : ↥(Lp G' 1 μ)) : G''))
        x}

Tactic:
exact (isClosed_Ici (a := 0)).preimage ((setToL1 hT).continuous.comp continuous_induced_dom)

Premises used: Continuous.comp, ContinuousLinearMap.continuous, continuous_induced_dom, IsClosed.preimage, MeasureTheory.L1.setToL1, isClosed_Ici
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g_1 : { g : ↥(Lp G' 1 μ) // 0 ≤ g }
g : { g : ↥(simpleFunc G' 1 μ) // 0 ≤ g }
⊢ (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) = (↑(↑g : ↥(simpleFunc G' 1 μ)) : ↥(Lp G' 1 μ))

Tactic:
have : (coeSimpleFuncNonnegToLpNonneg 1 μ G' g : α →₁[μ] G') = (g : α →₁ₛ[μ] G') := rfl
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g_1 : { g : ↥(Lp G' 1 μ) // 0 ≤ g }
g : { g : ↥(simpleFunc G' 1 μ) // 0 ≤ g }
this : (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) = (↑(↑g : ↥(simpleFunc G' 1 μ)) : ↥(Lp G' 1 μ))
refine_2 :
  LE.le.{u_8} (α := G'') (0 : G'')
    ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') (↑g : ↥(simpleFunc G' 1 μ)) : G'')
⊢ LE.le.{u_8} (α := G'') (0 : G'')
    ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) : G'')

Tactic:
rw [this, setToL1_eq_setToL1SCLM]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g_1 : { g : ↥(Lp G' 1 μ) // 0 ≤ g }
g : { g : ↥(simpleFunc G' 1 μ) // 0 ≤ g }
this : (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) = (↑(↑g : ↥(simpleFunc G' 1 μ)) : ↥(Lp G' 1 μ))
⊢ LE.le.{u_8} (α := G'') (0 : G'')
    ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') (↑g : ↥(simpleFunc G' 1 μ)) : G'')

Tactic:
setToL1S_nonneg (fun s => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg g.2

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, Subtype.property
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g_1 : { g : ↥(Lp G' 1 μ) // 0 ≤ g }
g : { g : ↥(simpleFunc G' 1 μ) // 0 ≤ g }
this : (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) = (↑(↑g : ↥(simpleFunc G' 1 μ)) : ↥(Lp G' 1 μ))
⊢ LE.le.{u_8} (α := G'') (0 : G'')
    ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') (↑g : ↥(simpleFunc G' 1 μ)) : G'')

Tactic:
exact setToL1S_nonneg (fun s => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg g.2

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S_nonneg, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.left, Subtype.property
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : ClosedIciTopology G''
inst_9 : 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 : ↥(Lp G' 1 μ)
hfg : f ≤ g
rw :
  ∀ (hfg : 0 ≤ g - f),
    0 ≤
      HSub.hSub (α := G'') (β := G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') g : G'')
        ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') f : G'')
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') f : G'')
    ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') g : G'')

Tactic:
rw [← sub_nonneg] at hfg ⊢

Premises used: sub_nonneg