-- Mathlib/Topology/Sequences.lean
theorem tendsto_nhds_iff_seq_tendsto [FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y} :
    Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), b ∉ ib ∧ IsClosed ib → ∃ ia, (a ∉ ia ∧ IsClosed ia) ∧ ∀ x ∈ iaᶜ, f x ∈ ibᶜ

Tactic:
rintro s ⟨hbs, hsc⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
⊢ ∃ ia, (a ∉ ia ∧ IsClosed ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s

Tactic:
exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)

Result:
no goals

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
⊢ a ∈ closure (f ⁻¹' s) → b ∈ s

Tactic:
rw [← seqClosure_eq_closure]

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
⊢ ∃ ia, (a ∉ ia ∧ IsClosed ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ

Tactic:
refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
⊢ a ∈ closure (f ⁻¹' s) → b ∈ s

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Tactic:
refine
  ⟨fun hf u hu => hf.comp hu, fun h =>
    ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), b ∉ ib ∧ IsClosed ib → ∃ ia, (a ∉ ia ∧ IsClosed ia) ∧ ∀ x ∈ iaᶜ, f x ∈ ibᶜ

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s

Tactic:
rintro ⟨u, hus, hu⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s