awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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) μ
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))
⊢ AEMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ

Tactic:
apply aemeasurable_of_tendsto_metrizable_ae L.filter (f := fun s => ∏ i ∈ s, f i)

Premises used: SummationFilter.filter, aemeasurable_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ ∀ (n : Finset ι), AEMeasurable.{u_6, u_7} (β := E) (∏ i ∈ n, f i) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ ∀ᵐ (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:
.of_forall fun x ↦ hm.choose_spec.apply_nhds x

Premises used: Exists.choose_spec, Filter.Eventually.of_forall, Filter.Tendsto.apply_nhds
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ ∀ᵐ (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:
exact .of_forall fun x ↦ hm.choose_spec.apply_nhds x
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
obtain :
  ∀ (t : TopologicalSpace α) (hle : t ≤ UpgradedStandardBorel.toTopologicalSpace) (ht : PolishSpace α)
    (s_clopen : IsClosed s ∧ IsOpen s), ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
⊢ ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
obtain ⟨t, hle, ht, s_clopen⟩ := hs.isClopenable

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

Tactic:
⟨t, ?_, ht, s_clopen⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
refine : BorelSpace α
⊢ ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
refine ⟨t, ?_, ht, s_clopen⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
measurable_eq : inst = borel α
⊢ BorelSpace α

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
rw : PolishSpace α
⊢ inst = borel α

Tactic:
rw [eq_borel_upgradeStandardBorel α, borel_eq_borel_of_le ht _ hle]

Premises used: MeasureTheory.borel_eq_borel_of_le, eq_borel_upgradeStandardBorel
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ PolishSpace α

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
obtain :
  ∀ (w : TopologicalSpace α),
    BorelSpace α → PolishSpace α → ∀ (s_closed : IsClosed s), IsOpen s → StandardBorelSpace.{u_4} (↑s : Type u_4)
⊢ StandardBorelSpace.{u_4} (↑s : Type u_4)

Tactic:
obtain ⟨_, _, _, s_closed, _⟩ := hs.isClopenable'

Premises used: MeasurableSet.isClopenable'
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ PolishSpace.{u_4} (↑s : Type u_4)

Tactic:
haveI := s_closed.polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
this : PolishSpace.{u_4} (↑s : Type u_4)
⊢ StandardBorelSpace.{u_4} (↑s : Type u_4)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 α
h₁ : Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
⊢ α ≃ᵐ (ℕ → Bool)

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 α
rwa : ¬Countable.{u_4 + 1} (↑univ : Type u_4)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬Countable α
⊢ ¬Set.Countable.{u_4} (α := α) univ

Tactic:
rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff]

Premises used: Set.countable_coe_iff, Equiv.countable_iff, Equiv.Set.univ
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 α
h₁ :
  ∀ (f : (ℕ → Bool) → α) (fcts : Continuous[_, this.toTopologicalSpace] f) (finj : Injective f),
    Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
⊢ 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])

Premises used: isClosed_univ, IsClosed.exists_nat_bool_injection_of_not_countable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
h₁ : ∀ (g : α → ℕ → Bool) (gmeas : Measurable g) (ginj : Injective g), Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))
⊢ Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))

Tactic:
obtain ⟨g, gmeas, ginj⟩ :=
    MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated α

Premises used: MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
g : α → ℕ → Bool
gmeas : Measurable g
ginj : Injective g
⊢ Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))

Tactic:
⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩

Premises used: Nonempty.intro, Continuous.measurable, PolishSpace.borelSchroederBernstein
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
g : α → ℕ → Bool
gmeas : Measurable g
ginj : Injective g
⊢ Nonempty.{u_4 + 1} (α ≃ᵐ (ℕ → Bool))

Tactic:
exact ⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 α) → α ≃ᵐ β
neg : (h : ¬Countable α) → α ≃ᵐ β
⊢ α ≃ᵐ β

Tactic:
by_cases h : Countable α

Premises used: Countable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : α) → β)
pos₁ : Measurable.{u_6, u_4} (α := β) (β := α) (⇑e.symm : (a : β) → α)
⊢ α ≃ᵐ β

Tactic:
refine ⟨e, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β := ⋯
⊢ Measurable.{u_4, u_6} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
apply measurable_of_countable

Premises used: measurable_of_countable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β := ⋯
⊢ Measurable.{u_6, u_4} (α := β) (β := α) (⇑e.symm : (a : β) → α)

Tactic:
apply measurable_of_countable

