awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
have neg : ∀ (n : Finset ι), AEMeasurable.{u_6, u_7} (β := E) (∏ i ∈ n, f i) μ
Tactic: apply aemeasurable_of_tendsto_metrizable_ae L.filter (f := fun s => ∏ i ∈ s, f i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
neg : ∀ (n : Finset ι), AEMeasurable.{u_6, u_7} (β := E) (∏ i ∈ n, f i) μ
⊢ AEMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
have neg₁ : ∀ᵐ (x : X) ∂μ,
  Tendsto (fun (n : Finset ι) ↦ (∏ i ∈ n, f i) x) L.filter
    (𝓝 (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm x))
Tactic: apply aemeasurable_of_tendsto_metrizable_ae L.filter (f := fun s => ∏ i ∈ s, f i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
have obtain : ∀ (t : TopologicalSpace α) (hle : t ≤ UpgradedStandardBorel.toTopologicalSpace) (ht : PolishSpace α)
  (s_clopen : IsClosed s ∧ IsOpen s), ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
Tactic: obtain ⟨t, hle, ht, s_clopen⟩ := hs.isClopenable
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed[t] s ∧ IsOpen[t] s
⊢ ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
have refine : BorelSpace α
Tactic: refine ⟨t, ?_, ht, s_clopen⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed[t] s ∧ IsOpen[t] s
⊢ BorelSpace α
have measurable_eq : inst = borel α
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed[t] s ∧ IsOpen[t] s
⊢ inst = borel α
have rw : PolishSpace α
Tactic: rw [eq_borel_upgradeStandardBorel α, borel_eq_borel_of_le ht _ hle]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ StandardBorelSpace.{u_4} (↑s : Type u_4)
have obtain : ∀ (w : TopologicalSpace α),
  BorelSpace α → PolishSpace α → ∀ (s_closed : IsClosed s), IsOpen s → StandardBorelSpace.{u_4} (↑s : Type u_4)
Tactic: obtain ⟨_, _, _, s_closed, _⟩ := hs.isClopenable'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w : TopologicalSpace α
left : BorelSpace α
left_1 : PolishSpace α
s_closed : IsClosed[w] s
right : IsOpen[w] s
⊢ StandardBorelSpace.{u_4} (↑s : Type u_4)
have this : PolishSpace.{u_4} (↑s : Type u_4)
Tactic: haveI := s_closed.polishSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
h : ¬Countable α
⊢ α ≃ᵐ (ℕ → Bool)
have h₁ : Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
Tactic: apply Nonempty.some
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬Set.Countable.{u_4} (α := α) univ
have rwa : ¬Countable.{u_4 + 1} (↑univ : Type u_4)
Tactic: rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
have h₁ : ∀ (f : (ℕ → Bool) → α) (fcts : Continuous[_, this.toTopologicalSpace] f) (finj : Injective f),
  Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
Tactic: obtain ⟨f, -, fcts, finj⟩ :=
    isClosed_univ.exists_nat_bool_injection_of_not_countable (α := α)
      (by rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff])
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
f : (ℕ → Bool) → α
fcts : Continuous[_, this.toTopologicalSpace] f
finj : Injective f
⊢ Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
have h₁ : ∀ (g : α → ℕ → Bool) (gmeas : Measurable g) (ginj : Injective g), Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
Tactic: obtain ⟨g, gmeas, ginj⟩ :=
    MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
e : α ≃ β
⊢ α ≃ᵐ β
have pos : (h : Countable α) → α ≃ᵐ β
Tactic: by_cases h : Countable α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
e : α ≃ β
pos : (h : Countable α) → α ≃ᵐ β
⊢ α ≃ᵐ β
have neg : (h : ¬Countable α) → α ≃ᵐ β
Tactic: by_cases h : Countable α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := ⋯
⊢ α ≃ᵐ β
have pos : Measurable.{u_4, u_6} (α := α) (β := β) (⇑e : (a : α) → β)
Tactic: refine ⟨e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := ⋯
pos : Measurable.{u_4, u_6} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ α ≃ᵐ β
have pos₁ : Measurable.{u_6, u_4} (α := β) (β := α) (⇑e.symm : (a : β) → α)
Tactic: refine ⟨e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
e : α ≃ β
h : ¬Countable α
⊢ α ≃ᵐ β
have neg : ¬Countable β
Tactic: refine measurableEquivOfNotCountable h ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α_1 : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β_1 : Type u_5
inst : MeasurableSpace β_1
β : Type u_6
inst_1 : MeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : StandardBorelSpace α
inst_4 : StandardBorelSpace β
e : α ≃ β
h : ¬Countable α
⊢ ¬Countable β
have neg : ∀ (h : ¬Countable β), ¬Countable β
Tactic: rwa [e.countable_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Finite α
⊢ ∃ (n : ℕ), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))
have obtain : ∀ (n : ℕ) (n_equiv : α ≃ Fin n),
  ∃ (n : ℕ), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))
