awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A : ∀ (n : ι), ∃ (x : β n), f n x = y
h₂ : ∀ (x : (n : ι) → β n) (hx : ∀ (n : ι), f n (x n) = y), y ∈ range F
⊢ y ∈ range F

Tactic:
choose x hx using A
-- 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
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ x ∈ t

Tactic:
mem_iInter.2 fun n => ?_

Premises used: Iff.mpr, Set.Mem, 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
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
refine : ∀ (n : ι), Membership.mem (γ := Set ((n : ι) → β n)) {x : γ | f n (x n) = f i₀ (x i₀)} x
⊢ x ∈ t

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
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ι), s n) y
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
n : ι
⊢ Membership.mem (γ := Set ((n : ι) → β n)) {x : γ | f n (x n) = f i₀ (x i₀)} x

Tactic:
simp [γ, hx]
-- 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
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ x ∈ t

Tactic:
have xt : x ∈ t := by
        refine mem_iInter.2 fun n => ?_
        simp [γ, hx]
-- 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
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
⊢ y ∈ range F

Tactic:
⟨⟨x, xt⟩, ?_⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.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
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
h₂ : F (Subtype.mk (p := fun (x : γ) ↦ x ∈ t) x xt) = y
⊢ y ∈ range F

Tactic:
refine ⟨⟨x, xt⟩, ?_⟩
-- 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
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
⊢ F (Subtype.mk (p := fun (x : γ) ↦ x ∈ t) x xt) = y

Tactic:
hx 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
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
⊢ F (Subtype.mk (p := fun (x : γ) ↦ x ∈ t) x xt) = y

Tactic:
exact hx 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
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
⊢ 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₀
-- 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
F_range : range F = ⋂ (n : ι), s n
rw : AnalyticSet (range F)
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)

Tactic:
rw [← F_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
F_range : range F = ⋂ (n : ι), s n
⊢ 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
ι : 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 (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
ι : Type u_2
inst : TopologicalSpace α
inst_1 : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
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 ι
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
⊢ Continuous[instTopologicalSpaceSigma, inst] F

Tactic:
have F_cont : Continuous F := continuous_sigma f_cont
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ range F = ⋃ (n : ι), s n

Tactic:
simp only [γ, F, range_sigma_eq_iUnion_range, f_range]

Premises used: Set.range_sigma_eq_iUnion_range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ 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]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
rw : AnalyticSet (range F)
⊢ AnalyticSet.{u_1} (α := α) (⋃ (n : ι), s n)

Tactic:
rw [← F_range]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 (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
ι : 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 (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 α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
⊢ PolishSpace.{u_1} (↑s : Type u_1)

Tactic:
haveI : PolishSpace s := hs.polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this : PolishSpace.{u_1} (↑s : Type u_1)
rw : AnalyticSet.{u_1} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
⊢ AnalyticSet s

Tactic:
rw [← @Subtype.range_val α s]

Premises used: Subtype.range_val
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this : PolishSpace.{u_1} (↑s : Type u_1)
⊢ AnalyticSet.{u_1} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))

Tactic:
analyticSet_range_of_polishSpace continuous_subtype_val

Premises used: continuous_subtype_val, MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this : PolishSpace.{u_1} (↑s : Type u_1)
⊢ AnalyticSet.{u_1} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))

Tactic:
exact analyticSet_range_of_polishSpace continuous_subtype_val

Premises used: continuous_subtype_val, MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
s : Set α
hs : MeasurableSet s
revert : ∀ {s : Set α} (hs : MeasurableSet s), IsClopenable s
⊢ IsClopenable s

Tactic:
revert s
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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ᶜ
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable.{u_1} (α := α) (⋃ (i : ℕ), f i)
⊢ ∀ {s : Set α} (hs : MeasurableSet s), IsClopenable s

Tactic:
apply MeasurableSet.induction_on_open
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ (U : Set α) (hU : IsOpen[inst] U), IsClopenable U

Tactic:
fun u hu => hu.isClopenable

Premises used: IsOpen.isClopenable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ (U : Set α) (hU : IsOpen[inst] U), IsClopenable U

Tactic:
exact fun u hu => hu.isClopenable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ (t : Set α) (ht : MeasurableSet t), IsClopenable t → IsClopenable tᶜ

Tactic:
fun u _ h'u => h'u.compl

Premises used: PolishSpace.IsClopenable.compl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ (t : Set α) (ht : MeasurableSet t), IsClopenable t → IsClopenable tᶜ

Tactic:
exact fun u _ h'u => h'u.compl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable.{u_1} (α := α) (⋃ (i : ℕ), f i)

Tactic:
fun f _ _ hf => IsClopenable.iUnion hf

Premises used: PolishSpace.IsClopenable.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable.{u_1} (α := α) (⋃ (i : ℕ), f i)

Tactic:
exact fun f _ _ hf => IsClopenable.iUnion hf

Premises used: PolishSpace.IsClopenable.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
hs : MeasurableSet s
⊢ ∃ t' ≤ t, PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
hs.isClopenable

Premises used: MeasurableSet.isClopenable, PolishSpace.IsClopenable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
hs : MeasurableSet s
obtain :
  ∀ (t' : TopologicalSpace α) (t't : t' ≤ t) (t'_polish : PolishSpace α) (s_closed : IsClosed s),
    IsOpen s → AnalyticSet 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

Premises used: MeasurableSet.isClopenable, TopologicalSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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

Tactic:
have A := @IsClosed.analyticSet α t' t'_polish s s_closed
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 (id '' s)

Tactic:
@AnalyticSet.image_of_continuous α t' α t s A id (continuous_id_of_le t't)

Premises used: MeasureTheory.AnalyticSet.image_of_continuous, continuous_id_of_le
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
h : s = id '' s
⊢ AnalyticSet s

Tactic:
convert! @AnalyticSet.image_of_continuous α t' α t s A id (continuous_id_of_le t't)

Premises used: MeasureTheory.AnalyticSet.image_of_continuous, continuous_id_of_le