-- 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:
α : 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)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (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
⊢ ⇑(map g f) ⁻¹' {g (f a)} = ⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range)

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

Tactic:
simp only [setToSimpleFunc, range_map]

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

Tactic:
simp_rw [h0]

Result:
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)

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
x : α
hx : f x = i ∧ f x = hi
⊢ x ∈ ∅

Tactic:
rw [← hx.1, ← hx.2] at hij

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
x : α
hij : f x ≠ f x
hx : f x = i ∧ f x = hi
⊢ x ∈ ∅

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
⊢ ⇑(map g f) ⁻¹' {g (f a)} = ⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range)

Tactic:
rw [map_preimage_singleton]

Result:
no goals

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))
x : G
hx : x ∈ filter (fun b => g b = g (f a)) f.range
⊢ (T (⇑f ⁻¹' {x})) (g (f a)) = (T (⇑f ⁻¹' {x})) (g x)

Tactic:
rw [mem_filter] at hx

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))
x : G
hx : x ∈ f.range ∧ g x = g (f a)
⊢ (T (⇑f ⁻¹' {x})) (g (f a)) = (T (⇑f ⁻¹' {x})) (g x)