-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable.{u_5, u_1} (ε := G) (⇑f : (a : α) → G) μ
g : G → F
hg : g 0 = 0
have have₁ have₂ :
  ∀ (T_empty : T ∅ = 0),
    setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have₃ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have₄ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_4 + 1} (α := F')
      (∑ x ∈ Finset.image g f.range, (T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x))
have₅ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (b : G) (hb : b ∈ f.range),
    Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g b}) : (a : F) → F') (g b) : F')
      (∑ j ∈ f.range with g j = g b, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) : F')
have₆ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)),
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
          (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
        F')
pos :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)) (h0 : g ((f : (a : α) → G) a) = 0),
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
          (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
        F')
neg neg₁ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)) (h0 : ¬g ((f : (a : α) → G) a) = 0),
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
          (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
        F')
neg₂ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)) (h0 : ¬g ((f : (a : α) → G) a) = 0)
    (h_left_eq :
      Eq.{u_4 + 1} (α := F')
        ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')
        ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')),
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
          (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
        F')
neg₃ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)) (h0 : ¬g ((f : (a : α) → G) a) = 0)
    (h_left_eq :
      Eq.{u_4 + 1} (α := F')
        ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')
        ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')),
    Eq.{u_4 + 1} (α := F')
      ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
          (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
        F')
neg₄ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)) (h0 : ¬g ((f : (a : α) → G) a) = 0)
    (h_left_eq :
      Eq.{u_4 + 1} (α := F')
        ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')
        ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F'))
    (h_left_eq' :
      Eq.{u_4 + 1} (α := F')
        ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')
        ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
              (a : F) → F')
            (g ((f : (a : α) → G) a)) :
          F')),
    Eq.{u_4 + 1} (α := F')
      ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
          (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
        F')
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have neg₅ : ∀ (T_empty : T ∅ = 0)
  (hfp :
    ∀ x ∈ f.range,
      x ≠ 0 →
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)) (h0 : ¬g ((f : (a : α) → G) a) = 0)
  (h_left_eq :
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F'))
  (h_left_eq' :
    Eq.{u_4 + 1} (α := F')
      ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')
      ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
            (a : F) → F')
          (g ((f : (a : α) → G) a)) :
        F')),
  Eq.{u_4 + 1} (α := F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
        (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
      F')
Tactic: classical
  have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
  have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne
  simp only [setToSimpleFunc, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  by_cases h0 : g (f a) = 0
  · simp_rw [h0]
    rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]
    rw [mem_filter] at hx
    rw [hx.2, map_zero]
  have h_left_eq :
    T (map g f ⁻¹' {g (f a)}) (g (f a))
      = T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) := by
    rw [map_preimage_singleton]
  rw [h_left_eq]
  have h_left_eq' :
    T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a))
      = T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, f ⁻¹' {y}) (g (f a)) := by
    rw [← Finset.set_biUnion_preimage_singleton]
  rw [h_left_eq']
  rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
  · simp only [sum_apply, ContinuousLinearMap.coe_sum']
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [mem_filter] at hx
    rw [hx.2]
  · exact fun i => measurableSet_fiber _ _
  · grind
  · grind [Set.disjoint_iff]