mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x✝ : Set α
⊢ ∀ᶠ (x : α) in f, x ∈ x✝ → p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
a✝ : α
pa : a✝ ∈ univ → p a✝
⊢ a✝ ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) S
ne : S.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ S, 𝓟 (s i) ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
⊢ ∀ᶠ (x : α) in f, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : α → β
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.map f l ↔ ∃ i, p i ∧ f '' s i ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∃ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ x, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝ : ∀ (j : ι), Nonempty (α j)
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ f.NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ x ∈ f ⁻¹' s i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ map m f = ⊥ → f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x ↦ p x) x
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : f = ⊥
⊢ map m f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.comap f l ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
P : α → Prop
⊢ (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
⊢ (¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ⊥ = map m f ↔ f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
⊢ (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
⊢ (map f F).NeBot ↔ F.NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
⊢ (∃ᶠ (x : α) in f, True) ↔ f.NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
⊢ ¬∃ᶠ (x : α) in f, False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
this : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
la : Filter α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
sa : Set α
h : lb.HasBasis pb sb
⊢ (𝓟 sa ×ˢ lb).HasBasis pb fun x ↦ sa ×ˢ sb x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
sb : Set β
⊢ (la ×ˢ 𝓟 sb).HasBasis pa fun x ↦ sa x ×ˢ sb

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
h : lb.HasBasis pb sb
⊢ (⊤ ×ˢ lb).HasBasis pb fun x ↦ univ ×ˢ sb x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
⊢ (la ×ˢ ⊤).HasBasis pa fun x ↦ sa x ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
⊢ ¬∃ᶠ (x : α) in ⊥, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
⊢ ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → Filter α
m : α → β
hf : Directed (fun x1 x2 ↦ x1 ≥ x2) f
inst✝ : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ map m (f i) ≤ 𝓟 s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
⊢ (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
a : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ x ∈ a, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f g : Filter α
⊢ (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {x | p x}
ne : ∃ i, p i
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
fs : Set (Filter α)
⊢ (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
fs : β → Filter α
⊢ (∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
f g : α → β
⊢ f =ᶠ[⊤] g ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set α
l : Filter α
⊢ s =ᶠ[l] univ ↔ s ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
⊢ ∀ (x : α), g x = g' x → f x = f' x → (fun x ↦ (f x, g x)) x = (fun x ↦ (f' x, g' x)) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
l : Filter α
inst✝ : Mul β
f₁ f₂ f₃ : α → β
h : f₁ =ᶠ[l] f₂
⊢ f₃ =ᶠ[l] f₃

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set α
l : Filter α
⊢ (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ ∅) ↔ ∀ᶠ (x : α) in l, x ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
hm : Injective m
f₁ f₂ : Filter α
⊢ Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ map (⇑e) (map (⇑e.symm) f) = map (⇑e) (comap (⇑e) f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f - g =ᶠ[l] 0
⊢ f =ᶠ[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LE β
l : Filter α
f f' g g' : α → β
H✝ : f ≤ᶠ[l] g
hf✝ : f =ᶠ[l] f'
hg✝ : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
⊢ f' x ≤ g' x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder β
l : Filter α
f g : α → β
⊢ f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ t ∈ l ⊓ 𝓟 s ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ (la ×ˢ lb).HasBasis p fun i ↦ sa i ×ˢ sb i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ W) = f '' f ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) = map f F ⊓ G

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
la : Filter α
r : α → α → Prop
⊢ (∃ t ∈ la, t ×ˢ t ⊆ {x | (fun x ↦ r x.1 x.2) x}) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (comap f G ⊓ F) = G ⊓ map f F

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
⊢ f ⊔ g ≤ᶠ[l] h

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint F (comap f G) ↔ Disjoint (map f F) G

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint (comap f G) F ↔ Disjoint G (map f F)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u_1
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
s : Set α
⊢ sᶜ ∈ comk p he hmono hunion ↔ p s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (comap m f ⊓ 𝓟 s).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 𝓟 s = map Subtype.val ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
F : Filter α
s : Set α
⊢ F ⊓ 𝓟 s = ⊥ ↔ comap Subtype.val F = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ map f (generate U) ≤ generate ((fun x ↦ f ⁻¹' x) ⁻¹' U)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ generate ((fun x ↦ f ⁻¹' x) '' U) ≤ comap f (generate U)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
f : Filter α
a : α
⊢ f ≤ pure a ↔ {a} ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
s : Set β
⊢ s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ atTop = pure ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
m : α → β
f : Filter α
⊢ Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g : α → β
f : Filter α
⊢ (pure g).seq f = map g f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
⊢ f.seq (pure a) = map (fun g ↦ g a) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ h.seq (g.seq x) = ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (map Prod.mk f).seq g = (map (fun b a ↦ (a, b)) g).seq f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ f₁.bind g₁ ≤ f₂.bind g₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : α → Filter β
s✝ s : Set β
⊢ (s ∈ f.bind fun x ↦ g x ⊓ 𝓟 s✝) ↔ s ∈ f.bind g ⊓ 𝓟 s✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
H : Filter β
hHG : H ≤ G
⊢ map m ((fun x ↦ F ⊓ comap m x) H) = H

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : α → β
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s

Tactic:
by

Goal state after: