awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_4
inst : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
⊢ Measure.map (fun (a : (i : ι) → α i) (i : ι) ↦ f i (a i)) (Measure.pi (α := α) μ) = Measure.pi (α := β) ν
have this : ∀ (i : ι), SigmaFinite (m0 := inst_2 i) (Measure.map (f i) (μ i))
Tactic: have (i : ι) : SigmaFinite ((μ i).map (f i)) := (hf i).map_eq ▸ hν i
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_4
inst : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (m0 := inst_2 i) (Measure.map (f i) (μ i))
⊢ Measure.map (fun (a : (i : ι) → α i) (i : ι) ↦ f i (a i)) (Measure.pi (α := α) μ) = Measure.pi (α := β) ν
have rw : (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (μ i)) = Measure.pi (α := β) ν
Tactic: rw [pi_map_pi (fun i ↦ (hf i).aemeasurable)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasurableSpace β₁
inst_3 : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst_4 : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ : (a : β₁) → β₂) (μ i) (ν ((eα : (a : α₁) → α₂) i))
⊢ MeasurePreserving (α := α₁ → β₁) (β := α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (Measure.pi (α := fun (a : α₁) ↦ β₁) fun (i : α₁) ↦ μ i) (Measure.pi (α := fun (a : α₂) ↦ β₂) fun (i : α₂) ↦ ν i)
have h : Eq (α := (α₁ → β₁) → α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
  (comp (β := (b : α₁) → β₂)
    (⇑(MeasurableEquiv.piCongrLeft.{u_4, u_6, u_7} (fun (i : α₂) ↦ β₂) eα : ((b : α₁) → β₂) ≃ᵐ ((a : α₂) → β₂)) :
      (a : (b : α₁) → β₂) → (a : α₂) → β₂)
    fun (a : (i : α₁) → β₁) (i : α₁) ↦ (eβ : (a : β₁) → β₂) (a i))
Tactic: convert!
    (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
      (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasurableSpace β₁
inst_3 : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst_4 : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ : (a : β₁) → β₂) (μ i) (ν ((eα : (a : α₁) → α₂) i))
⊢ MeasurePreserving (α := α₁ → β₁) (β := α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (Measure.pi (α := fun (a : α₁) ↦ β₁) fun (i : α₁) ↦ μ i) (Measure.pi (α := fun (a : α₂) ↦ β₂) fun (i : α₂) ↦ ν i)
have h : Eq (α := (α₁ → β₁) → α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
  (comp (β := (b : α₁) → β₂)
    (⇑(MeasurableEquiv.piCongrLeft.{u_4, u_6, u_7} (fun (i : α₂) ↦ β₂) eα : ((b : α₁) → β₂) ≃ᵐ ((a : α₂) → β₂)) :
      (a : (b : α₁) → β₂) → (a : α₂) → β₂)
    fun (a : (i : α₁) → β₁) (i : α₁) ↦ (eβ : (a : β₁) → β₂) (a i))
Tactic: classical
  convert!
    (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
      (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)
  simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe,
    comp_def, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft,
    Equiv.piCongrLeft, Equiv.symm_symm, Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
h : StandardBorelSpace α
⊢ UpgradedStandardBorel α
have choose : (τ : TopologicalSpace α) → (hb : BorelSpace α) → (hp : PolishSpace α) → UpgradedStandardBorel α
Tactic: choose τ hb hp using h.polish
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
τ : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : PolishSpace α
⊢ StandardBorelSpace α
have exists : BorelSpace α ∧ PolishSpace α
Tactic: exists τ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ AnalyticSet.{u_1} (α := α) ∅
have rw : Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = ∅
Tactic: rw [AnalyticSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
⊢ AnalyticSet (range f)
have inl : IsEmpty β → AnalyticSet (range f)
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
inl : IsEmpty β → AnalyticSet (range f)
⊢ AnalyticSet (range f)
have inr : Nonempty β → AnalyticSet (range f)
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : IsEmpty β
⊢ AnalyticSet (range f)
have inl : AnalyticSet.{u_1} (α := α) ∅
Tactic: rw [range_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
⊢ AnalyticSet (range f)
have inr : range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f
Tactic: rw [AnalyticSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
⊢ range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f
have inr : ∀ (g : (ℕ → ℕ) → β) (g_cont : Continuous[_, inst_1] g) (hg : Surjective g),
  range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f
Tactic: obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
      exists_nat_nat_continuous_surjective β
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst_1] g
hg : Surjective g
⊢ range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f
have inr : range (f ∘ g) = range f
Tactic: refine Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst_1] g
hg : Surjective g
⊢ range (f ∘ g) = range f
have inr : range f = range f
Tactic: rw [hg.range_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
s : Set β
hs : IsOpen[inst_1] s
f : β → α
f_cont : Continuous[inst_1, inst] f
⊢ AnalyticSet (f '' s)
have rw : AnalyticSet.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β))
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
s : Set β
hs : IsOpen[inst_1] s
f : β → α
f_cont : Continuous[inst_1, inst] f
⊢ AnalyticSet.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β))
have this : PolishSpace.{u_3} (↑s : Type u_3)
Tactic: haveI : PolishSpace s := hs.polishSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ AnalyticSet s ↔
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
have mp : AnalyticSet s →
  ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
mp :
  AnalyticSet s →
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
⊢ AnalyticSet s ↔
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
have mpr : (∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s) →
  AnalyticSet s
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : AnalyticSet s
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
have h₁ : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
Tactic: rw [AnalyticSet] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
have mp : ∀ (h : s = ∅),
  ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
have mp₁ : ∀ (h : ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s),
  ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
⊢ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
have mp : range Empty.elim = s
Tactic: refine ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = s
have mp : Eq.{u_1 + 1} (α := Set α) (range Empty.elim) ∅
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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 s
have mpr : AnalyticSet (range f)
Tactic: rw [← f_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
⊢ AnalyticSet (f '' s)
have rcases : ∀ (γ : Type) (γtop : TopologicalSpace γ) (γpolish : PolishSpace γ) (g : γ → α) (g_cont : Continuous[_, inst] g)
  (gs : range g = s), AnalyticSet (f '' s)
Tactic: rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨γ, γtop, γpolish, g, g_cont, gs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
have rw : f '' s = f '' range g
Tactic: rw [range_comp, gs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ f '' s = range (f ∘ g)
have rw₁ : f '' s = f '' s
Tactic: rw [range_comp, gs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
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
⊢ AnalyticSet (f '' s)
have this : f '' s = range (f ∘ g)
Tactic: have : f '' s = range (f ∘ g) := by rw [range_comp, gs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ AnalyticSet (f '' s)
have rw : AnalyticSet (range (f ∘ g))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ AnalyticSet (range (f ∘ g))
have f_cont : Continuous[γtop, inst_1] (f ∘ g)
Tactic: apply analyticSet_range_of_polishSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ Continuous[γtop, inst_1] (f ∘ g)
have apply : ∀ (x : γ), g x ∈ s
Tactic: apply hf.comp_continuous g_cont fun x => _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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 ∈ s
have rw : ∀ (x : γ), g x ∈ range g
Tactic: rw [← gs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
hι : Nonempty ι
inst_1 : Countable ι
inst_2 : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
have rcases : ∀ (i₀ : ι), AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
Tactic: rcases hι with ⟨i₀⟩
Cleared hypotheses: hι
-- 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₀ : ι
⊢ 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 (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₀)}
⊢ IsClosed[Pi.topologicalSpace] t
have h : ∀ (i : ι), IsClosed[Pi.topologicalSpace] {x : γ | f i (x i) = f i₀ (x i₀)}
Tactic: apply isClosed_iInter
-- 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₀)}
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
have t_closed : 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₀))
-- 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
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
have this : PolishSpace.{u_2} (↑t : Type u_2)
Tactic: haveI : PolishSpace t := t_closed.polishSpace
-- 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₀)
⊢ AnalyticSet.{u_1} (α := α) (⋂ (n : ι), s n)
have F_cont : Continuous[instTopologicalSpaceSubtype, inst] F
Tactic: have F_cont : Continuous F := (f_cont i₀).comp ((continuous_apply i₀).comp continuous_subtype_val)
-- 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
⊢ range F = ⋂ (n : ι), s n
have h₁ : range F ⊆ ⋂ (n : ι), s n
Tactic: apply Subset.antisymm
-- 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
h₁ : range F ⊆ ⋂ (n : ι), s n
⊢ range F = ⋂ (n : ι), s n
have h₂ : ⋂ (n : ι), s n ⊆ range F
Tactic: apply Subset.antisymm
-- 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
x : (↑t : Type u_2)
⊢ Membership.mem (γ := Set α) (⋂ (n : ι), s n) (F x)
have h₁ : ∀ (n : ι), F x ∈ s n
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
x : (↑t : Type u_2)
n : ι
⊢ F x ∈ s n
have this₁ : f n ((↑x : γ) n) = F x
Tactic: have : f n ((x : γ) n) = F x := (mem_iInter.1 x.2 n :)