-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem map_of_continuous [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β]
    [BorelSpace β] [h : InnerRegularCompactLTTop μ] {f : α → β} (hf : Continuous f) :
    InnerRegularCompactLTTop (Measure.map f μ)

Proof state:
case innerRegular.refine_1.intro
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
s : Set β
hs : MeasurableSet s
h's : (map f μ) s ≠ ⊤
⊢ MeasurableSet (f ⁻¹' s) ∧ μ (f ⁻¹' s) ≠ ⊤

Tactic:
exact ⟨hf.measurable hs, by rwa [map_apply hf.measurable hs] at h's⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
s : Set β
hs : MeasurableSet s
h's : (map f μ) s ≠ ⊤
⊢ μ (f ⁻¹' s) ≠ ⊤

Tactic:
rwa [map_apply hf.measurable hs] at h's

Result:
no goals

Proof state:
case innerRegular.refine_2.intro
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact hs

Result:
no goals

Proof state:
case innerRegular
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ (map f μ).InnerRegularWRT IsCompact fun s => MeasurableSet s ∧ (map f μ) s ≠ ⊤

Tactic:
refine InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_

Result:
case innerRegular.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ ∀ (U : Set β), MeasurableSet U ∧ (map f μ) U ≠ ⊤ → MeasurableSet (f ⁻¹' U) ∧ μ (f ⁻¹' U) ≠ ⊤

case innerRegular.refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ ∀ (U : Set β), MeasurableSet U ∧ (map f μ) U ≠ ⊤ → MeasurableSet U

Proof state:
case innerRegular.refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ ∀ (U : Set β), MeasurableSet U ∧ (map f μ) U ≠ ⊤ → MeasurableSet U

Tactic:
rintro s ⟨hs, -⟩

Result:
case innerRegular.refine_2.intro
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ (map f μ).InnerRegularCompactLTTop

Tactic:
constructor

Result:
case innerRegular
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ (map f μ).InnerRegularWRT IsCompact fun s => MeasurableSet s ∧ (map f μ) s ≠ ⊤

Proof state:
case innerRegular.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
⊢ ∀ (U : Set β), MeasurableSet U ∧ (map f μ) U ≠ ⊤ → MeasurableSet (f ⁻¹' U) ∧ μ (f ⁻¹' U) ≠ ⊤

Tactic:
rintro s ⟨hs, h's⟩

Result:
case innerRegular.refine_1.intro
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous f
s : Set β
hs : MeasurableSet s
h's : (map f μ) s ≠ ⊤
⊢ MeasurableSet (f ⁻¹' s) ∧ μ (f ⁻¹' s) ≠ ⊤