awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : 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
rw : LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (g - f) : G'')
⊢ 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 [← (setToL1 hT).map_sub]

Premises used: ContinuousLinearMap.map_sub, MeasureTheory.L1.setToL1
-- 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 : 0 ≤ g - f
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (g - f) : G'')

Tactic:
setToL1_nonneg hT hT_nonneg hfg

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 : 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
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (g - f) : G'')

Tactic:
exact setToL1_nonneg hT hT_nonneg hfg

Premises used: MeasureTheory.L1.setToL1_nonneg
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1 hT‖ ≤ (↑1 : ℝ) * ‖setToL1SCLM α E μ hT‖

Tactic:
ContinuousLinearMap.opNorm_extend_le (setToL1SCLM α E μ hT)
          (simpleFunc.denseRange one_ne_top) fun x => le_of_eq ?_

Premises used: Set.Mem, ContinuousLinearMap.opNorm_extend_le, MeasureTheory.Lp.simpleFunc.denseRange, MeasureTheory.L1.SimpleFunc.setToL1SCLM, MeasureTheory.L1.setToL1, le_of_eq, ENNReal.one_ne_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 α
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 μ))
⊢ ‖setToL1 hT‖ ≤ (↑1 : ℝ) * ‖setToL1SCLM α E μ hT‖

Tactic:
refine
        ContinuousLinearMap.opNorm_extend_le (setToL1SCLM α E μ hT)
          (simpleFunc.denseRange one_ne_top) fun x => le_of_eq ?_

Premises used: ContinuousLinearMap.opNorm_extend_le, MeasureTheory.L1.SimpleFunc.setToL1SCLM, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
rw : ‖x‖ = norm (E := ↥(Lp E 1 μ)) ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
⊢ ‖x‖ = (↑1 : ℝ) * 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]

Premises used: NNReal.coe_one, one_mul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
⊢ ‖x‖ = norm (E := ↥(Lp E 1 μ)) ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))

Tactic:
simp [coeToLp]

Premises used: MeasureTheory.Lp.simpleFunc.coeToLp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
rw : 1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
rw₁ rw₂ : ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
⊢ (↑1 : ℝ) * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖

Tactic:
rw [NNReal.coe_one, one_mul]

Premises used: NNReal.coe_one, one_mul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
f : ↥(Lp E 1 μ)
⊢ norm.{u_3} (E := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ≤ C * ‖f‖

Tactic:
calc
    ‖setToL1 hT f‖ ≤ ‖setToL1SCLM α E μ hT‖ * ‖f‖ :=
      ContinuousLinearMap.le_of_opNorm_le _ (norm_setToL1_le_norm_setToL1SCLM hT) _
    _ ≤ C * ‖f‖ := mul_le_mul (norm_setToL1SCLM_le hT hC) le_rfl (norm_nonneg _) hC

Premises used: Trans.trans, le_rfl, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, ContinuousLinearMap.le_of_opNorm_le, mul_le_mul, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ norm.{u_3} (E := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ≤ max C 0 * ‖f‖

Tactic:
calc
    ‖setToL1 hT f‖ ≤ ‖setToL1SCLM α E μ hT‖ * ‖f‖ :=
      ContinuousLinearMap.le_of_opNorm_le _ (norm_setToL1_le_norm_setToL1SCLM hT) _
    _ ≤ max C 0 * ‖f‖ :=
      mul_le_mul (norm_setToL1SCLM_le' hT) le_rfl (norm_nonneg _) (le_max_right _ _)

Premises used: le_max_right, Trans.trans, le_rfl, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, ContinuousLinearMap.le_of_opNorm_le, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le', mul_le_mul, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ ‖setToL1 hT‖ ≤ C

Tactic:
ContinuousLinearMap.opNorm_le_bound _ hC (norm_setToL1_le_mul_norm hT hC)

Premises used: ContinuousLinearMap.opNorm_le_bound, MeasureTheory.L1.norm_setToL1_le_mul_norm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1 hT‖ ≤ max C 0

Tactic:
ContinuousLinearMap.opNorm_le_bound _ (le_max_right _ _) (norm_setToL1_le_mul_norm' hT)

Premises used: le_max_right, ContinuousLinearMap.opNorm_le_bound, MeasureTheory.L1.norm_setToL1_le_mul_norm'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ LipschitzWith (α := ↥(Lp E 1 μ)) (β := F) C.toNNReal (⇑(setToL1 hT) : (a : ↥(Lp E 1 μ)) → F)

Tactic:
(setToL1 hT).lipschitz.weaken (norm_setToL1_le' hT)

Premises used: ContinuousLinearMap.lipschitz, MeasureTheory.L1.norm_setToL1_le', LipschitzWith.weaken, MeasureTheory.L1.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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
ι : Type u_7
fs : ι → ↥(Lp E 1 μ)
l : Filter ι
hfs : Tendsto fs l (𝓝 f)
⊢ Tendsto.{u_7, u_3} (β := F) (fun (i : ι) ↦ ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (fs i) : F)) l
    (𝓝 ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f) : Filter F)

Tactic:
((setToL1 hT).continuous.tendsto _).comp hfs

Premises used: Continuous.tendsto, ContinuousLinearMap.continuous, MeasureTheory.L1.setToL1, Filter.Tendsto.comp
-- 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 : ℝ
f : α → E
hF : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ setToFun μ T hT f = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf)

Tactic:
simp [setToFun, hF, hf]

Premises used: 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 : ℝ
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)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
⊢ setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E) = (setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f

Tactic:
rw [setToFun_eq hT (L1.integrable_coeFn f), Integrable.toL1_coeFn]

Premises used: MeasureTheory.Integrable.toL1_coeFn, MeasureTheory.L1.integrable_coeFn, MeasureTheory.setToFun_eq
-- 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = 0
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = 0
⊢ setToFun μ T hT f = 0

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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
hF : CompleteSpace F
⊢ setToFun μ T hT f = 0

Tactic:
simp [setToFun, hF, hf]

Premises used: 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = 0

Tactic:
simp [setToFun, hF]

Premises used: 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬AEStronglyMeasurable f μ
⊢ setToFun μ T hT f = 0

Tactic:
setToFun_undef hT (not_and_of_not_left _ hf)

Premises used: MeasureTheory.setToFun_undef, not_and_of_not_left
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
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
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
⊢ setToFun μ T hT f = setToFun μ T' hT' f

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 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

Tactic:
simp [setToFun, hF]

Premises used: 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 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
neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f = setToFun μ T' hT' f
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
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)
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left T T' hT hT' h]

Premises used: MeasureTheory.L1.setToL1_congr_left, MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf]

Premises used: MeasureTheory.setToFun_undef
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ T' hT' f
⊢ setToFun μ T hT f = setToFun μ T' hT' f

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 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

Tactic:
simp [setToFun, hF]

Premises used: 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 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
neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f = setToFun μ T' hT' f
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
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)
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left' T T' hT hT' h]

Premises used: MeasureTheory.L1.setToL1_congr_left', MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf]

Premises used: MeasureTheory.setToFun_undef
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f
neg : ∀ (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

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 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

Tactic:
simp [setToFun, hF]

Premises used: 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 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
neg : ∀ (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

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  (L1.setToL1 ⋯ : (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)
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_add_left hT hT']

Premises used: MeasureTheory.L1.setToL1_add_left, MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
neg : 0 = HAdd.hAdd (α := F) 0 0
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf, add_zero]

Premises used: MeasureTheory.setToFun_undef, add_zero