awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
mp :
  ∀ (h : s = ∅),
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
mp₁ :
  ∀ (h : ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s),
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s

Tactic:
rcases h with h | h
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s

Tactic:
⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩

Premises used: Empty.elim, continuous_bot, inferInstance, Empty, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
mp : range Empty.elim = s
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s

Tactic:
refine ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
mp : Eq.{u_1 + 1} (α := Set α) (range Empty.elim) ∅
⊢ range Empty.elim = s

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
⊢ Eq.{u_1 + 1} (α := Set α) (range Empty.elim) ∅

Tactic:
range_eq_empty _

Premises used: Set.range_eq_empty
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
⊢ Eq.{u_1 + 1} (α := Set α) (range Empty.elim) ∅

Tactic:
exact range_eq_empty _

Premises used: Set.range_eq_empty
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s

Tactic:
⟨ℕ → ℕ, inferInstance, inferInstance, h⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s

Tactic:
exact ⟨ℕ → ℕ, inferInstance, inferInstance, h⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous[h, inst] f
f_range : range f = s
mpr : AnalyticSet (range f)
⊢ AnalyticSet s

Tactic:
rw [← f_range]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous[h, inst] f
f_range : range f = s
⊢ AnalyticSet (range f)

Tactic:
analyticSet_range_of_polishSpace f_cont

Premises used: MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous[h, inst] f
f_range : range f = s
⊢ AnalyticSet (range f)

Tactic:
exact analyticSet_range_of_polishSpace f_cont

Premises used: MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
rcases :
  ∀ (γ : Type) (γtop : TopologicalSpace γ) (γpolish : PolishSpace γ) (g : γ → α) (g_cont : Continuous[_, inst] g)
    (gs : range g = s), AnalyticSet (f '' s)
⊢ AnalyticSet (f '' s)

Tactic:
rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨γ, γtop, γpolish, g, g_cont, gs⟩

Premises used: MeasureTheory.analyticSet_iff_exists_polishSpace_range, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
rw : f '' s = f '' range g
rw₁ rw₂ : f '' s = f '' s
⊢ f '' s = range (f ∘ g)

Tactic:
rw [range_comp, gs]

Premises used: Set.range_comp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
⊢ f '' s = range (f ∘ g)

Tactic:
have : f '' s = range (f ∘ g) := by rw [range_comp, gs]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
this : f '' s = range (f ∘ g)
rw : AnalyticSet (range (f ∘ g))
⊢ AnalyticSet (f '' s)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
this : f '' s = range (f ∘ g)
f_cont : Continuous[γtop, inst_1] (f ∘ g)
⊢ AnalyticSet (range (f ∘ g))

Tactic:
apply analyticSet_range_of_polishSpace

Premises used: MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
this : f '' s = range (f ∘ g)
apply : ∀ (x : γ), g x ∈ s
⊢ Continuous[γtop, inst_1] (f ∘ g)

Tactic:
apply hf.comp_continuous g_cont fun x => _

Premises used: ContinuousOn.comp_continuous
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
this : f '' s = range (f ∘ g)
rw : ∀ (x : γ), g x ∈ range g
⊢ ∀ (x : γ), g x ∈ s

Tactic:
rw [← gs]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ range g

Tactic:
mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ range g

Tactic:
exact mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : Continuous[inst, inst_1] f
⊢ AnalyticSet (f '' s)

Tactic:
hs.image_of_continuousOn hf.continuousOn

Premises used: Continuous.continuousOn, MeasureTheory.AnalyticSet.image_of_continuousOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
hι : Nonempty ι
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
rcases : ∀ (i₀ : ι), AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)

Tactic:
rcases hι with ⟨i₀⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
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)
⊢ 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)

Premises used: MeasureTheory.analyticSet_iff_exists_polishSpace_range, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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₀)}
h : ∀ (i : ι), IsClosed[Pi.topologicalSpace] {x : γ | f i (x i) = f i₀ (x i₀)}
⊢ IsClosed[Pi.topologicalSpace] t

Tactic:
apply isClosed_iInter

Premises used: isClosed_iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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₀)}
n : ι
⊢ IsClosed[Pi.topologicalSpace] {x : γ | f n (x n) = f i₀ (x i₀)}

Tactic:
isClosed_eq ((f_cont n).comp (continuous_apply n)) ((f_cont i₀).comp (continuous_apply i₀))

Premises used: Continuous.comp, isClosed_eq, continuous_apply
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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₀)}
n : ι
⊢ IsClosed[Pi.topologicalSpace] {x : γ | f n (x n) = f i₀ (x i₀)}

Tactic:
exact
      isClosed_eq ((f_cont n).comp (continuous_apply n)) ((f_cont i₀).comp (continuous_apply i₀))

Premises used: Continuous.comp, isClosed_eq, continuous_apply
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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₀)}
⊢ IsClosed[Pi.topologicalSpace] t

Tactic:
have t_closed : IsClosed t := by
    apply isClosed_iInter
    intro n
    exact
      isClosed_eq ((f_cont n).comp (continuous_apply n)) ((f_cont i₀).comp (continuous_apply i₀))
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ PolishSpace.{u_2} (↑t : Type u_2)

Tactic:
haveI : PolishSpace t := t_closed.polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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₀)
⊢ Continuous[instTopologicalSpaceSubtype, inst] F

Tactic:
have F_cont : Continuous F := (f_cont i₀).comp ((continuous_apply i₀).comp continuous_subtype_val)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
h₁ : range F ⊆ ⋂ (n : ι), s n
h₂ : ⋂ (n : ι), s n ⊆ range F
⊢ range F = ⋂ (n : ι), s n

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
x : (↑t : Type u_2)
⊢ Membership.mem (γ := Set α) (⋂ (n : ι), s n) (F x)

Tactic:
mem_iInter.2 fun n => ?_

Premises used: Iff.mpr, Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
x : (↑t : Type u_2)
h₁ : ∀ (n : ι), F x ∈ s n
⊢ Membership.mem (γ := Set α) (⋂ (n : ι), s n) (F x)

Tactic:
refine mem_iInter.2 fun n => ?_

Premises used: Iff.mpr, Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
x : (↑t : Type u_2)
n : ι
⊢ f n ((↑x : γ) n) = F x

Tactic:
have : f n ((x : γ) n) = F x := (mem_iInter.1 x.2 n :)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
h₁ : f n ((↑x : γ) n) ∈ range (f n)
⊢ F x ∈ s n

Tactic:
rw [← this, ← f_range n]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 n ((↑x : γ) n) ∈ range (f n)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 n ((↑x : γ) n) ∈ range (f n)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : ι
rw : y ∈ s n
⊢ ∃ (x : β n), f n x = y

Tactic:
rw [← mem_range, f_range n]

Premises used: Set.mem_range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : ι
⊢ y ∈ s n

Tactic:
mem_iInter.1 hy n

Premises used: Set.mem_iInter, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : ι
⊢ y ∈ s n

Tactic:
exact mem_iInter.1 hy n

Premises used: Set.mem_iInter, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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

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