-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem injective_mapNatBool [MeasurableSpace α] [CountablyGenerated α]
    [SeparatesPoints α] : Injective (mapNatBool α)

Proof state:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ ∀ s ∈ range (natGeneratingSequence α), x ∈ s ↔ y ∈ s

Tactic:
rintro - ⟨n, rfl⟩

Result:
case a.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n

Proof state:
case a.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)

α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (x ∈ natGeneratingSequence α n)

α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (y ∈ natGeneratingSequence α n)

Tactic:
exact congr_fun hxy n

Result:
no goals

Proof state:
case a.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n

Tactic:
rw [← decide_eq_decide]

Result:
case a.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)

α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (x ∈ natGeneratingSequence α n)

α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (y ∈ natGeneratingSequence α n)

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ Injective (mapNatBool α)

Tactic:
intro x y hxy

Result:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y

Tactic:
rw [← generateFrom_natGeneratingSequence α] at *

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y

Tactic:
apply separating_of_generateFrom (range (natGeneratingSequence _))

Result:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ ∀ s ∈ range (natGeneratingSequence α), x ∈ s ↔ y ∈ s