awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this_1 : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
x : (↑t : Type u_2)
n : ι
this : f n ((↑x : γ) n) = F x
⊢ F x ∈ s n
have h₁ : f n ((↑x : γ) n) ∈ range (f n)
Tactic: rw [← this, ← f_range n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
n : ι
⊢ ∃ (x : β n), f n x = y
have rw : y ∈ s n
Tactic: rw [← mem_range, f_range n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
⊢ y ∈ range F
have A : ∀ (n : ι), ∃ (x : β n), f n x = y
Tactic: have A : ∀ n, ∃ x : β n, f n x = y := by
        intro n
        rw [← mem_range, f_range n]
        exact mem_iInter.1 hy n
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
A : ∀ (n : ι), ∃ (x : β n), f n x = y
⊢ y ∈ range F
have h₂ : ∀ (x : (n : ι) → β n) (hx : ∀ (n : ι), f n (x n) = y), y ∈ range F
Tactic: choose x hx using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ x ∈ t
have refine : ∀ (n : ι), Membership.mem (γ := Set ((n : ι) → β n)) {x : γ | f n (x n) = f i₀ (x i₀)} x
Tactic: refine mem_iInter.2 fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ y ∈ range F
have xt : x ∈ t
Tactic: have xt : x ∈ t := by
        refine mem_iInter.2 fun n => ?_
        simp [γ, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
⊢ y ∈ range F
have h₂ : F (Subtype.mk (p := fun (x : γ) ↦ x ∈ t) x xt) = y
Tactic: refine ⟨⟨x, xt⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
have F_range : range F = ⋂ (n : ι), s n
Tactic: have F_range : range F = ⋂ n : ι, s n := by
    apply Subset.antisymm
    · rintro y ⟨x, rfl⟩
      refine mem_iInter.2 fun n => ?_
      have : f n ((x : γ) n) = F x := (mem_iInter.1 x.2 n :)
      rw [← this, ← f_range n]
      exact mem_range_self _
    · intro y hy
      have A : ∀ n, ∃ x : β n, f n x = y := by
        intro n
        rw [← mem_range, f_range n]
        exact mem_iInter.1 hy n
      choose x hx using A
      have xt : x ∈ t := by
        refine mem_iInter.2 fun n => ?_
        simp [γ, hx]
      refine ⟨⟨x, xt⟩, ?_⟩
      exact hx i₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ (n : ι), {x : γ | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace.{u_2} (↑t : Type u_2)
F : (↑t : Type u_2) → α := fun (x : (↑t : Type u_2)) ↦ f i₀ ((↑x : γ) i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
F_range : range F = ⋂ (n : ι), s n
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
have rw : AnalyticSet (range F)
Tactic: rw [← F_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
⊢ AnalyticSet.{u_1} (α := α) (⋃ (n : ι), s n)
have choose : ∀ (β : (n : ι) → Type) (hβ : (n : ι) → TopologicalSpace (β n)) (h'β : ∀ (n : ι), PolishSpace (β n))
  (f : (n : ι) → β n → α) (f_cont : ∀ (n : ι), Continuous[_, inst] (f n)) (f_range : ∀ (n : ι), range (f n) = s n),
  AnalyticSet.{u_1} (α := α) (⋃ (n : ι), s n)
Tactic: choose β hβ h'β f f_cont f_range using fun n =>
    analyticSet_iff_exists_polishSpace_range.1 (hs n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
F : γ → α :=
  fun (x : γ) ↦
    match (motive := γ → α) x with
    | ⟨n, x⟩ => f n x
⊢ AnalyticSet.{u_1} (α := α) (⋃ (n : ι), s n)
have F_cont : Continuous[instTopologicalSpaceSigma, inst] F
Tactic: have F_cont : Continuous F := continuous_sigma f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
F : γ → α :=
  fun (x : γ) ↦
    match (motive := γ → α) x with
    | ⟨n, x⟩ => f n x
F_cont : Continuous[instTopologicalSpaceSigma, inst] F
⊢ AnalyticSet.{u_1} (α := α) (⋃ (n : ι), s n)
have F_range : range F = ⋃ (n : ι), s n
Tactic: have F_range : range F = ⋃ n, s n := by
    simp only [γ, F, range_sigma_eq_iUnion_range, f_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : (n : ι) → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
F : γ → α :=
  fun (x : γ) ↦
    match (motive := γ → α) x with
    | ⟨n, x⟩ => f n x
F_cont : Continuous[instTopologicalSpaceSigma, inst] F
F_range : range F = ⋃ (n : ι), s n
⊢ AnalyticSet.{u_1} (α := α) (⋃ (n : ι), s n)
have rw : AnalyticSet (range F)
Tactic: rw [← F_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
⊢ AnalyticSet s
have this : PolishSpace.{u_1} (↑s : Type u_1)
Tactic: haveI : PolishSpace s := hs.polishSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this : PolishSpace.{u_1} (↑s : Type u_1)
⊢ AnalyticSet s
have rw : AnalyticSet.{u_1} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
Tactic: rw [← @Subtype.range_val α s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
s : Set α
hs : MeasurableSet s
⊢ IsClopenable s
have revert : ∀ {s : Set α} (hs : MeasurableSet s), IsClopenable s
Tactic: revert s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ {s : Set α} (hs : MeasurableSet s), IsClopenable s
have isOpen : ∀ (U : Set α) (hU : IsOpen[inst] U), IsClopenable U
Tactic: apply MeasurableSet.induction_on_open
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
isOpen : ∀ (U : Set α) (hU : IsOpen[inst] U), IsClopenable U
⊢ ∀ {s : Set α} (hs : MeasurableSet s), IsClopenable s
have compl : ∀ (t : Set α) (ht : MeasurableSet t), IsClopenable t → IsClopenable tᶜ
Tactic: apply MeasurableSet.induction_on_open
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
isOpen : ∀ (U : Set α) (hU : IsOpen[inst] U), IsClopenable U
compl : ∀ (t : Set α) (ht : MeasurableSet t), IsClopenable t → IsClopenable tᶜ
⊢ ∀ {s : Set α} (hs : MeasurableSet s), IsClopenable s
have iUnion : ∀ (f : ℕ → Set α),
  Pairwise (Disjoint on f) →
    ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)),
      (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable.{u_1} (α := α) (⋃ (i : ℕ), f i)
Tactic: apply MeasurableSet.induction_on_open
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
hs : MeasurableSet s
⊢ AnalyticSet s
have obtain : ∀ (t' : TopologicalSpace α) (t't : t' ≤ t) (t'_polish : PolishSpace α) (s_closed : IsClosed s), IsOpen s → AnalyticSet s
Tactic: obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
      ∃ t' : TopologicalSpace α, t' ≤ t ∧ @PolishSpace α t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
    hs.isClopenable
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_3
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed[t'] s
right : IsOpen[t'] s
⊢ AnalyticSet s
have A : AnalyticSet s
Tactic: have A := @IsClosed.analyticSet α t' t'_polish s s_closed
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed[t'] s
right : IsOpen[t'] s
A : AnalyticSet s
⊢ AnalyticSet s
have h : s = id '' s
Tactic: convert! @AnalyticSet.image_of_continuous α t' α t s A id (continuous_id_of_le t't)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
have obtain : ∀ (b : Set (Set (↑(range f) : Type u_4))) (b_count : b.Countable) (hb : IsTopologicalBasis b),
  ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
Tactic: obtain ⟨b, b_count, -, hb⟩ :
      ∃ b : Set (Set (range f)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
    exists_countable_basis (range f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
have this : Countable.{u_4 + 1} (↑b : Type u_4)
Tactic: haveI : Countable b := b_count.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
s : (↑b : Type u_4)
⊢ IsClopenable (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
have hs : MeasurableSet (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Tactic: apply MeasurableSet.isClopenable
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
have this₁ : ∀ (s : (↑b : Type u_4)), IsClopenable (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Tactic: have : ∀ s : b, IsClopenable (rangeFactorization f ⁻¹' s) := fun s ↦ by
    apply MeasurableSet.isClopenable
    exact hf.subtype_mk (hb.isOpen s.2).measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this_1 : Countable.{u_4 + 1} (↑b : Type u_4)
this : ∀ (s : (↑b : Type u_4)), IsClopenable (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
have choose : ∀ (T : (s : (↑b : Type u_4)) → TopologicalSpace α) (Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t)
  (Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α),
  (∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))) →
    ∀ (Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))),
      ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
Tactic: choose T Tt Tpolish _ Topen using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
have obtain : ∀ (t' : TopologicalSpace α) (t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i) (t't : t' ≤ t) (t'_polish : PolishSpace α),
  ∃ t' ≤ t, Continuous[_, tβ] 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
have refine : Continuous[t', tβ] f
Tactic: refine ⟨t', t't, ?_, t'_polish⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ Continuous[t', tβ] f
have this₁ : Continuous[t', instTopologicalSpaceSubtype] (rangeFactorization f)
Tactic: have : Continuous[t', _] (rangeFactorization f) :=
    hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
⊢ AnalyticSet (f '' s)
have hs₁ : MeasurableSet s
Tactic: rw [eq_borel_upgradeStandardBorel X] at hs
Cleared hypotheses: hs, hf, this