awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
⊢ DominatedFinMeasAdditive (μ + μ') T' C'

Tactic:
have I' : DominatedFinMeasAdditive (μ + μ') T' C' := .add_measure_left _ _ hT' hC'
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
⊢ setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f

Tactic:
have A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f :=
    setToFun_congr_measure_of_add_left _ _ _ (hf.add_measure hf')
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
⊢ DominatedFinMeasAdditive (μ + μ') T'' C''

Tactic:
have I'' : DominatedFinMeasAdditive (μ + μ') T'' C'' := .of_measure_le hμ hT'' hC''
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ μ'' ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')

Tactic:
simpa using hμ
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
hfμ : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f

Tactic:
apply setToFun_congr_measure_of_integrable (c' := 1) (by simp) (by simpa using hμ)

Premises used: OfNat.ofNat, MeasureTheory.setToFun_congr_measure_of_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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ Integrable f (μ + μ')

Tactic:
apply hf.add_measure hf'

Premises used: MeasureTheory.Integrable.add_measure
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f

Tactic:
have A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f := by
    apply setToFun_congr_measure_of_integrable (c' := 1) (by simp) (by simpa using hμ)
    apply hf.add_measure hf'
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f
rw : setToFun (μ + μ') T'' I'' f = setToFun (μ + μ') T I f + setToFun (μ + μ') T' I' f
⊢ setToFun μ'' T'' hT'' f = setToFun μ T hT f + setToFun μ' T' hT' f

Tactic:
rw [← A, ← A', ← A'']
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T 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 + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f
⊢ setToFun (μ + μ') T'' I'' f = setToFun (μ + μ') T I f + setToFun (μ + μ') T' I' f

Tactic:
apply setToFun_add_left' _ _ _ h

Premises used: MeasureTheory.setToFun_add_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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
pos : ∀ (hF : CompleteSpace F), ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ C * ‖f‖
neg : ∀ (hF : ¬CompleteSpace F), ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ C * ‖f‖
⊢ ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ C * ‖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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
hF : ¬CompleteSpace F
neg : 0 ≤ C * ‖f‖
⊢ ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ C * ‖f‖

Tactic:
simp only [setToFun, hF, ↓reduceDIte, norm_zero]

Premises used: norm_zero, reduceDIte, MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
hF : ¬CompleteSpace F
⊢ 0 ≤ C * ‖f‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
hF : CompleteSpace F
pos : norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ≤ C * ‖f‖
⊢ ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ C * ‖f‖

Tactic:
rw [L1.setToFun_eq_setToL1]

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

Tactic:
L1.norm_setToL1_le_mul_norm hT hC f

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
hF : CompleteSpace F
⊢ norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ≤ C * ‖f‖

Tactic:
exact L1.norm_setToL1_le_mul_norm hT hC f

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
pos : ∀ (hF : CompleteSpace F), ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ max C 0 * ‖f‖
neg : ∀ (hF : ¬CompleteSpace F), ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ max C 0 * ‖f‖
⊢ ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ max C 0 * ‖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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hF : ¬CompleteSpace F
neg : 0 ≤ max C 0 * ‖f‖
⊢ ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ max C 0 * ‖f‖

Tactic:
simp only [setToFun, hF, ↓reduceDIte, norm_zero]

Premises used: norm_zero, reduceDIte, MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hF : ¬CompleteSpace F
⊢ 0 ≤ max C 0 * ‖f‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hF : CompleteSpace F
pos : norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ≤ max C 0 * ‖f‖
⊢ ‖setToFun μ T hT (↑(↑f : α →ₘ[μ] E) : α → E)‖ ≤ max C 0 * ‖f‖

Tactic:
rw [L1.setToFun_eq_setToL1]

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

Tactic:
L1.norm_setToL1_le_mul_norm' hT f

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hF : CompleteSpace F
⊢ norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ≤ max C 0 * ‖f‖

Tactic:
exact L1.norm_setToL1_le_mul_norm' hT f

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
pos : ∀ (hF : CompleteSpace F), ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖
neg : ∀ (hF : ¬CompleteSpace F), ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖
⊢ ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

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 μ
hC : 0 ≤ C
hF : ¬CompleteSpace F
neg : 0 ≤ C * ‖Integrable.toL1 f hf‖
⊢ ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
simp only [setToFun, hF, ↓reduceDIte, norm_zero]

Premises used: norm_zero, reduceDIte, 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 μ
hC : 0 ≤ C
hF : ¬CompleteSpace F
⊢ 0 ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
positivity
-- 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 μ
hC : 0 ≤ C
hF : CompleteSpace F
pos :
  norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) ≤ C * ‖Integrable.toL1 f hf‖
⊢ ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
rw [setToFun_eq hT hf]

Premises used: 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 μ
hC : 0 ≤ C
hF : CompleteSpace F
⊢ norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
L1.norm_setToL1_le_mul_norm hT hC _

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
hF : CompleteSpace F
⊢ norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
exact L1.norm_setToL1_le_mul_norm hT hC _

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
pos : ∀ (hF : CompleteSpace F), ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖
neg : ∀ (hF : ¬CompleteSpace F), ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖
⊢ ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖

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
neg : 0 ≤ max C 0 * ‖Integrable.toL1 f hf‖
⊢ ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
simp only [setToFun, hF, ↓reduceDIte, norm_zero]

Premises used: norm_zero, reduceDIte, 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
⊢ 0 ≤ max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
positivity
-- 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
pos :
  norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) ≤
    max C 0 * ‖Integrable.toL1 f hf‖
⊢ ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
rw [setToFun_eq hT hf]

Premises used: 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 μ
hF : CompleteSpace F
⊢ norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) ≤
    max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
L1.norm_setToL1_le_mul_norm' hT _

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hF : CompleteSpace F
⊢ norm.{u_3} (E := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) ≤
    max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
exact L1.norm_setToL1_le_mul_norm' hT _

Premises used: 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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
pos : ∀ (hF : CompleteSpace F), ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
neg : ∀ (hF : ¬CompleteSpace F), ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
⊢ ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace