-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : α →ₛ G}
    (hf : Integrable f μ) {g : G → F} (hg : g 0 = 0) :
    (f.map g).setToSimpleFunc T = ∑ x ∈ f.range, T (f ⁻¹' {x}) (g x)

Proof state:
case pos
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
⊢ (T (⇑(map g f) ⁻¹' {0})) 0 = ∑ x ∈ filter (fun j => g j = 0) f.range, (T (⇑f ⁻¹' {x})) (g x)

Tactic:
rw [ContinuousLinearMap.map_zero, Finset.sum_eq_zero fun x hx => ?_]

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ filter (fun j => g j = 0) f.range
⊢ (T (⇑f ⁻¹' {x})) (g x) = 0

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
⊢ (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))

Tactic:
congr

Result:
case e_a.e_a
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
⊢ ⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range) = ⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y}

Proof state:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
⊢ (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a)) =
    ∑ j ∈ filter (fun j => g j = g (f a)) f.range, (T (⇑f ⁻¹' {j})) (g j)

Tactic:
rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]

Result:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
⊢ (∑ i ∈ filter (fun b => g b = g (f a)) f.range, T (⇑f ⁻¹' {i})) (g (f a)) =
    ∑ j ∈ filter (fun j => g j = g (f a)) f.range, (T (⇑f ⁻¹' {j})) (g j)

case neg.hS_meas
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ (i : G), MeasurableSet (⇑f ⁻¹' {i})

case neg.hSp
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ i ∈ filter (fun b => g b = g (f a)) f.range, μ (⇑f ⁻¹' {i}) ≠ ⊤

case neg.h_disj
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ i ∈ filter (fun b => g b = g (f a)) f.range,
    ∀ j ∈ filter (fun b => g b = g (f a)) f.range, i ≠ j → Disjoint (⇑f ⁻¹' {i}) (⇑f ⁻¹' {j})