awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
f : Filter α
simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₁ : f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₂ : f.lift' powerset = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
simp_rw₃ : f.lift (𝓟 ∘ powerset) = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
simp_rw₄ : Eq.{u_1 + 1} (α := Filter (Set α)) (⨅ s ∈ f, (𝓟 ∘ powerset) s) (⨅ b ∈ f.sets, 𝓟 (𝒫 b))
simp_rw₅ : Eq.{u_1 + 1} (α := Filter (Set α)) (⨅ s ∈ f, 𝓟 (𝒫 s)) (⨅ b ∈ f.sets, 𝓟 (𝒫 b))
⊢ f.smallSets = generate (powerset '' f.sets)

Tactic:
simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]

Premises used: Filter.smallSets, Filter.mem_sets, iInf_image, Filter.lift', Filter.lift, Filter.generate_eq_biInf, Function.comp_apply
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
L : Filter (Set α)
l : Filter α
simp_rw : L.bind 𝓟 ≤ l ↔ l.sets ⊆ powerset ⁻¹' L.sets
⊢ (fun (L : Filter (Set α)) ↦ L.bind 𝓟) L ≤ l ↔ L ≤ l.smallSets

Tactic:
simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff]

Premises used: Filter.smallSets_eq_generate, Filter.le_generate_iff, Set.image_subset_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ l.sets ⊆ powerset ⁻¹' L.sets

Tactic:
rfl
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
ι : Sort u_3
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l.smallSets.HasBasis p fun (i : ι) ↦ 𝒫 s i

Tactic:
h.lift' monotone_powerset

Premises used: Filter.smallSets, setOf, Set.powerset, Filter.HasBasis.lift', Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
⊢ l.smallSets.HasBasis (fun (t : Set α) ↦ t ∈ l) powerset

Tactic:
l.basis_sets.smallSets

Premises used: Filter.basis_sets, Filter.HasBasis.smallSets
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
ι : Sort u_3
l : Filter α
p : ι → Prop
s : ι → Set α
P : Set α → Prop
h₁ : ∀ᶠ (t : Set α) in l.smallSets, P t
h₂ : l.HasBasis p s
⊢ ∃ (i : ι), p i ∧ P (s i)

Tactic:
(h₂.smallSets.eventually_iff.mp h₁).imp fun _i ⟨hpi, hi⟩ ↦ ⟨hpi, hi Subset.rfl⟩

Premises used: Exists.imp, Filter.HasBasis.smallSets, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
ι : Sort u_3
l : Filter α
p : ι → Prop
s : ι → Set α
P : Set α → Prop
h₁ : ∀ (i : ι), p i → P (s i)
h₂ : l.HasBasis p s
⊢ ∃ᶠ (t : Set α) in l.smallSets, P t

Tactic:
h₂.smallSets.frequently_iff.mpr fun _ hi => ⟨_, Subset.rfl, h₁ _ hi⟩

Premises used: Iff.mpr, Filter.HasBasis.frequently_iff, Set.Subset.rfl, And.intro, Filter.HasBasis.smallSets, Exists.intro
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
p : Set α → Prop
h : ∀ᶠ (t : Set α) in l.smallSets, p t
⊢ ∃ s ∈ l, p s

Tactic:
h.exists_mem_basis_of_smallSets l.basis_sets

Premises used: Filter.basis_sets, Filter.Eventually.exists_mem_basis_of_smallSets
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → Set β
⊢ Tendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ (x : α) in la, f x ⊆ t

Tactic:
(hasBasis_smallSets lb).tendsto_right_iff

Premises used: Set.Mem, setOf, Set.powerset, Filter.HasBasis.tendsto_right_iff, Filter.hasBasis_smallSets
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
p : Set α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t ⊆ s, p t

Tactic:
eventually_lift'_iff monotone_powerset

