-- Mathlib/Topology/Sequences.lean
theorem Topology.IsInducing.frechetUrysohnSpace [FrechetUrysohnSpace Y] {f : X → Y}
    (hf : IsInducing f) : FrechetUrysohnSpace X

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
⊢ x ∈ seqClosure s

Tactic:
rcases hx with ⟨u, hus, hu⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hus : ∀ (n : ℕ), u n ∈ f '' s
hu : Tendsto u atTop (𝓝 (f x))
⊢ x ∈ seqClosure s

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ x ∈ seqClosure s

Tactic:
refine ⟨v, hv, ?_⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ Tendsto v atTop (𝓝 x)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure s
⊢ x ∈ seqClosure s

Tactic:
rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
⊢ x ∈ seqClosure s

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hx ↦ ?_⟩

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure s
⊢ x ∈ seqClosure s

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ Tendsto v atTop (𝓝 x)

Tactic:
simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hus : ∀ (n : ℕ), u n ∈ f '' s
hu : Tendsto u atTop (𝓝 (f x))
⊢ x ∈ seqClosure s

Tactic:
choose v hv hvu using hus

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ x ∈ seqClosure s