-- Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
theorem exists_subset_real_measurableEquiv : ∃ s : Set ℝ, MeasurableSet s ∧ Nonempty (α ≃ᵐ s)

Proof state:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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)

Tactic:
haveI : BorelSpace (Fin n) := ⟨rfl⟩

Result:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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)

Proof state:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ MeasurableSet (range fun x => ↑↑x)

Tactic:
letI : MeasurableSpace (Fin n) := borel (Fin n)

Result:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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)

Proof state:
case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSet (range Nat.cast)

Tactic:
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)

Result:
case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableEmbedding Nat.cast

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable

Tactic:
exact Cardinal.not_countable_real

Result:
no goals

Proof state:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
refine ⟨_, ?_, h_nonempty_equiv⟩

Result:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ MeasurableSet (range fun x => ↑↑x)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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)

Tactic:
infer_instance

Result:
no goals

Proof state:
case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableEmbedding Nat.cast

Tactic:
exact continuous_of_discreteTopology.measurableEmbedding Nat.cast_injective

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
cases finite_or_infinite α

Result:
case pos.inl
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
by_cases hα : Countable α

Result:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

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

Result:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ

Proof state:
case pos.inl
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α

Result:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Proof state:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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)

Tactic:
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)

Result:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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

Proof state:
case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩

Result:
case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSet (range Nat.cast)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSpace ℕ

Tactic:
infer_instance

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ

Tactic:
rw [countable_coe_iff]

Result:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable

Proof state:
case pos.inl.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
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

Tactic:
exact continuous_of_discreteTopology.measurableEmbedding
  (Nat.cast_injective.comp Fin.val_injective)

Result:
no goals