-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_map_of_stronglyMeasurable {β} [MeasurableSpace β] {φ : α → β} (hφ : Measurable φ)
    {f : β → G} (hfm : StronglyMeasurable f) : ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Tactic:
rw [integral_undef hfi, integral_undef]

Result:
case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ¬Integrable (fun x => f (φ x)) μ

Proof state:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : ¬CompleteSpace G
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Tactic:
swap

Result:
case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ¬Integrable (fun x => f (φ x)) μ

Tactic:
exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)

Result:
no goals

Proof state:
case h.e'_3.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
y : G
x✝ : y ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range
hy : ⇑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y} = ∅
⊢ (μ (⇑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y})).toReal • y = 0

Tactic:
rw [hy]

Result:
case h.e'_3.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
y : G
x✝ : y ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range
hy : ⇑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y} = ∅
⊢ (μ ∅).toReal • y = 0

Proof state:
case h.e'_3
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
⊢ (fun n => SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n)) = fun n =>
    SimpleFunc.integral μ (approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ n)

Tactic:
ext1 i

Result:
case h.e'_3.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) =
    SimpleFunc.integral μ (approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)

Proof state:
case h.e'_3.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
y : G
x✝ : y ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range
hy : y ∉ ((approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ).range
⊢ (μ (⇑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y})).toReal • y = 0

Tactic:
rw [SimpleFunc.mem_range, ← Set.preimage_singleton_eq_empty, SimpleFunc.coe_comp] at hy

Result:
case h.e'_3.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
y : G
x✝ : y ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range
hy : ⇑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y} = ∅
⊢ (μ (⇑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y})).toReal • y = 0