case pos
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : ¬Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
by_cases hα : Countable α
case pos.inl
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

case pos.inr
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
cases finite_or_infinite α
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
case pos.inl
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ MeasurableSet (range fun x => ↑↑x)
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
refine' ⟨_, _, h_nonempty_equiv⟩
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this : MeasurableSpace (Fin n) := borel (Fin n)
⊢ MeasurableSet (range fun x => ↑↑x)
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ MeasurableSet (range fun x => ↑↑x)
letI : MeasurableSpace (Fin n) := borel (Fin n)
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this✝ : MeasurableSpace (Fin n) := borel (Fin n)
this : BorelSpace (Fin n)
⊢ MeasurableSet (range fun x => ↑↑x)
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this : MeasurableSpace (Fin n) := borel (Fin n)
⊢ MeasurableSet (range fun x => ↑↑x)
haveI : BorelSpace (Fin n) := ⟨rfl⟩
case pos.inl.intro.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this✝ : MeasurableSpace (Fin n) := borel (Fin n)
this : BorelSpace (Fin n)
⊢ MeasurableSpace (Fin n)

case pos.inl.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this✝ : MeasurableSpace (Fin n) := borel (Fin n)
this : BorelSpace (Fin n)
⊢ MeasurableEmbedding fun x => ↑↑x
case pos.inl.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this✝ : MeasurableSpace (Fin n) := borel (Fin n)
this : BorelSpace (Fin n)
⊢ MeasurableSet (range fun x => ↑↑x)
refine' MeasurableEmbedding.measurableSet_range _
no goals
case pos.inl.intro.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this✝ : MeasurableSpace (Fin n) := borel (Fin n)
this : BorelSpace (Fin n)
⊢ MeasurableSpace (Fin n)
infer_instance
no goals
case pos.inl.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
this✝ : MeasurableSpace (Fin n) := borel (Fin n)
this : BorelSpace (Fin n)
⊢ MeasurableEmbedding fun x => ↑↑x
exact
  continuous_of_discreteTopology.measurableEmbedding
    (Nat.cast_injective.comp Fin.val_injective)
case pos.inr
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSet (range Nat.cast)
case pos.inr
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
refine' ⟨_, _, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
case pos.inr.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSpace ℕ

case pos.inr.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableEmbedding Nat.cast
case pos.inr
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSet (range Nat.cast)
refine' MeasurableEmbedding.measurableSet_range _
no goals
case pos.inr.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSpace ℕ
infer_instance
no goals
case pos.inr.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableEmbedding Nat.cast
exact continuous_of_discreteTopology.measurableEmbedding Nat.cast_injective
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : ¬Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
refine'
  ⟨univ, MeasurableSet.univ,
    ⟨(PolishSpace.measurableEquivOfNotCountable hα _ : α ≃ᵐ (univ : Set ℝ))⟩⟩
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : ¬Countable α
⊢ ¬Set.Countable univ
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ
rw [countable_coe_iff]
no goals
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.399198
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
hα : ¬Countable α
⊢ ¬Set.Countable univ
exact Cardinal.not_countable_real