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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
pos : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (f + g) ⋯) = setToFun μ T hT f + setToFun μ T hT g
pos₁ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (f + g) ⋯) =
    HAdd.hAdd (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (setToFun μ T hT g)
pos₂ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (f + g) ⋯) =
    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 g hg) : F)
pos₃ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf + Integrable.toL1 g hg) =
    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 g hg) : F)
pos₄ : Integrable f μ
pos₅ : Integrable g μ
pos₆ :
  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 g hg) : F) =
    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 g hg) : F)
pos₇ : Integrable f μ
pos₈ : Integrable g μ
pos₉ :
  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 g hg) : F) =
    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 g hg) : F)
pos₁₀ : Integrable f μ
pos₁₁ : Integrable g μ
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

Tactic:
rw [setToFun_eq hT (hf.add hg), setToFun_eq hT hf, setToFun_eq hT hg, Integrable.toL1_add,
    (L1.setToL1 hT).map_add]

Premises used: ContinuousLinearMap.map_add, MeasureTheory.Integrable.add, MeasureTheory.L1.setToL1, MeasureTheory.Integrable.toL1_add, 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
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
revert : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
⊢ setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
revert 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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
⊢ ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- 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
ι : Type u_7
s : Finset ι
f : ι → α → E
refine_1 :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) μ),
    setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)) →
        ∀ (hf : ∀ i ∈ insert a s, Integrable (f i) μ),
          setToFun μ T hT (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, setToFun μ T hT (f i)
⊢ ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
refine Finset.induction_on s ?_ ?_
-- 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
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) μ
⊢ setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)

Tactic:
simp only [setToFun_zero, Finset.sum_empty]

Premises used: MeasureTheory.setToFun_zero, Finset.sum_empty
-- 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
ι : Type u_7
s_1 : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
refine_2 : setToFun μ T hT (f i + ∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)
⊢ setToFun μ T hT (∑ i ∈ insert i s, f i) = ∑ i ∈ insert i s, setToFun μ T hT (f i)

Tactic:
simp only [his, Finset.sum_insert, not_false_iff]

Premises used: Finset.sum_insert, not_false_iff
-- 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
ι : Type u_7
s_1 : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
refine_2 :
  setToFun μ T hT (f i) + setToFun μ T hT (∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)
rw : Integrable.{u_2, u_1} (ε := E) (∑ i ∈ s, f i) μ
⊢ setToFun μ T hT (f i + ∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
rw [setToFun_add hT (hf i (Finset.mem_insert_self i s)) _]

Premises used: Finset.mem_insert_self, MeasureTheory.setToFun_add
-- 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
ι : Type u_7
s_1 : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
refine_2 refine_2₁ :
  setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)
⊢ setToFun μ T hT (f i) + setToFun μ T hT (∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
rw [ih fun i hi => hf i (Finset.mem_insert_of_mem hi)]

Premises used: Finset.mem_insert_of_mem
-- 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
ι : Type u_7
s_1 : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) μ

Tactic:
integrable_finsetSum s fun i hi => hf i (Finset.mem_insert_of_mem hi)

Premises used: MeasureTheory.integrable_finsetSum, Finset.mem_insert_of_mem
-- 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
ι : Type u_7
s_1 : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
h : ∀ (x : α), Eq.{u_2 + 1} (α := E) ((∑ i ∈ s, f i) x) (∑ i ∈ s, f i x)
⊢ Integrable.{u_2, u_1} (ε := E) (∑ i ∈ s, f i) μ

Tactic:
convert! integrable_finsetSum s fun i hi => hf i (Finset.mem_insert_of_mem hi) with x

Premises used: MeasureTheory.integrable_finsetSum, Finset.mem_insert_of_mem
-- 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
ι : Type u_7
s_1 : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
x : α
⊢ Eq.{u_2 + 1} (α := E) ((∑ i ∈ s, f i) x) (∑ i ∈ s, f i x)

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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
revert : ∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
refine_1 :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) μ),
    setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)
