-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrable_map_homeomorph [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → E}
    {μ : Measure X} : LocallyIntegrable f (Measure.map e μ) ↔ LocallyIntegrable (f ∘ e) μ

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn (f ∘ ⇑e.toMeasurableEquiv) (⇑e.toMeasurableEquiv ⁻¹' (⇑e.symm ⁻¹' U)) μ

Tactic:
simp only [Homeomorph.toMeasurableEquiv_coe]

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' (⇑e.symm ⁻¹' U)) μ

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn f (⇑e.symm ⁻¹' U) (map (⇑e) μ)

Tactic:
apply (integrableOn_map_equiv e.toMeasurableEquiv).2

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn (f ∘ ⇑e.toMeasurableEquiv) (⇑e.toMeasurableEquiv ⁻¹' (⇑e.symm ⁻¹' U)) μ

Proof state:
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
⊢ LocallyIntegrable f (map (⇑e) μ) ↔ LocallyIntegrable (f ∘ ⇑e) μ

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩

Result:
case refine_1
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f (map (⇑e) μ)
x : X
⊢ IntegrableAtFilter (f ∘ ⇑e) (𝓝 x) μ

case refine_2
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
⊢ IntegrableAtFilter f (𝓝 x) (map (⇑e) μ)

Proof state:
case refine_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f (map (⇑e) μ)
x : X
U : Set Y
hU : U ∈ 𝓝 (e x)
h'U : IntegrableOn f U (map (⇑e) μ)
⊢ IntegrableAtFilter (f ∘ ⇑e) (𝓝 x) μ

Tactic:
refine ⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩

Result:
case refine_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f (map (⇑e) μ)
x : X
U : Set Y
hU : U ∈ 𝓝 (e x)
h'U : IntegrableOn f U (map (⇑e) μ)
⊢ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' U) μ

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f (map (⇑e) μ)
x : X
⊢ IntegrableAtFilter (f ∘ ⇑e) (𝓝 x) μ

Tactic:
rcases h (e x) with ⟨U, hU, h'U⟩

Result:
case refine_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f (map (⇑e) μ)
x : X
U : Set Y
hU : U ∈ 𝓝 (e x)
h'U : IntegrableOn f U (map (⇑e) μ)
⊢ IntegrableAtFilter (f ∘ ⇑e) (𝓝 x) μ

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' (⇑e.symm ⁻¹' U)) μ

Tactic:
convert h'U

Result:
case h.e'_7
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ ⇑e ⁻¹' (⇑e.symm ⁻¹' U) = U

Proof state:
case h.e'_7
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ ⇑e ⁻¹' (⇑e.symm ⁻¹' U) = U

Tactic:
ext x

Result:
case h.e'_7.h
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x✝ : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x✝)
h'U : IntegrableOn (f ∘ ⇑e) U μ
x : X
⊢ x ∈ ⇑e ⁻¹' (⇑e.symm ⁻¹' U) ↔ x ∈ U

Proof state:
case refine_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f (map (⇑e) μ)
x : X
U : Set Y
hU : U ∈ 𝓝 (e x)
h'U : IntegrableOn f U (map (⇑e) μ)
⊢ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' U) μ

Tactic:
exact (integrableOn_map_equiv e.toMeasurableEquiv).1 h'U

Result:
no goals

Proof state:
case h.e'_7.h
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x✝ : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x✝)
h'U : IntegrableOn (f ∘ ⇑e) U μ
x : X
⊢ x ∈ ⇑e ⁻¹' (⇑e.symm ⁻¹' U) ↔ x ∈ U

Tactic:
simp only [mem_preimage, Homeomorph.symm_apply_apply]

Result:
no goals