awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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'')
have 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}
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
-- 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 : 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}
⊢ ∀ (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'')
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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 }
⊢ LE.le.{u_8} (α := G'') (0 : G'')
    ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) : G'')
have this : (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) = (↑(↑g : ↥(simpleFunc G' 1 μ)) : ↥(Lp G' 1 μ))
Tactic: have : (coeSimpleFuncNonnegToLpNonneg 1 μ G' g : α →₁[μ] G') = (g : α →₁ₛ[μ] G') := 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 : 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'')
    ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) : ↥(Lp G' 1 μ)) : G'')
have refine_2 : LE.le.{u_8} (α := G'') (0 : G'')
  ((setToL1SCLM α G' μ hT : (a : ↥(simpleFunc G' 1 μ)) → G'') (↑g : ↥(simpleFunc G' 1 μ)) : G'')
Tactic: rw [this, setToL1_eq_setToL1SCLM]
-- 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 : 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
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') f : G'')
    ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') g : G'')
have 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'')
Tactic: rw [← sub_nonneg] at hfg ⊢
Cleared hypotheses: hfg
-- 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 : 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 : 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'')
have rw : LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (g - f) : G'')
Tactic: rw [← (setToL1 hT).map_sub]
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1 hT‖ ≤ (↑1 : ℝ) * ‖setToL1SCLM α E μ hT‖
have α₁ : ∀ (x : ↥(simpleFunc E 1 μ)),
  ‖x‖ = (↑1 : ℝ) * norm (E := ↥(Lp E 1 μ)) ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
Tactic: refine
        ContinuousLinearMap.opNorm_extend_le (setToL1SCLM α E μ hT)
          (simpleFunc.denseRange one_ne_top) fun x => le_of_eq ?_
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
⊢ ‖x‖ = (↑1 : ℝ) * norm (E := ↥(Lp E 1 μ)) ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
have rw : ‖x‖ = norm (E := ↥(Lp E 1 μ)) ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
Tactic: rw [NNReal.coe_one, one_mul]
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ (↑1 : ℝ) * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
have rw : 1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
Tactic: rw [NNReal.coe_one, one_mul]
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
rw : 1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
⊢ (↑1 : ℝ) * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
have rw₁ : ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
Tactic: rw [NNReal.coe_one, one_mul]
-- 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 : ↥(Lp E 1 μ)
⊢ setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E) = (setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f
have rw : Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) sorry) : F)
  ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
Tactic: rw [setToFun_eq hT (L1.integrable_coeFn f), Integrable.toL1_coeFn]
-- 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 : ↥(Lp E 1 μ)
rw :
  Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : F)
    ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
⊢ setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E) = (setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f
have rw₁ : Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
Tactic: rw [setToFun_eq hT (L1.integrable_coeFn f), Integrable.toL1_coeFn]
-- 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = 0
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = 0
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = 0
⊢ setToFun μ T hT f = 0
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = 0
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
⊢ setToFun μ T hT f = setToFun μ T' hT' f
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
⊢ setToFun μ T hT f = setToFun μ T' hT' f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
⊢ 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
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 : α → E
hF : CompleteSpace F
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
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 : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
  ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left T T' hT hT' h]
-- 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 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 : α → E
⊢ setToFun μ T hT f = setToFun μ T' hT' f
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
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 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 : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
⊢ setToFun μ T hT f = setToFun μ T' hT' f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
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 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 : α → E
hF : CompleteSpace F
⊢ 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
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 : α → E
hF : CompleteSpace F
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
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 : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
  ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left' T T' hT hT' h]
-- 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
have pos : ∀ (hF : CompleteSpace F), setToFun μ (T + T') sorry f = setToFun μ T hT f + setToFun μ T' hT' f
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ (T + T') sorry f = setToFun μ T hT f + setToFun μ T' hT' f
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
have pos : ∀ (hf : Integrable f μ), setToFun μ (T + T') sorry 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
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 : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ (T + T') sorry 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
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 : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
have pos : (L1.setToL1 sorry : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) =
  HAdd.hAdd (α := F) (β := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
    ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: simp_rw [setToFun_eq _ hf, L1.setToL1_add_left hT 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
have neg : 0 = HAdd.hAdd (α := F) 0 0
Tactic: simp_rw [setToFun_undef _ hf, add_zero]
-- 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 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 : α → E
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f
have pos : ∀ (hF : CompleteSpace F), setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f
Tactic: by_cases hF : CompleteSpace F