-- Mathlib/Topology/DiscreteSubset.lean
lemma Continuous.discrete_of_tendsto_cofinite_cocompact [T1Space X] [WeaklyLocallyCompactSpace Y]
    (hf' : Continuous f) (hf : Tendsto f cofinite (cocompact _)) :
    DiscreteTopology X

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
⊢ IsOpen {x}

Tactic:
obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen {x}

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen {x}

Tactic:
obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'

Result:
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
⊢ IsOpen {x}

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
hU₄ : (f ⁻¹' U).Finite
⊢ IsOpen {x}

Tactic:
exact isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
⊢ DiscreteTopology X

Tactic:
refine singletons_open_iff_discrete.mp (fun x ↦ ?_)

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
⊢ IsOpen {x}

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
⊢ IsOpen {x}

Tactic:
have hU₄ : Set.Finite (f⁻¹' U) :=
  Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)

Result:
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace Y
f : X → Y
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
hU₄ : (f ⁻¹' U).Finite
⊢ IsOpen {x}