awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ setToFun μ T hT (↑(↑(indicatorConstLp (s := s) 1 hs hμs x) : α →ₘ[μ] E) : α → E) = (T s : (a : E) → F) x
have rw : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (indicatorConstLp (s := s) 1 hs hμs x) : F)
  ((T s : (a : E) → F) x : F)
Tactic: rw [L1.setToFun_eq_setToL1 hT]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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 : ℝ
inst_4 : CompleteSpace F
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
⊢ (setToFun μ T hT fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x
have this : Eq (α := α → E) (fun (x_1 : α) ↦ x) (indicator univ fun (x_1 : α) ↦ x)
Tactic: have : (fun _ : α => x) = Set.indicator univ fun _ => x := (indicator_univ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : ℝ
inst_4 : CompleteSpace F
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : Eq (α := α → E) (fun (x_1 : α) ↦ x) (indicator univ fun (x_1 : α) ↦ x)
⊢ (setToFun μ T hT fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x
have rw : setToFun μ T hT (indicator univ fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ setToFun μ T hT (⇑f : (a : α) → E) = ∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x
have h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
Tactic: have h'f : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
⊢ setToFun μ T hT (⇑f : (a : α) → E) = ∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x
have A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
Tactic: have A : f =ᵐ[μ] g := h'f.coeFn_toLp.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
⊢ setToFun μ T hT (⇑f : (a : α) → E) = ∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x
have rw : Eq.{u_3 + 1} (α := F) ((L1.SimpleFunc.setToL1SCLM α E μ hT : (a : ↥(Lp.simpleFunc E 1 μ)) → F) g : F)
  (∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
Tactic: rw [setToFun_congr_ae hT A, L1.setToFun_eq_setToL1 hT, L1.setToL1_eq_setToL1SCLM]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
⊢ Eq.{u_3 + 1} (α := F) ((L1.SimpleFunc.setToL1SCLM α E μ hT : (a : ↥(Lp.simpleFunc E 1 μ)) → F) g : F)
    (∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
have apply : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
Tactic: apply (SimpleFunc.setToSimpleFunc_congr T (fun s ↦ hT.eq_zero_of_measure_zero) hT.1 hf _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
have grw : (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
Tactic: grw [A, Lp.simpleFunc.toSimpleFunc_eq_toFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
grw : (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
have grw₁ : (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
Tactic: grw [A, Lp.simpleFunc.toSimpleFunc_eq_toFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
have pos : ∀ (hG'' : CompleteSpace G''), setToFun μ T hT f ≤ setToFun μ T' hT' f
Tactic: by_cases hG'' : CompleteSpace G''
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
pos : ∀ (hG'' : CompleteSpace G''), setToFun μ T hT f ≤ setToFun μ T' hT' f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
have neg : ∀ (hG'' : ¬CompleteSpace G''), setToFun μ T hT f ≤ setToFun μ T' hT' f
Tactic: by_cases hG'' : CompleteSpace G''
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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''
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
have pos : ∀ (hf : Integrable f μ), setToFun μ T hT f ≤ setToFun μ T' hT' f
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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''
pos : ∀ (hf : Integrable f μ), setToFun μ T hT f ≤ setToFun μ T' hT' f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f ≤ setToFun μ T' hT' f
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 μ
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
have 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'')
Tactic: simp_rw [setToFun_eq _ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 μ
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
have neg : LE.le.{u_8} (α := G'') 0 0
Tactic: simp_rw [setToFun_undef _ hf, le_rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ 0 ≤ setToFun μ T hT f
have pos : ∀ (hG'' : CompleteSpace G''), 0 ≤ setToFun μ T hT f
Tactic: by_cases hG'' : CompleteSpace G''
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ 0 ≤ setToFun μ T hT f
have neg : ∀ (hG'' : ¬CompleteSpace G''), 0 ≤ setToFun μ T hT f
Tactic: by_cases hG'' : CompleteSpace G''
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
have pos : ∀ (hfi : Integrable f μ), 0 ≤ setToFun μ T hT f
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ 0 ≤ setToFun μ T hT f
have neg : ∀ (hfi : ¬Integrable f μ), 0 ≤ setToFun μ T hT f
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 μ
⊢ 0 ≤ setToFun μ T hT f
have pos : LE.le.{u_8} (α := G'') (0 : G'') ((L1.setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (Integrable.toL1 f hfi) : G'')
Tactic: simp_rw [setToFun_eq _ hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 μ
⊢ 0 ≤ setToFun μ T hT f
have neg : LE.le.{u_8} (α := G'') 0 0
Tactic: simp_rw [setToFun_undef _ hfi, le_rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ setToFun μ T hT f ≤ setToFun μ T hT g
have rw : 0 ≤ setToFun μ T hT (g - f)
Tactic: rw [← sub_nonneg, ← setToFun_sub hT hg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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)
have refine : ∀ (a : α) (ha : f a ≤ g a), 0 a ≤ (g - f) a
Tactic: refine setToFun_nonneg hT hT_nonneg (hfg.mono fun a ha => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)
have pos : ∀ (hF : CompleteSpace F),
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)
have neg : ∀ (hF : ¬CompleteSpace F),
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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)
have pos : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f
Tactic: simp_rw [L1.setToFun_eq_setToL1 hT]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have 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))
Tactic: rcases eq_or_neBot l with rfl | hl
Cleared hypotheses: l, hfsi, hfs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have inr : ∀ (hl : l.NeBot), Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
Tactic: rcases eq_or_neBot l with rfl | hl