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 : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
x y : E
hxy : x ≠ y
refine :
  ∀ (z : α),
    Membership.mem (γ := Set α)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) z →
      Membership.mem (γ := Set α) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} z
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null (fun z => ?_) h

Premises used: MeasureTheory.measure_mono_null
-- 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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h_1 :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
x y : E
hxy : x ≠ y
z : α
h : (f : (a : α) → E) z = x ∧ (g : (a : α) → E) z = y
rwa : ¬x = (g : (a : α) → E) z
rwa₁ rwa₂ rwa₃ rwa₄ : ¬x = y
⊢ ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) z : E) ((g : (a : α) → E) z : E)

Tactic:
rwa [h.1, h.2]

Premises used: And.right, And.left
-- 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' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
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:
sum_congr rfl fun x _ => ?_

Premises used: 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 T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
refine :
  ∀ x ∈ f.range,
    Eq.{u_3 + 1} (α := F) ((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 : F)
⊢ 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:
refine sum_congr rfl fun x _ => ?_

Premises used: 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 T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h_1 : x ∈ f.range
pos :
  ∀ (hx0 : x = 0),
    Eq.{u_3 + 1} (α := F) ((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 : F)
neg :
  ∀ (hx0 : ¬x = 0),
    Eq.{u_3 + 1} (α := F) ((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 : F)
⊢ Eq.{u_3 + 1} (α := F) ((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 : F)

Tactic:
by_cases hx0 : x = 0
-- 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' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h_1 : x ∈ f.range
hx0 : x = 0
⊢ Eq.{u_3 + 1} (α := F) ((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 : F)

Tactic:
simp [hx0]
-- 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' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h_1 : x ∈ f.range
hx0 : ¬x = 0
neg neg₁ :
  Eq.{u_3 + 1} (α := F) ((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 : F)
⊢ Eq.{u_3 + 1} (α := F) ((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 : F)

Tactic:
rw [h (f ⁻¹' {x}) (SimpleFunc.measurableSet_fiber _ _)
        (SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hx0)]

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_fiber, Singleton.singleton, DFunLike.coe
-- 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 T' : Set α → F →L[ℝ] F'
f : α →ₛ F
simp_rw :
  ∑ x ∈ f.range,
      (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) + T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) :
          (a : F) → F')
        x =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
⊢ setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc, Pi.add_apply]

Premises used: Pi.add_apply, MeasureTheory.SimpleFunc.setToSimpleFunc
-- 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 T' : Set α → F →L[ℝ] F'
f : α →ₛ F
push_cast :
  ∑ x ∈ f.range,
      HAdd.hAdd (α := (a : F) → F') (β := (a : F) → F')
        (⇑(T (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F')
        (⇑(T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F') x =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
⊢ ∑ x ∈ f.range,
      (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) + T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) :
          (a : F) → F')
        x =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)

Tactic:
push_cast
-- 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 T' : Set α → F →L[ℝ] F'
f : α →ₛ F
simp_rw :
  ∑ x ∈ f.range,
      HAdd.hAdd (α := F') (β := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F')
        ((T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
⊢ ∑ x ∈ f.range,
      HAdd.hAdd (α := (a : F) → F') (β := (a : F) → F')
        (⇑(T (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F')
        (⇑(T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F') x =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)

Tactic:
simp_rw [Pi.add_apply, sum_add_distrib]

Premises used: Finset.sum_add_distrib, Pi.add_apply
-- 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)
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + 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_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) μ
this :
  ∀ 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})
rw :
  Eq.{u_3 + 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,
      HAdd.hAdd (α := F) (β := F) ((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 : F))
⊢ ∑ 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)

Tactic:
rw [← 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 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) μ
this :
  ∀ 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})
⊢ Eq.{u_3 + 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,
      HAdd.hAdd (α := F) (β := F) ((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 : 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_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) μ
this :
  ∀ 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})
refine :
  ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
    (T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x =
      HAdd.hAdd (α := F) (β := F) ((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 : F)
⊢ Eq.{u_3 + 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,
      HAdd.hAdd (α := F) (β := F) ((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 : 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_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) μ
this :
  ∀ 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})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
rw :
  (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F)
      x =
    HAdd.hAdd (α := F) (β := F) ((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 : F)
⊢ (T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x =
    HAdd.hAdd (α := F) (β := F) ((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 : F)

Tactic:
rw [this x hx]
-- 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) μ
this :
  ∀ 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})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
push_cast :
  HAdd.hAdd (α := (a : E) → F) (β := (a : E) → F) (⇑(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})) : (a : E) → F)
      (⇑(T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})) : (a : E) → F) x =
    HAdd.hAdd (α := F) (β := F) ((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 : F)
⊢ (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F)
      x =
    HAdd.hAdd (α := F) (β := F) ((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 : F)

Tactic:
push_cast
-- 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) μ
this :
  ∀ 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})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
rw rw₁ :
  HAdd.hAdd (α := F) (β := F) ((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 : F) =
    HAdd.hAdd (α := F) (β := F) ((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 : F)
⊢ HAdd.hAdd (α := (a : E) → F) (β := (a : E) → F) (⇑(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})) : (a : E) → F)
      (⇑(T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})) : (a : E) → F) x =
    HAdd.hAdd (α := F) (β := F) ((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 : F)

Tactic:
rw [Pi.add_apply]

Premises used: Pi.add_apply
-- 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) μ
suffices :
  ∀ 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})
⊢ ∑ 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)

Tactic:
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]
-- 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) μ
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})

Tactic:
h_add (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_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) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
h_add₁ : 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})

Tactic:
refine
    h_add (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_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) μ
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_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) μ
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_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) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Tactic:
exact hx.2

Premises used: And.right