-- Mathlib/Topology/Basic.lean
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : α → X} {l : Filter α} {s : Set α}
    (h : ∀ a ∉ s, f a = x) : Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
replace h : 𝓟 sᶜ ≤ comap f (𝓝 x) := by
  rintro U ⟨t, ht, htU⟩ x hx
  have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
  exact htU this

Result:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Proof state:
case intro.intro
X : Type u
α : Type u_1
x✝ : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
⊢ x ∈ U

Tactic:
have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht

Result:
case intro.intro
X : Type u
α : Type u_1
x✝ : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
refine ⟨fun h' => ?_, le_trans inf_le_left⟩

Result:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff]
  at this

Result:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
have := sup_le h' h

Result:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ 𝓟 sᶜ ≤ comap f (𝓝 x)

Tactic:
rintro U ⟨t, ht, htU⟩ x hx

Result:
case intro.intro
X : Type u
α : Type u_1
x✝ : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
⊢ x ∈ U

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)

Tactic:
rw [tendsto_iff_comap, tendsto_iff_comap]

Result:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Proof state:
case intro.intro
X : Type u
α : Type u_1
x✝ : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U

Tactic:
exact htU this

Result:
no goals

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
exact this.1

Result:
no goals