awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
simp_rw :
  ∑ x ∈ f.range with x ≠ 0, (T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x =
    HAdd.hAdd (α := F) (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
      (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
simp_rw₁ simp_rw₂ :
  ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
    T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) =
      T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
simp_rw₃ : ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}), x ≠ 0
simp_rw₄ : ∀ (x : E) (hx : x ∈ f.range ∧ x ≠ 0), x ≠ 0
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
c : ℝ
f : α →ₛ F
simp_rw :
  ∑ x ∈ f.range, (c • T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x =
    HSMul.hSMul (β := F') c (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
simp_rw₁ :
  ∑ x ∈ f.range, HSMul.hSMul (β := F') c ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') =
    HSMul.hSMul (β := F') c (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
⊢ setToSimpleFunc (fun (s : Set α) ↦ c • T s) f = c • setToSimpleFunc T f

Tactic:
simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]

Premises used: ContinuousLinearMap.smul_apply, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
simp_rw :
  ∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c
      (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f

Tactic:
simp_rw [setToSimpleFunc_eq_sum_filter]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
rw :
  Eq.{u_4 + 1} (α := F')
    (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
    (∑ x ∈ f.range with x ≠ 0,
      HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F'))
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c
      (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)

Tactic:
rw [smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
    (∑ x ∈ f.range with x ≠ 0,
      HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F'))

Tactic:
Finset.sum_congr rfl fun x hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
refine :
  ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
    (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
      HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
    (∑ x ∈ f.range with x ≠ 0,
      HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F'))

Tactic:
refine Finset.sum_congr rfl fun x hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
rw :
  (c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
rw₁ rw₂ :
  HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
⊢ (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')

Tactic:
rw [this x hx, ContinuousLinearMap.smul_apply]

Premises used: ContinuousLinearMap.smul_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
suffices :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c
      (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)

Tactic:
suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
    rw [smul_sum]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx, ContinuousLinearMap.smul_apply]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})

Tactic:
h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_preimage, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
h_smul₁ : x ≠ 0
⊢ T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})

Tactic:
refine
    h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_preimage, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ x ∈ f.range ∧ x ≠ 0

Tactic:
rw [mem_filter] at hx

Premises used: Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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 : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
simp_rw :
  ∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c
      (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
simp_rw₁ simp_rw₂ :
  ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
simp_rw₃ : ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}), x ≠ 0
simp_rw₄ : ∀ (x : E) (hx : x ∈ f.range ∧ x ≠ 0), x ≠ 0
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f

Tactic:
classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
    rw [smul_sum]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx, ContinuousLinearMap.smul_apply]
  intro x hx
  refine
    h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
rw : HAdd.hAdd (α := E) 0.1 0.2 = 0
⊢ setToSimpleFunc T (f + g) =
    ∑ x ∈ (f.pair g).range,
      (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) (x.1 + x.2)

Tactic:
rw [add_eq_map₂, map_setToSimpleFunc T h_add hp_pair]

Premises used: MeasureTheory.SimpleFunc.add_eq_map₂, MeasureTheory.SimpleFunc.map_setToSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ HAdd.hAdd (α := E) 0.1 0.2 = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
rw rw₁ :
  HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
⊢ ∑ x ∈ (f.pair g).range,
      HAdd.hAdd (α := F) (β := F)
        ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1 : F)
        ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2 : F) =
    HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)

Tactic:
rw [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
rw :
  HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    setToSimpleFunc T (map Prod.fst (f.pair g)) +
      ∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2
rw₁ rw₂ :
  HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
⊢ HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    setToSimpleFunc T (map Prod.fst (f.pair g)) + setToSimpleFunc T (map Prod.snd (f.pair g))

Tactic:
rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero,
        map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]

Premises used: Prod.fst_zero, MeasureTheory.SimpleFunc.map_setToSimpleFunc, Prod.snd_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
rw :
  Eq.{u_3 + 1} (α := F) (∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (-x))
    (∑ x ∈ f.range, -(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
⊢ setToSimpleFunc T (map Neg.neg f) = -setToSimpleFunc T f

Tactic:
rw [map_setToSimpleFunc T h_add hf neg_zero, setToSimpleFunc, ← sum_neg_distrib]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum_neg_distrib, neg_zero, MeasureTheory.SimpleFunc.map_setToSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ Eq.{u_3 + 1} (α := F) (∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (-x))
    (∑ x ∈ f.range, -(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)

Tactic:
Finset.sum_congr rfl fun x _ => map_neg _ _

Premises used: map_neg, Set.preimage, Singleton.singleton, DFunLike.coe, Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ Eq.{u_3 + 1} (α := F) (∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (-x))
    (∑ x ∈ f.range, -(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)

Tactic:
exact Finset.sum_congr rfl fun x _ => map_neg _ _

Premises used: map_neg, Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
rw : Integrable.{u_2, u_1} (ε := E) (⇑(-g) : (a : α) → E) μ
⊢ setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g

Tactic:
rw [sub_eq_add_neg, setToSimpleFunc_add T h_add hf, setToSimpleFunc_neg T h_add hg,
    sub_eq_add_neg]

Premises used: sub_eq_add_neg, MeasureTheory.SimpleFunc.setToSimpleFunc_add, MeasureTheory.SimpleFunc.setToSimpleFunc_neg
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
rw :
  ∀
    (hg :
      ∀ (y : E),
        y ≠ 0 →
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑(-g) : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable.{u_2, u_1} (ε := E) (⇑(-g) : (a : α) → E) μ

Tactic:
rw [integrable_iff] at hg ⊢

Premises used: MeasureTheory.SimpleFunc.integrable_iff