-- 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 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
⊢ (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = ∑ j ∈ filter (fun j => g j = g (f a)) f.range, (T (⇑f ⁻¹' {j})) (g j)

Tactic:
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
  congr; rw [map_preimage_singleton]

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))
⊢ (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = ∑ j ∈ filter (fun j => g j = g (f a)) f.range, (T (⇑f ⁻¹' {j})) (g j)

Proof state:
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}

Tactic:
rw [← Finset.set_biUnion_preimage_singleton]

Result:
no goals

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}) ≠ ⊤
⊢ ∑ x ∈ Finset.image g f.range, (T (⇑(map g f) ⁻¹' {x})) x = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

Tactic:
refine Finset.sum_image' _ fun b hb => ?_

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}) ≠ ⊤
b : G
hb : b ∈ f.range
⊢ (T (⇑(map g f) ⁻¹' {g b})) (g b) = ∑ j ∈ filter (fun j => g j = g b) f.range, (T (⇑f ⁻¹' {j})) (g j)

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))
⊢ (∑ 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)

Tactic:
simp only [sum_apply, ContinuousLinearMap.coe_sum']

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))
⊢ ∑ c ∈ filter (fun b => g b = g (f a)) f.range, (T (⇑f ⁻¹' {c})) (g (f a)) =
    ∑ j ∈ filter (fun b => g b = g (f a)) f.range, (T (⇑f ⁻¹' {j})) (g j)

Proof state:
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 : G
_j : i ∈ filter (fun b => g b = g (f a)) f.range
hi : G
a✝ : hi ∈ filter (fun b => g b = g (f a)) f.range
hij : i ≠ hi
⊢ Disjoint (⇑f ⁻¹' {i}) (⇑f ⁻¹' {hi})

Tactic:
rw [Set.disjoint_iff]

Result:
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 : G
_j : i ∈ filter (fun b => g b = g (f a)) f.range
hi : G
a✝ : hi ∈ filter (fun b => g b = g (f a)) f.range
hij : i ≠ hi
⊢ ⇑f ⁻¹' {i} ∩ ⇑f ⁻¹' {hi} ⊆ ∅