-- Mathlib/Topology/Category/LightProfinite/Sequence.lean
/--
The continuous map from `ℕ∪{∞}` to `ℝ` sending `n` to `1/(n+1)` and `∞` to `0` is a closed
embedding.
-/
lemma isClosedEmbedding_natUnionInftyEmbedding : IsClosedEmbedding natUnionInftyEmbedding

Proof state:
case refine_1

⊢ Function.Injective ⇑natUnionInftyEmbedding

Tactic:
rintro (_|n) (_|m) h

Result:
case refine_1.none.none
h : natUnionInftyEmbedding none = natUnionInftyEmbedding none
⊢ none = none

case refine_1.none.some
m : ℕ
h : natUnionInftyEmbedding none = natUnionInftyEmbedding (Option.some m)
⊢ none = Option.some m

case refine_1.some.none
n : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding none
⊢ Option.some n = none

case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m

Proof state:
⊢ IsClosedEmbedding ⇑natUnionInftyEmbedding

Tactic:
refine .of_continuous_injective_isClosedMap
  natUnionInftyEmbedding.continuous ?_ ?_

Result:
case refine_1

⊢ Function.Injective ⇑natUnionInftyEmbedding

case refine_2

⊢ IsClosedMap ⇑natUnionInftyEmbedding

Proof state:
case refine_1.some.none
n : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding none
⊢ Option.some n = none

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_eq_zero] at h

Result:
case refine_1.some.none
n : ℕ
h : ↑n + 1 = 0
⊢ Option.some n = none

Proof state:
case refine_1.none.some
m : ℕ
h : natUnionInftyEmbedding none = natUnionInftyEmbedding (Option.some m)
⊢ none = Option.some m

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, zero_eq_inv] at h

Result:
case refine_1.none.some
m : ℕ
h : 0 = ↑m + 1
⊢ none = Option.some m

Proof state:
case refine_1.none.some
m : ℕ
h : 0 = ↑m + 1
⊢ none = Option.some m

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, eq_comm, Nat.cast_eq_zero] at h

Result:
case refine_1.none.some
m : ℕ
h : m + 1 = 0
⊢ none = Option.some m

Proof state:
case refine_2

⊢ IsClosedMap ⇑natUnionInftyEmbedding

Tactic:
exact fun _ hC => (hC.isCompact.image natUnionInftyEmbedding.continuous).isClosed

Result:
no goals

Proof state:
case refine_1.some.none
n : ℕ
h : ↑n + 1 = 0
⊢ Option.some n = none

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_eq_zero] at h

Result:
case refine_1.some.none
n : ℕ
h : n + 1 = 0
⊢ Option.some n = none

Proof state:
case refine_1.none.none
h : natUnionInftyEmbedding none = natUnionInftyEmbedding none
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1.some.some
n m : ℕ
h : n = m
⊢ Option.some n = Option.some m

Tactic:
rw [h]

Result:
no goals

Proof state:
case refine_1.none.some
m : ℕ
h : m + 1 = 0
⊢ none = Option.some m

Tactic:
simp at h

Result:
no goals

Proof state:
case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
  Nat.cast_inj] at h

Result:
case refine_1.some.some
n m : ℕ
h : n = m
⊢ Option.some n = Option.some m

Proof state:
case refine_1.some.none
n : ℕ
h : n + 1 = 0
⊢ Option.some n = none

Tactic:
simp at h

Result:
no goals