Premises used: Filter.smallSets, Set.Mem, Filter.eventually_lift'_iff, setOf, Set.powerset, Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
⊢ (∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, p s

Tactic:
eventually_smallSets.trans <|
    exists_congr fun s => Iff.rfl.and ⟨fun H => H s Subset.rfl, fun hs _t ht => hp ht hs⟩

Premises used: Iff.rfl, Filter.eventually_smallSets, exists_congr, Set.Subset.rfl, Iff.and, Iff.intro, Iff.trans
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
rw : (∃ s ∈ l, q s) ↔ ∃ (i : ι), p i ∧ q (s i)
rw₁ rw₂ : (∃ (i : ι), p i ∧ q (s i)) ↔ ∃ (i : ι), p i ∧ q (s i)
⊢ (∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ (i : ι), p i ∧ q (s i)

Tactic:
rw [l.eventually_smallSets' hq, hl.exists_iff hq]

Premises used: Filter.HasBasis.exists_iff, Filter.eventually_smallSets'
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
p : Set α → Prop
⊢ (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s ⊆ t, p s

Tactic:
l.hasBasis_smallSets.frequently_iff

Premises used: Set.Mem, setOf, Set.powerset, Filter.HasBasis.frequently_iff, Filter.hasBasis_smallSets
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
⊢ ∃ᶠ (s : Set α) in l.smallSets, s ∈ l

Tactic:
frequently_smallSets.2 fun t ht => ⟨t, Subset.rfl, ht⟩

Premises used: Iff.mpr, Set.Subset.rfl, And.intro, Filter.frequently_smallSets, Exists.intro
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ ⦃s t : Set α⦄, s ⊆ t → (fun (x : Set α) ↦ ¬p x) t → (fun (x : Set α) ↦ ¬p x) s
tauto₅ : ∀ ⦃s t : Set α⦄, s ⊆ t → ¬p t → ¬p s
tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ tauto₁₁ tauto₁₂ tauto₁₃ : ∀ ⦃s t : Set α⦄, s ⊆ t → ¬p t → p s → False
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (fun (x : Set α) ↦ ¬p x) t → (fun (x : Set α) ↦ ¬p x) s

Tactic:
tauto
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
h : (∀ t ∈ l, p t) ↔ ¬∃ s ∈ l, (fun (x : Set α) ↦ ¬p x) s
⊢ (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t

Tactic:
convert! not_iff_not.mpr <| l.eventually_smallSets' (p := (¬p ·)) (by tauto)

Premises used: not_iff_not, Iff.mpr, Filter.eventually_smallSets'
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∀ t ∈ l, p t) ↔ ¬∃ s ∈ l, (fun (x : Set α) ↦ ¬p x) s

Tactic:
simp
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
rw : (∀ t ∈ l, q t) ↔ ∀ (i : ι), p i → q (s i)
rw₁ rw₂ : (∀ (i : ι), p i → q (s i)) ↔ ∀ (i : ι), p i → q (s i)
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)

Tactic:
rw [Filter.frequently_smallSets' hq, hl.forall_iff hq]

Premises used: Filter.frequently_smallSets', Filter.HasBasis.forall_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
rw : (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb
⊢ Tendsto (fun (x : Set α) ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
rw [tendsto_smallSets_iff]

Premises used: Filter.tendsto_smallSets_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb

Tactic:
forall₂_congr fun u hu ↦ ?_

Premises used: forall₂_congr, Filter.Tendsto
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
refine : ∀ (u : Set β) (hu : u ∈ lb), (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb

Tactic:
refine forall₂_congr fun u hu ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
rw : (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la

Tactic:
rw [eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht]

Premises used: Set.image_mono, HasSubset.Subset.trans, Filter.eventually_smallSets'
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la

Tactic:
simp only [image_subset_iff, exists_mem_subset_iff, mem_map]

Premises used: Filter.exists_mem_subset_iff, Set.image_subset_iff, Filter.mem_map
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
ι : Type u_4
inst : Preorder ι
s : ι → Set α
hl : l.HasAntitoneBasis s
⊢ Tendsto s atTop l.smallSets

Tactic:
tendsto_smallSets_iff.2 fun _t ht => hl.eventually_subset ht

Premises used: Iff.mpr, Filter.tendsto_smallSets_iff, Filter.HasAntitoneBasis.eventually_subset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Filter α) smallSets

Tactic:
monotone_lift' monotone_id monotone_const

Premises used: Filter.smallSets, monotone_const, monotone_id, Filter.monotone_lift'
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
rw : Monotone.{u_1, u_1} (α := Set α) powerset
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊥) (pure ∅)

Tactic:
rw [smallSets, lift'_bot, powerset_empty, principal_singleton]

Premises used: Filter.smallSets, Filter.lift'_bot, Set.powerset_empty, Filter.principal_singleton
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Set α) powerset

Tactic:
monotone_powerset

Premises used: Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Set α) powerset

Tactic:
exact monotone_powerset

Premises used: Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter (Set α)) (Filter.lift' ⊤ powerset) ⊤
rw₁ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 (𝒫 univ)) ⊤
rw₂ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 univ) ⊤
rw₃ rw₄ : Eq.{u_1 + 1} (α := Filter (Set α)) ⊤ ⊤
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊤) ⊤

Tactic:
rw [smallSets, lift'_top, powerset_univ, principal_univ]

Premises used: Filter.smallSets, Filter.principal_univ, Set.powerset_univ, Filter.lift'_top
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
s : Set α
⊢ (𝓟 s).smallSets = 𝓟 (𝒫 s)

Tactic:
lift'_principal monotone_powerset

Premises used: Filter.smallSets, Filter.lift'_principal, Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = comap (image f) l.smallSets

Tactic:
(gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_

Premises used: Filter.bind_smallSets_gc, GaloisConnection.u_comm_of_l_comm, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
refine : ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟
⊢ (comap f l).smallSets = comap (image f) l.smallSets

Tactic:
refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_

Premises used: Filter.bind_smallSets_gc, GaloisConnection.u_comm_of_l_comm, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟

Tactic:
simp [Function.comp_def, map_bind, bind_map]

Premises used: Filter.map_bind, Filter.bind_map, Function.comp_def
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = l.lift' (powerset ∘ preimage f)

Tactic:
comap_lift'_eq2 monotone_powerset

Premises used: Filter.smallSets, Filter.comap_lift'_eq2, Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
l : Filter β
f : α → Set β
⊢ comap f l.smallSets = l.lift' (preimage f ∘ powerset)

Tactic:
comap_lift'_eq

Premises used: Filter.smallSets, Filter.comap_lift'_eq
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
ι : Sort u_3
f : ι → Filter α
⊢ (iInf f).smallSets = ⨅ (i : ι), (f i).smallSets

Tactic:
lift'_iInf_of_map_univ (powerset_inter _ _) powerset_univ

Premises used: Filter.smallSets, Set.powerset_univ, Filter.lift'_iInf_of_map_univ, Set.powerset_inter
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l₁ l₂ : Filter α
⊢ (l₁ ⊓ l₂).smallSets = l₁.smallSets ⊓ l₂.smallSets

Tactic:
lift'_inf _ _ powerset_inter

Premises used: Filter.smallSets, Set.Mem, setOf, Filter.lift'_inf, Set.powerset_inter
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
l_1 l' la : Filter α
lb : Filter β
l : Filter α
⊢ l.smallSets.NeBot

Tactic:
(lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty

Premises used: Iff.mpr, Filter.smallSets, Set.powerset_nonempty, Filter.lift'_neBot_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
l_1 l' la : Filter α
lb : Filter β
l : Filter α
refine : Monotone.{u_1, u_1} (α := Set α) powerset
⊢ l.smallSets.NeBot

Tactic:
refine (lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty

Premises used: Iff.mpr, Set.powerset_nonempty, Filter.lift'_neBot_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
l_1 l' la : Filter α
lb : Filter β
l : Filter α
⊢ Monotone.{u_1, u_1} (α := Set α) powerset

Tactic:
monotone_powerset

Premises used: Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
l_1 l' la : Filter α
lb : Filter β
l : Filter α
⊢ Monotone.{u_1, u_1} (α := Set α) powerset

Tactic:
exact monotone_powerset

Premises used: Set.monotone_powerset
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la lb.smallSets
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
rw :
  ∀ (ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1) (hst : ∀ᶠ (x : α) in la, s x ⊆ t x),
    ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t
⊢ Tendsto s la lb.smallSets

Tactic:
rw [tendsto_smallSets_iff] at ht ⊢

Premises used: Filter.tendsto_smallSets_iff
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t

Tactic:
fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)

Premises used: HasSubset.Subset.trans, Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t

Tactic:
exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)

Premises used: HasSubset.Subset.trans, Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s : α → Set β
f : α → β
hs : Tendsto s la lb.smallSets
hf : ∀ᶠ (x : α) in la, f x ∈ s x
⊢ Tendsto f la lb

Tactic:
fun t ht =>
  hf.mp <| (tendsto_smallSets_iff.mp hs t ht).mono fun _ h₁ h₂ => h₁ h₂

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.tendsto_smallSets_iff, Filter.Eventually.mono, Filter.Eventually.mp, Set.preimage, Filter.Tendsto, Iff.mp
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x

Tactic:
simp only [eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x

Tactic:
simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]

Premises used: Filter.eventually_inf, and_imp, Set.mem_inter_iff, and_comm
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
p : α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p

Premises used: inf_top_eq, Filter.eventually_top, Filter.eventually_smallSets_eventually
-- Module: Mathlib.Order.Filter.SmallSets
Goal:
α : Type u_1
l : Filter α
s : Set α
⊢ (∀ᶠ (t : Set α) in l.smallSets, t ⊆ s) ↔ s ∈ l

Tactic:
eventually_smallSets_forall

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.eventually_smallSets_forall, Set.Subset
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage, Filter.Tendsto, Set
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ (x : α) in l₁, f x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
s : Set β
hf : Tendsto f l₁ l₂
h : s ∈ l₂
⊢ ∀ᶠ (x : α) in l₁, f x ∈ s

Tactic:
hf h

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
p : β → Prop
hf : Tendsto f l₁ l₂
h : ∀ᶠ (y : β) in l₂, p y
⊢ ∀ᶠ (x : α) in l₁, p (f x)

Tactic:
hf h

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s

Tactic:
simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, not_eventually]

Premises used: exists_prop, Filter.tendsto_iff_forall_eventually_mem, Filter.not_eventually, Classical.not_forall
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
p : β → Prop
hf : Tendsto f l₁ l₂
h : ∃ᶠ (x : α) in l₁, p (f x)
⊢ ∃ᶠ (y : β) in l₂, p y

Tactic:
mt hf.eventually h

Premises used: mt, Filter.Frequently, Filter.Tendsto.eventually
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
p : α → Prop
q : β → Prop
f : α → β
c : Tendsto f l₁ l₂
w : ∀ (x : α), p x → q (f x)
h : ∃ᶠ (x : α) in l₁, p x
⊢ ∃ᶠ (y : β) in l₂, q y

Tactic:
c.frequently (h.mono w)

Premises used: Filter.Tendsto.frequently, Filter.Frequently.mono
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
⊢ Tendsto f ⊥ l

Tactic:
simp [Tendsto]

Premises used: Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ Tendsto f l ⊥ ↔ l = ⊥

Tactic:
simp [Tendsto]

Premises used: Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
inl : ∀ (h : NeBot.{u_1} (α := α) ⊥ → Tendsto f ⊥ lb), Tendsto f ⊥ lb
inr : ∀ (hla : la.NeBot), Tendsto f la lb
⊢ Tendsto f la lb

Tactic:
rcases eq_or_neBot la with rfl | hla

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
lb : Filter β
h : NeBot.{u_1} (α := α) ⊥ → Tendsto f ⊥ lb
⊢ Tendsto f ⊥ lb

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
lb : Filter β
h : NeBot.{u_1} (α := α) ⊥ → Tendsto f ⊥ lb
⊢ Tendsto f ⊥ lb

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
hla : la.NeBot
⊢ Tendsto f la lb

Tactic:
h hla
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
hla : la.NeBot
⊢ Tendsto f la lb

Tactic:
exact h hla
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ Tendsto f l ⊤

Tactic:
le_top

Premises used: Set.Mem, Filter.Tendsto, le_top
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
rw : map mab (map mba g) ≤ map mab f
⊢ g ≤ map mab f

Tactic:
rw [← @map_id _ g, ← map_congr h₁, ← map_map]

Premises used: Filter.map_congr, Filter.map_map, Filter.map_id
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f

Tactic:
map_mono h₂

Premises used: Filter.map_mono
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f

Tactic:
exact map_mono h₂

Premises used: Filter.map_mono
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
inst : IsEmpty α
f : α → β
la : Filter α
lb : Filter β
⊢ Tendsto f la lb

Tactic:
simp only [filter_eq_bot_of_isEmpty la, tendsto_bot]

Premises used: Filter.tendsto_bot, Filter.filter_eq_bot_of_isEmpty
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
g₁ g₂ : β → α
fa : Filter α
fb : Filter β
hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x
hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y
htendsto : Tendsto g₂ fb fa
⊢ g₁ =ᶠ[fb] g₂

Tactic:
(htendsto.eventually hleft).mp <| hright.mono fun _ hr hl => (congr_arg g₁ hr.symm).trans hl

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, congr_arg, Filter.Eventually.mp, Filter.Tendsto.eventually, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ l₁ ≤ comap f l₂

Tactic:
map_le_iff_le_comap

Premises used: Filter.Tendsto, Filter.map_le_iff_le_comap
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
la₁ la₂ : Filter α
lb₁ lb₂ : Filter β
h₁ : Tendsto f la₁ lb₁
hd : Disjoint lb₁ lb₂
h₂ : Tendsto f la₂ lb₂
⊢ Disjoint la₁ la₂

Tactic:
(disjoint_comap hd).mono h₁.le_comap h₂.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.disjoint_comap, Disjoint.mono
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
rw : map f₁ l₁ ≤ l₂ ↔ Tendsto f₂ l₁ l₂
rw₁ : map f₁ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
rw₂ rw₃ : map f₂ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Tactic:
rw [Tendsto, Tendsto, map_congr hl]

Premises used: Filter.map_congr, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
h : Tendsto f₁ l₁ l₂
⊢ Tendsto f₂ l₁ l₂

Tactic:
(tendsto_congr' hl).1 h

Premises used: Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
h : ∀ (x : α), f₁ x = f₂ x
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Tactic:
tendsto_congr' (univ_mem' h)

Premises used: Filter.tendsto_congr', Filter.univ_mem'
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
h : ∀ (x : α), f₁ x = f₂ x
⊢ Tendsto f₁ l₁ l₂ → Tendsto f₂ l₁ l₂

Tactic:
(tendsto_congr h).1

Premises used: Filter.tendsto_congr, Iff.mp
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
x y : Filter α
⊢ Tendsto id x y ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
x : Filter α
⊢ Tendsto id x x

Tactic:
le_refl x

Premises used: le_refl, Set.Mem, setOf, Set.preimage, Filter.Tendsto