-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Nobeling.isClosedEmbedding : IsClosedEmbedding (Nobeling.ι S)

Proof state:
case h
S : Profinite
⊢ Continuous (ι S)

Tactic:
dsimp (config := { unfoldPartialApp := true }) [ι]

Result:
case h
S : Profinite
⊢ Continuous fun s C => decide (s ∈ ↑C)

Proof state:
case h.e'_3.h
S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ (fun a => decide (a ∈ ↑C)) ⁻¹' {true} ↔ x ∈ ↑C

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]

Result:
no goals

Proof state:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ False

Tactic:
apply hh.2 ∘ of_decide_eq_true

Result:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true

Proof state:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
⊢ a = b

Tactic:
by_contra hn

Result:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
⊢ False

Proof state:
case h
S : Profinite
⊢ Continuous fun s C => decide (s ∈ ↑C)

Tactic:
refine continuous_pi ?_

Result:
case h
S : Profinite
⊢ ∀ (i : { C // IsClopen C }), Continuous fun a => decide (a ∈ ↑i)

Proof state:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true

Tactic:
dsimp (config := { unfoldPartialApp := true }) [ι] at h

Result:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : (fun C => decide (a ∈ ↑C)) = fun C => decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true

Proof state:
case h
S : Profinite
C : { C // IsClopen C }
⊢ ∀ (y : Bool), IsOpen ((fun a => decide (a ∈ ↑C)) ⁻¹' {y})

Tactic:
rintro ⟨⟩

Result:
case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})

case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a => decide (a ∈ ↑C)) ⁻¹' {true})

Proof state:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
⊢ False

Tactic:
obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn

Result:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ False

Proof state:
case h.e'_3.h
S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})ᶜ ↔ x ∈ ↑C

Tactic:
simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
  decide_eq_false_iff_not, not_not]

Result:
no goals

Proof state:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : (fun C => decide (a ∈ ↑C)) = fun C => decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (a ∈ ↑⟨C, hC⟩) = true

Tactic:
exact decide_eq_true hh.1

Result:
no goals

Proof state:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : (fun C => decide (a ∈ ↑C)) = fun C => decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true

Tactic:
rw [← congr_fun h ⟨C, hC⟩]

Result:
case hf.intro.intro
S : Profinite
a b : ↑S.toTop
h : (fun C => decide (a ∈ ↑C)) = fun C => decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (a ∈ ↑⟨C, hC⟩) = true

Proof state:
case hf
S : Profinite
⊢ Function.Injective (ι S)

Tactic:
intro a b h

Result:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
⊢ a = b

Proof state:
case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})

Tactic:
refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)

Result:
case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})ᶜ

Proof state:
S : Profinite
⊢ IsClosedEmbedding (ι S)

Tactic:
apply Continuous.isClosedEmbedding

Result:
case h
S : Profinite
⊢ Continuous (ι S)

case hf
S : Profinite
⊢ Function.Injective (ι S)

Proof state:
case h
S : Profinite
⊢ ∀ (i : { C // IsClopen C }), Continuous fun a => decide (a ∈ ↑i)

Tactic:
intro C

Result:
case h
S : Profinite
C : { C // IsClopen C }
⊢ Continuous fun a => decide (a ∈ ↑C)

Proof state:
case h.e'_3
S : Profinite
C : { C // IsClopen C }
⊢ (fun a => decide (a ∈ ↑C)) ⁻¹' {true} = ↑C

Tactic:
ext x

Result:
case h.e'_3.h
S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ (fun a => decide (a ∈ ↑C)) ⁻¹' {true} ↔ x ∈ ↑C

Proof state:
case h.e'_3
S : Profinite
C : { C // IsClopen C }
⊢ ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})ᶜ = ↑C

Tactic:
ext x

Result:
case h.e'_3.h
S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})ᶜ ↔ x ∈ ↑C

Proof state:
case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a => decide (a ∈ ↑C)) ⁻¹' {true})

Tactic:
refine IsClopen.isOpen ?_

Result:
case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a => decide (a ∈ ↑C)) ⁻¹' {true})

Proof state:
case h
S : Profinite
C : { C // IsClopen C }
⊢ Continuous fun a => decide (a ∈ ↑C)

Tactic:
rw [← IsLocallyConstant.iff_continuous]

Result:
case h
S : Profinite
C : { C // IsClopen C }
⊢ IsLocallyConstant fun a => decide (a ∈ ↑C)

Proof state:
case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a => decide (a ∈ ↑C)) ⁻¹' {true})

Tactic:
convert C.2

Result:
case h.e'_3
S : Profinite
C : { C // IsClopen C }
⊢ (fun a => decide (a ∈ ↑C)) ⁻¹' {true} = ↑C

Proof state:
case h
S : Profinite
C : { C // IsClopen C }
⊢ IsLocallyConstant fun a => decide (a ∈ ↑C)

Tactic:
refine ((IsLocallyConstant.tfae _).out 0 3).mpr ?_

Result:
case h
S : Profinite
C : { C // IsClopen C }
⊢ ∀ (y : Bool), IsOpen ((fun a => decide (a ∈ ↑C)) ⁻¹' {y})

Proof state:
case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})ᶜ

Tactic:
convert C.2

Result:
case h.e'_3
S : Profinite
C : { C // IsClopen C }
⊢ ((fun a => decide (a ∈ ↑C)) ⁻¹' {false})ᶜ = ↑C