-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
/-- Preimage of an analytic set is an analytic set. -/
protected lemma AnalyticSet.preimage {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [PolishSpace X] [T2Space Y] {s : Set Y} (hs : AnalyticSet s) {f : X → Y} (hf : Continuous f) :
    AnalyticSet (f ⁻¹' s)

Proof state:
case h.e'_3.h
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
this : IsClosed {x | f x.1 = g x.2}
x : X
⊢ x ∈ f ⁻¹' range g ↔ x ∈ Prod.fst '' {x | f x.1 = g x.2}

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
⊢ AnalyticSet (f ⁻¹' range g)

Tactic:
have : IsClosed {x : X × Z | f x.1 = g x.2} := isClosed_eq hf.fst' hg.snd'

Result:
case intro.intro.intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
this : IsClosed {x | f x.1 = g x.2}
⊢ AnalyticSet (f ⁻¹' range g)

Proof state:
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
s : Set Y
hs : AnalyticSet s
f : X → Y
hf : Continuous f
⊢ AnalyticSet (f ⁻¹' s)

Tactic:
rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨Z, _, _, g, hg, rfl⟩

Result:
case intro.intro.intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
⊢ AnalyticSet (f ⁻¹' range g)

Proof state:
case intro.intro.intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
this : IsClosed {x | f x.1 = g x.2}
⊢ AnalyticSet (f ⁻¹' range g)

Tactic:
convert this.analyticSet.image_of_continuous continuous_fst

Result:
case h.e'_3
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
this : IsClosed {x | f x.1 = g x.2}
⊢ f ⁻¹' range g = Prod.fst '' {x | f x.1 = g x.2}

Proof state:
case h.e'_3
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
this : IsClosed {x | f x.1 = g x.2}
⊢ f ⁻¹' range g = Prod.fst '' {x | f x.1 = g x.2}

Tactic:
ext x

Result:
case h.e'_3.h
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous g
hs : AnalyticSet (range g)
this : IsClosed {x | f x.1 = g x.2}
x : X
⊢ x ∈ f ⁻¹' range g ↔ x ∈ Prod.fst '' {x | f x.1 = g x.2}