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'' : ℝ
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
pos : ∀ (hF : CompleteSpace F), setToFun μ T'' hT'' 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 = 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' 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
hF : ¬CompleteSpace F
⊢ setToFun μ T'' hT'' 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' 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
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T'' hT'' 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 = 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' 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
hF : CompleteSpace F
hf : Integrable f μ
pos :
  (L1.setToL1 hT'' : (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'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

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

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' 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
hF : CompleteSpace F
hf : ¬Integrable f μ
neg : 0 = HAdd.hAdd (α := F) 0 0
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf, add_zero]

Premises used: MeasureTheory.setToFun_undef, add_zero
-- 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
c : ℝ
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • 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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : ¬CompleteSpace F
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • 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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
neg : ∀ (hf : ¬Integrable f μ), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • 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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  (L1.setToL1 (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) ⋯ : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left hT c]

Premises used: MeasureTheory.L1.setToL1_smul_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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
neg : 0 = HSMul.hSMul (β := F) c 0
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_undef _ hf, smul_zero]

Premises used: MeasureTheory.setToFun_undef, smul_zero
-- 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'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T' hT' f = c • setToFun μ T hT f
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T' hT' f = c • setToFun μ T hT f
⊢ setToFun μ T' hT' f = c • 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'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : ¬CompleteSpace F
⊢ setToFun μ T' hT' f = c • 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'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T' hT' f = c • setToFun μ T hT f
neg : ∀ (hf : ¬Integrable f μ), setToFun μ T' hT' f = c • setToFun μ T hT f
⊢ setToFun μ T' hT' f = c • 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'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  (L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_smul]

Premises used: MeasureTheory.L1.setToL1_smul_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'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
neg : 0 = HSMul.hSMul (β := F) c 0
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_undef _ hf, smul_zero]

Premises used: MeasureTheory.setToFun_undef, smul_zero
-- 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
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT 0 = 0
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT 0 = 0
⊢ setToFun μ T hT 0 = 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : ¬CompleteSpace F
⊢ setToFun μ T hT 0 = 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fun (x : α) ↦ 0) ⋯) : F) (0 : F)
⊢ setToFun μ T hT 0 = 0

Tactic:
rw [Pi.zero_def, setToFun_eq hT (integrable_zero _ _ _)]

Premises used: MeasureTheory.integrable_zero, Pi.zero_def, 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 0 ⋯) : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fun (x : α) ↦ 0) ⋯) : F) (0 : F)

Tactic:
simp only [← Pi.zero_def]

Premises used: Pi.zero_def
-- 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
hF : CompleteSpace F
pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) 0 : F) (0 : F)
pos₁ pos₂ : Eq.{u_3 + 1} (α := F) 0 0
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 0 ⋯) : F) (0 : F)

Tactic:
rw [Integrable.toL1_zero, map_zero]

Premises used: MeasureTheory.Integrable.toL1_zero, map_zero
-- 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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
pos : ∀ (hF : CompleteSpace F), setToFun μ 0 hT f = 0
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ 0 hT f = 0
⊢ setToFun μ 0 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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : ¬CompleteSpace F
⊢ setToFun μ 0 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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ 0 hT f = 0
neg : ∀ (hf : ¬Integrable f μ), setToFun μ 0 hT f = 0
⊢ setToFun μ 0 hT f = 0

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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
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) (0 : F)
⊢ setToFun μ 0 hT f = 0

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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (0 : F)

Tactic:
L1.setToL1_zero_left hT _

Premises used: MeasureTheory.L1.setToL1_zero_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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (0 : F)

Tactic:
exact L1.setToL1_zero_left hT _

Premises used: MeasureTheory.L1.setToL1_zero_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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ 0 hT f = 0

Tactic:
setToFun_undef hT 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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ 0 hT f = 0

Tactic:
exact setToFun_undef hT 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 : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
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
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
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
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T hT f = 0
neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f = 0
⊢ setToFun μ T hT f = 0

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 : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
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) (0 : F)
⊢ setToFun μ T hT f = 0

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
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (0 : F)

Tactic:
L1.setToL1_zero_left' hT h_zero _

Premises used: MeasureTheory.L1.setToL1_zero_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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (0 : F)

Tactic:
exact L1.setToL1_zero_left' hT h_zero _

Premises used: MeasureTheory.L1.setToL1_zero_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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = 0

Tactic:
setToFun_undef hT 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 : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = 0

Tactic:
exact setToFun_undef hT 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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

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 g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : ¬CompleteSpace F
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

Tactic:
simp [setToFun, hF]

Premises used: MeasureTheory.setToFun