-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem tendsto_iff_seq_tendsto {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
    Tendsto f k l ↔ ∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
⊢ False

Tactic:
rcases (hx.2.and (h hs)).exists with ⟨N, hnmem, hmem⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnmem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
refine ⟨x, hx.1, fun h => ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
⊢ False

Proof state:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot

Tactic:
simpa [neBot_iff, inf_principal_eq_bot]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k

Tactic:
contrapose! H

Result:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]

Result:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnmem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False

Tactic:
exact hnmem hmem

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩

Result:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
rw [tendsto_inf, tendsto_principal] at hx

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l