case refine'_1
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f
x : X
⊢ IntegrableAtFilter (f ∘ ↑e) (𝓝 x)

case refine'_2
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ↑e)
x : Y
⊢ IntegrableAtFilter f (𝓝 x)
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
⊢ LocallyIntegrable f ↔ LocallyIntegrable (f ∘ ↑e)
refine' ⟨fun h x => _, fun h x => _⟩
case refine'_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f
x : X
U : Set Y
hU : U ∈ 𝓝 (↑e x)
h'U : IntegrableOn f U
⊢ IntegrableAtFilter (f ∘ ↑e) (𝓝 x)
case refine'_1
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f
x : X
⊢ IntegrableAtFilter (f ∘ ↑e) (𝓝 x)
rcases h (e x) with ⟨U, hU, h'U⟩
case refine'_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f
x : X
U : Set Y
hU : U ∈ 𝓝 (↑e x)
h'U : IntegrableOn f U
⊢ IntegrableOn (f ∘ ↑e) (↑e ⁻¹' U)
case refine'_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f
x : X
U : Set Y
hU : U ∈ 𝓝 (↑e x)
h'U : IntegrableOn f U
⊢ IntegrableAtFilter (f ∘ ↑e) (𝓝 x)
refine' ⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, _⟩
no goals
case refine'_1.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable f
x : X
U : Set Y
hU : U ∈ 𝓝 (↑e x)
h'U : IntegrableOn f U
⊢ IntegrableOn (f ∘ ↑e) (↑e ⁻¹' U)
exact (integrableOn_map_equiv e.toMeasurableEquiv).1 h'U
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableAtFilter f (𝓝 x)
case refine'_2
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ↑e)
x : Y
⊢ IntegrableAtFilter f (𝓝 x)
rcases h (e.symm x) with ⟨U, hU, h'U⟩
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableOn f (↑(Homeomorph.symm e) ⁻¹' U)
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableAtFilter f (𝓝 x)
refine' ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, _⟩
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableOn (f ∘ ↑(Homeomorph.toMeasurableEquiv e))
    (↑(Homeomorph.toMeasurableEquiv e) ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U))
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableOn f (↑(Homeomorph.symm e) ⁻¹' U)
apply (integrableOn_map_equiv e.toMeasurableEquiv).2
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableOn (f ∘ ↑e) (↑e ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U))
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableOn (f ∘ ↑(Homeomorph.toMeasurableEquiv e))
    (↑(Homeomorph.toMeasurableEquiv e) ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U))
simp only [Homeomorph.toMeasurableEquiv_coe]
case h.e'_6
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ ↑e ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U) = U
case refine'_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ IntegrableOn (f ∘ ↑e) (↑e ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U))
convert h'U
case h.e'_6.h
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x✝)
h'U : IntegrableOn (f ∘ ↑e) U
x : X
⊢ x ∈ ↑e ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U) ↔ x ∈ U
case h.e'_6
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x)
h'U : IntegrableOn (f ∘ ↑e) U
⊢ ↑e ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U) = U
ext x
no goals
case h.e'_6.h
X : Type u_1
Y : Type u_2
E : Type u_3
R : Type ?u.130650
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
f✝ : X → E
μ✝ : Measure X
s : Set X
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 ∈ 𝓝 (↑(Homeomorph.symm e) x✝)
h'U : IntegrableOn (f ∘ ↑e) U
x : X
⊢ x ∈ ↑e ⁻¹' (↑(Homeomorph.symm e) ⁻¹' U) ↔ x ∈ U
simp only [mem_preimage, Homeomorph.symm_apply_apply]