Premises used: measurable_of_countable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 α
neg : ¬Countable β
⊢ α ≃ᵐ β

Tactic:
refine measurableEquivOfNotCountable h ?_

Premises used: PolishSpace.measurableEquivOfNotCountable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 α
neg neg₁ neg₂ neg₃ : ∀ (h : ¬Countable β), ¬Countable β
⊢ ¬Countable β

Tactic:
rwa [e.countable_iff] at h

Premises used: Equiv.countable_iff
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Finite α
obtain :
  ∀ (n : ℕ) (n_equiv : α ≃ Fin n),
    ∃ (n : ℕ), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))
⊢ ∃ (n : ℕ), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))

Tactic:
obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))

Tactic:
⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩

Premises used: Equiv.trans, Nonempty.intro, Exists.intro, PolishSpace.Equiv.measurableEquiv
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Finite α
n : ℕ
n_equiv : α ≃ Fin n
refine : Fin n ≃ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type)
⊢ ∃ (n : ℕ), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type))

Tactic:
refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ (↑(range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ)) : Type)

Tactic:
exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)

Premises used: Equiv.ofInjective, Fin.val_injective, Function.Injective.comp, Nat.cast_injective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Infinite α
inst_3 : Countable α
⊢ PolishSpace (↑(range Nat.cast) : Type)

Tactic:
have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
    Nat.isClosedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))

Tactic:
⟨PolishSpace.Equiv.measurableEquiv ?_⟩

Premises used: Nonempty.intro, PolishSpace.Equiv.measurableEquiv
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Infinite α
inst_3 : Countable α
this : PolishSpace (↑(range Nat.cast) : Type)
refine : α ≃ (↑(range Nat.cast) : Type)
⊢ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑(range Nat.cast) : Type))

Tactic:
refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
inst_2 : Infinite α
inst_3 : Countable α
this : PolishSpace (↑(range Nat.cast) : Type)
refine : ℕ ≃ (↑(range Nat.cast) : Type)
⊢ α ≃ (↑(range Nat.cast) : Type)

Tactic:
refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_

Premises used: Equiv.trans, Nonempty.some, nonempty_equiv_of_countable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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)

Tactic:
exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective

Premises used: Nat.cast, Equiv.ofInjective, Nat.cast_injective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
pos : ∀ (hα : Countable α), ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
neg : ∀ (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))

Tactic:
by_cases hα : Countable α

Premises used: Countable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))
pos₁ : Infinite α → ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))

Tactic:
cases finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Finite α
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))
⊢ ∃ (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 α

Premises used: MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))

Tactic:
⟨_, ?_, h_nonempty_equiv⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))
pos : MeasurableSet (α := ℝ) (range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ))
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))

Tactic:
refine ⟨_, ?_, h_nonempty_equiv⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))
⊢ MeasurableSet (α := ℝ) (range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ))

Tactic:
(Set.finite_range ((↑) : Fin n → ℝ)).measurableSet

Premises used: Set.finite_range, Fin.val, Nat.cast, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))
⊢ MeasurableSet (α := ℝ) (range fun (x : Fin n) ↦ (↑(↑x : ℕ) : ℝ))

Tactic:
exact (Set.finite_range ((↑) : Fin n → ℝ)).measurableSet

Premises used: Set.finite_range, Fin.val, Nat.cast, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
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))

Tactic:
⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩

Premises used: MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Infinite α
pos : MeasurableSet (α := ℝ) (range Nat.cast)
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))

Tactic:
refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Infinite α
⊢ MeasurableSet (α := ℝ) (range Nat.cast)

Tactic:
Nat.isClosedEmbedding_coe_real.isClosed_range.measurableSet

Premises used: IsClosed.measurableSet, Nat.isClosedEmbedding_coe_real, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : Countable α
h : Infinite α
⊢ MeasurableSet (α := ℝ) (range Nat.cast)

Tactic:
exact Nat.isClosedEmbedding_coe_real.isClosed_range.measurableSet

Premises used: IsClosed.measurableSet, Nat.isClosedEmbedding_coe_real, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : ¬Countable α
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))

Tactic:
⟨univ, MeasurableSet.univ,
        ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩

Premises used: PolishSpace.measurableEquivOfNotCountable, Set.univ, Nonempty.intro, And.intro, Exists.intro, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : ¬Countable α
neg : ¬Countable (↑univ : Type)
⊢ ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))

Tactic:
refine
      ⟨univ, MeasurableSet.univ,
        ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