-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have neg₁₃ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ) (hx0 : ¬x = 0), Membership.mem (γ := Set F) {x} 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