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

Tactic:
rw [h_left_eq']

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

Proof state:
case intro
α : 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
⊢ (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:
by_cases h0 : g (f a) = 0

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

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)

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

Tactic:
exact absurd rfl hij

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}) ≠ ⊤
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

Tactic:
rw [mem_filter] at 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 ∈ f.range ∧ g x = 0
⊢ (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
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

Tactic:
have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
  (measure_preimage_lt_top_of_integrable f hf hx0).ne

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