-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem measurableEquiv_nat_bool_of_countablyGenerated [MeasurableSpace α]
    [CountablyGenerated α] [SeparatesPoints α] :
    ∃ s : Set (ℕ → Bool), Nonempty (α ≃ᵐ s)

Proof state:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ Subtype.val ⁻¹' {y | y n = true} = ⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n

Tactic:
rw [← Equiv.preimage_eq_iff_eq_image]

Result:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ ⇑(Equiv.ofInjective (mapNatBool α) ⋯) ⁻¹' (Subtype.val ⁻¹' {y | y n = true}) = natGeneratingSequence α n

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet {y | y n = true}

Tactic:
measurability

Result:
no goals

Proof state:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n)

Tactic:
refine ⟨{y | y n}, by measurability, ?_⟩

Result:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ Subtype.val ⁻¹' {y | y n = true} = ⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ ∃ s, Nonempty (α ≃ᵐ ↑s)

Tactic:
use range (mapNatBool α), Equiv.ofInjective _ <|
  injective_mapNatBool _,
  Measurable.subtype_mk <| measurable_mapNatBool _

Result:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ Measurable ⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm

Proof state:
case measurable_invFun.h
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' t)

Tactic:
rintro _ ⟨n, rfl⟩

Result:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' natGeneratingSequence α n)

Proof state:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ ⇑(Equiv.ofInjective (mapNatBool α) ⋯) ⁻¹' (Subtype.val ⁻¹' {y | y n = true}) = natGeneratingSequence α n

Tactic:
simp [mapNatBool]

Result:
no goals

Proof state:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ Measurable ⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm

Tactic:
apply measurable_generateFrom

Result:
case measurable_invFun.h
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' t)

Proof state:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' natGeneratingSequence α n)

Tactic:
rw [← Equiv.image_eq_preimage _ _]

Result:
case measurable_invFun.h.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n)