refine_2 refine_2₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (hf : ∀ i ∈ s, Integrable (f i) μ), setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)) →
        ∀ (hf : ∀ i ∈ insert a s, Integrable (f i) μ),
          setToFun μ T hT (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, setToFun μ T hT (f i)
⊢ setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
classical
  revert hf
  refine Finset.induction_on s ?_ ?_
  · intro _
    simp only [setToFun_zero, Finset.sum_empty]
  · intro i s his ih hf
    simp only [his, Finset.sum_insert, not_false_iff]
    rw [setToFun_add hT (hf i (Finset.mem_insert_self i s)) _]
    · rw [ih fun i hi => hf i (Finset.mem_insert_of_mem hi)]
    · convert! integrable_finsetSum s fun i hi => hf i (Finset.mem_insert_of_mem hi) with x
      simp

Premises used: MeasureTheory.setToFun_zero, Finset.sum_empty, Finset.sum_insert, not_false_iff
-- 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
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
setToFun_finsetSum' hT s hf

Premises used: MeasureTheory.setToFun_finsetSum'
-- 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
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
h : ∀ (a : α), Eq.{u_2 + 1} (α := E) (∑ i ∈ s, f i a) ((∑ i ∈ s, f i) a)
⊢ (setToFun μ T hT fun (a : α) ↦ ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
convert! setToFun_finsetSum' hT s hf with a

Premises used: MeasureTheory.setToFun_finsetSum'
-- 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
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
a : α
⊢ Eq.{u_2 + 1} (α := E) (∑ i ∈ s, f i a) ((∑ i ∈ s, f i) a)

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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos : setToFun μ T hT (-f) = -(L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf)
pos₁ :
  Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (-f) ⋯) : F)
    (-(L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : 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)
pos₃ : 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)
pos₅ : 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)
pos₇ : Integrable f μ
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

Tactic:
rw [setToFun_eq hT hf, setToFun_eq hT hf.neg, Integrable.toL1_neg,
      (L1.setToL1 hT).map_neg]

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.L1.setToL1, ContinuousLinearMap.map_neg, MeasureTheory.Integrable.toL1_neg, 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
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
neg : ¬Integrable (-f) μ
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

Tactic:
rw [setToFun_undef hT hf, setToFun_undef hT, neg_zero]

Premises used: MeasureTheory.setToFun_undef, neg_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
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
neg neg₁ neg₂ neg₃ : ∀ (hf : ¬Integrable (-f) μ), ¬Integrable (-f) μ
⊢ ¬Integrable (-f) μ

Tactic:
rwa [← integrable_neg_iff] at hf

Premises used: MeasureTheory.integrable_neg_iff
-- 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 : α → E
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → (-T) s = HSMul.hSMul (α := ℝ) (-1) (T s)

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

Tactic:
simpa using setToFun_smul_left' hT hT.neg (-1) (by simp) f

Premises used: MeasureTheory.DominatedFinMeasAdditive.neg, MeasureTheory.setToFun_smul_left', OfNat.ofNat, Neg.neg
-- 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 μ
rw : setToFun μ T hT (f + -g) = setToFun μ T hT f - setToFun μ T hT g
rw₁ : setToFun μ T hT (f + -g) = setToFun μ T hT f + -setToFun μ T hT g
rw₂ : setToFun μ T hT f + setToFun μ T hT (-g) = setToFun μ T hT f + -setToFun μ T hT g
rw₃ rw₄ : setToFun μ T hT f + -setToFun μ T hT g = setToFun μ T hT f + -setToFun μ T hT g
⊢ setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, setToFun_add hT hf hg.neg, setToFun_neg hT g]

Premises used: MeasureTheory.Integrable.neg, sub_eq_add_neg, MeasureTheory.setToFun_add, MeasureTheory.setToFun_neg
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
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 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT (c • f) = c • setToFun μ T hT f
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT (c • f) = c • setToFun μ T hT f
⊢ setToFun μ T hT (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
𝕜 : Type u_6
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 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T hT (c • f) = c • setToFun μ T hT f
neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT (c • f) = c • setToFun μ T hT f
⊢ setToFun μ T hT (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
𝕜 : Type u_6
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 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
pos₁ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (c • f) ⋯) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
pos₂ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (c • Integrable.toL1 f hf) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
pos₃ pos₄ :
  HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.toL1_smul', MeasureTheory.L1.setToL1_smul, MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
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 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
pos : ∀ (hr : c = 0), setToFun μ T hT (c • f) = c • setToFun μ T hT f
neg : ∀ (hr : ¬c = 0), setToFun μ T hT (c • f) = c • setToFun μ T hT f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
by_cases hr : c = 0
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
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 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : c = 0
pos : setToFun μ T hT (HSMul.hSMul (α := 𝕜) 0 f) = HSMul.hSMul.{u_6, u_3, u_3} (α := 𝕜) 0 (setToFun μ T hT f)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
rw [hr]