-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.Measurable.exists_continuous {α β : Type*} [t : TopologicalSpace α] [PolishSpace α]
    [MeasurableSpace α] [BorelSpace α] [tβ : TopologicalSpace β] [MeasurableSpace β]
    [OpensMeasurableSpace β] {f : α → β} [SecondCountableTopology (range f)] (hf : Measurable f) :
    ∃ t' : TopologicalSpace α, t' ≤ t ∧ @Continuous α β t' tβ f ∧ @PolishSpace α t'

Proof state:
case intro.intro.intro
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)
⊢ ∃ t' ≤ t, Continuous f ∧ PolishSpace α

Tactic:
obtain ⟨t', t'T, t't, t'_polish⟩ :
    ∃ t' : TopologicalSpace α, (∀ i, t' ≤ T i) ∧ t' ≤ t ∧ @PolishSpace α t' :=
  exists_polishSpace_forall_le (t := t) T Tt Tpolish

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ ∃ t' ≤ t, Continuous f ∧ PolishSpace α

Proof state:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
⊢ ∃ t' ≤ t, Continuous f ∧ PolishSpace α

Tactic:
obtain ⟨b, b_count, -, hb⟩ :
    ∃ b : Set (Set (range f)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
  exists_countable_basis (range f)

Result:
case intro.intro.intro
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
⊢ ∃ t' ≤ t, Continuous f ∧ PolishSpace α

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ Continuous f

Tactic:
have : Continuous[t', _] (rangeFactorization f) :=
  hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this✝ : Countable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
this : Continuous (rangeFactorization f)
⊢ Continuous f