Tactic: obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ ∃ (n : ℕ), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))
have refine : Fin n ≃ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type)
Tactic: refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Infinite α
inst_3 : Countable α
⊢ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range Nat.cast) : Type))
have this : PolishSpace (↑(range Nat.cast) : Type)
Tactic: have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
    Nat.isClosedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Infinite α
inst_3 : Countable α
this : PolishSpace (↑(range Nat.cast) : Type)
⊢ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range Nat.cast) : Type))
have refine : α ≃ (↑(range Nat.cast) : Type)
Tactic: refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Infinite α
inst_3 : Countable α
this : PolishSpace (↑(range Nat.cast) : Type)
⊢ α ≃ (↑(range Nat.cast) : Type)
have refine : ℕ ≃ (↑(range Nat.cast) : Type)
Tactic: refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have pos : ∀ (hα : Countable α), ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
Tactic: by_cases hα : Countable α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
pos : ∀ (hα : Countable α), ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have neg : ∀ (hα : ¬Countable α), ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
Tactic: by_cases hα : Countable α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have pos : Finite α → ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
pos : Finite α → ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have pos₁ : Infinite α → ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Finite α
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have pos : ∀ (n : ℕ) (h_nonempty_equiv : Nonempty.{u_1 + 1} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))),
  ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
Tactic: obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Finite α
n : ℕ
h_nonempty_equiv : Nonempty.{u_1 + 1} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have pos : MeasurableSet (α := ℝ) (range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ))
Tactic: refine ⟨_, ?_, h_nonempty_equiv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Infinite α
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have pos : MeasurableSet (α := ℝ) (range Nat.cast)
Tactic: refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : ¬Countable α
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have neg : ¬Countable (↑univ : Type)
Tactic: refine
      ⟨univ, MeasurableSet.univ,
        ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
⊢ ∃ (f : α → ℝ), MeasurableEmbedding f
have obtain : ∀ (s : Set ℝ) (hs : MeasurableSet s) (e : α ≃ᵐ (↑s : Type)), ∃ (f : α → ℝ), MeasurableEmbedding f
Tactic: obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have inl : ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥],
  MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) ⊥ (𝓝 c)}
Tactic: obtain rfl | hl := eq_or_neBot l
Cleared hypotheses: l, inst_3
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inl :
  ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥],
    MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) ⊥ (𝓝 c)}
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have inr : ∀ (hl : l.NeBot), MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
Tactic: obtain rfl | hl := eq_or_neBot l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have this₁ : SecondCountableTopology.{u_3} (↑s : Type u_3)
Tactic: have : SecondCountableTopology s := @UniformSpace.secondCountable_of_separable s _ _
    (IsSeparable.iUnion (fun i ↦ (hf i).isSeparable_range)).closure.separableSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this : SecondCountableTopology.{u_3} (↑s : Type u_3)
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have this₁ : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
Tactic: have : IsCompletelyPseudoMetrizableSpace s := isClosed_closure.isCompletelyPseudoMetrizableSpace
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have mg : ∀ (i : ι), Measurable (g i)
Tactic: have mg i : Measurable (g i) := (hf i).measurable.subtype_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
have h : ∀ (x : X),
  (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) ↔
    ∃ (c : (↑s : Type u_3)), Tendsto (fun (n : ι) ↦ g n x) l (𝓝 c)
Tactic: convert! MeasureTheory.measurableSet_exists_tendsto (l := l) mg with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
x : X
⊢ (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) ↔
    ∃ (c : (↑s : Type u_3)), Tendsto (fun (n : ι) ↦ g n x) l (𝓝 c)
have h : (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) →
  ∀ (c : E) (hc : Tendsto (fun (x_2 : ι) ↦ f x_2 x) l (𝓝 c)), c ∈ s
Tactic: refine ⟨fun ⟨c, hc⟩ ↦ ⟨⟨c, ?_⟩, tendsto_subtype_rng.2 hc⟩,
    fun ⟨c, hc⟩ ↦ ⟨c, tendsto_subtype_rng.1 hc⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
have inl : ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥],
  StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ limUnder ⊥ fun (x_1 : ι) ↦ f x_1 x
Tactic: obtain rfl | hl := eq_or_neBot l
Cleared hypotheses: l, inst_3