-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
inr inr₁ :
  ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
inr₂ :
  ∀ (hs_empty : s.Nonempty),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
inr₃ :
  ∀ (hs : MeasurableSet.{u_1} (α := α) Set.univ) (hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
              (a : F) → F')
            x_1 :
        F')
      ((T Set.univ : (a : F) → F') x : F')
inr₄ inr₅ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
inr₆ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ {x, 0},
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
pos :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : x = 0),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ {x, 0},
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
neg neg₁ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ {x, 0},
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
neg₂ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0),
    HAdd.hAdd (α := F') (β := F')
        ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x :
          F')
        (∑ x_1 ∈ {0},
            (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
              x_1 :
          F') =
      (T s : (a : F) → F') x
neg₃ neg₄ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), x ∉ {0}
neg₅ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0),
    HAdd.hAdd (α := F') (β := F')
        ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x :
          F')
        (∑ x_1 ∈ {0},
            (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
              x_1 :
          F') =
      (T s : (a : F) → F') x
neg₆ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), x ∉ {0}
neg₇ neg₈ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0),
    HAdd.hAdd (α := F') (β := F')
        ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x :
          F')
        (∑ x_1 ∈ {0},
            (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
              x_1 :
          F') =
      (T s : (a : F) → F') x
neg₉ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0),
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x : F')
      ((T s : (a : F) → F') x : F')
neg₁₀ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0),
    Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x} = s
neg₁₁ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.indicator (Function.const α x) ⁻¹' {x} = s
neg₁₂ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
neg₁₃ neg₁₄ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), Membership.mem (γ := Set F) {x} x
neg₁₅ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
neg₁₆ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), Membership.mem (γ := Set F) {x} x
neg₁₇ neg₁₈ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
neg₁₉ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.ite Set.univ ∅ = s
neg₂₀ neg₂₁ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), 0 ∉ {x}
neg₂₂ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.ite Set.univ ∅ = s
neg₂₃ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), 0 ∉ {x}
neg₂₄ neg₂₅ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), s.ite Set.univ ∅ = s
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x

Tactic:
classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp

Premises used: Set.mem_singleton, Finset.mem_singleton, ContinuousLinearMap.map_zero, MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply, Set.preimage_const_of_notMem, Set.univ, MeasureTheory.SimpleFunc.coe_piecewise, Finset.sum_singleton, Set.eq_empty_or_nonempty, Set.mem_singleton_iff, Function.const_def, MeasureTheory.SimpleFunc.piecewise_empty, Set.indicator_preimage, MeasureTheory.SimpleFunc.setToSimpleFunc, Function.const_zero, eq_or_ne, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, Finset.sum_insert, add_zero, Set.preimage_const_of_mem, MeasureTheory.SimpleFunc.coe_const, rfl, ContinuousLinearMap.zero_apply