awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst : Subsingleton β
rw : ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f
rw₁ : ⋂ i ∈ range s, i ∈ f ↔ ∀ (i : β), s i ∈ f
rw₂ : (∀ i ∈ range s, i ∈ f) ↔ ∀ (i : β), s i ∈ f
rw₃ rw₄ : (∀ (i : β), s i ∈ f) ↔ ∀ (i : β), s i ∈ f
⊢ ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f

Tactic:
rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]

Premises used: Set.forall_mem_range, Set.subsingleton_range, Set.sInter_eq_biInter, Set.sInter_range, Filter.biInter_mem'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
⊢ (∃ t ∈ f, t ⊆ s) ↔ s ∈ f

Tactic:
⟨fun ⟨_, ht, ts⟩ => mem_of_superset ht ts, fun hs => ⟨s, hs, Subset.rfl⟩⟩

Premises used: Membership.mem, Set.Subset.rfl, And.intro, Iff.intro, Exists.intro, _private.0.Filter.exists_mem_subset_iff.match_1, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ Monotone (β := Prop) fun (s : Set α) ↦ s ∈ f

Tactic:
fun _ _ hst h =>
  mem_of_superset h hst

Premises used: Monotone, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
mp : ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u
mpr : (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
v : Set α
hvf : v ∈ f
hQv : Q v
⊢ ∃ u ∈ f, P u ∧ Q u

Tactic:
⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩

Premises used: Filter.inter_mem, Set.inter_subset_left, Inter.inter, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
v : Set α
hvf : v ∈ f
hQv : Q v
⊢ ∃ u ∈ f, P u ∧ Q u

Tactic:
exact
      ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
hQu : Q u
⊢ (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Tactic:
⟨⟨u, huf, hPu⟩, u, huf, hQu⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
hQu : Q u
⊢ (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Tactic:
exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ s ∈ 𝓟 s

Tactic:
Subset.rfl

Premises used: Set.Mem, setOf, Set.Subset, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ ∀ᶠ (x : α) in 𝓟 s, x ∈ s

Tactic:
mem_principal_self s

Premises used: Filter.mem_principal_self, Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
simp_rw : (¬∀ x ∈ g, x ∈ f) ↔ ∃ s ∈ g, s ∉ f
simp_rw₁ : (∃ (x : Set α) (_ : x ∈ g), x ∉ f) ↔ ∃ s ∈ g, s ∉ f
⊢ ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

Tactic:
simp_rw [le_def, not_forall, exists_prop]

Premises used: exists_prop, Classical.not_forall, Filter.le_def
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ s
⊢ U ∈ generate s

Tactic:
GenerateSets.basic h

Premises used: Set.Mem, setOf, Filter.GenerateSets.basic
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Set α)
f : Filter α
h : s ⊆ f.sets
x : Set α
hu : x ∈ generate s
s_1 t : Set α
h_1 : GenerateSets s s_1
hxy : s_1 ⊆ t
⊢ s_1 ∈ f → t ∈ f

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ generate {s} = 𝓟 s

Tactic:
le_antisymm (fun _t ht ↦ mem_of_superset (mem_generate_of_mem <| mem_singleton _) ht) <|
    le_generate_iff.2 <| singleton_subset_iff.2 Subset.rfl

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, Filter.le_generate_iff, Filter.mem_generate_of_mem, le_antisymm, Set.Subset.rfl, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Set α)
hs : (generate s).sets = s
⊢ Filter.mkOfClosure s hs = generate s

Tactic:
Filter.ext fun u =>
    show u ∈ (Filter.mkOfClosure s hs).sets ↔ u ∈ (generate s).sets from hs.symm ▸ Iff.rfl

Premises used: Iff.rfl, Filter.ext, Eq.rec, Eq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s : Set α
⊢ s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s : Set α
h : s ∈ f
⊢ s ∈ f ⊓ g

Tactic:
⟨s, h, univ, univ_mem, (inter_univ s).symm⟩

Premises used: Set.Mem, Set.univ, Set.inter_univ, setOf, And.intro, Exists.intro, Filter.univ_mem, Eq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s : Set α
h : s ∈ g
⊢ s ∈ f ⊓ g

Tactic:
⟨univ, univ_mem, s, h, (univ_inter s).symm⟩

Premises used: Set.Mem, Set.univ, setOf, Set.univ_inter, And.intro, Exists.intro, Filter.univ_mem, Eq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s t : Set α
hs : s ∈ f
ht : t ∈ g
⊢ s ∩ t ∈ f ⊓ g

Tactic:
⟨s, hs, t, ht, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s t u : Set α
hs : s ∈ f
ht : t ∈ g
h : s ∩ t ⊆ u
⊢ u ∈ f ⊓ g

Tactic:
mem_of_superset (inter_mem_inf hs ht) h

Premises used: Filter.inter_mem_inf, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s : Set α
⊢ s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s

Tactic:
⟨fun ⟨t₁, h₁, t₂, h₂, Eq⟩ => ⟨t₁, h₁, t₂, h₂, Eq ▸ Subset.rfl⟩, fun ⟨_, h₁, _, h₂, sub⟩ =>
    mem_inf_of_inter h₁ h₂ sub⟩

Premises used: Filter.mem_inf_of_inter, Membership.mem, Exists, Eq.rec, HasSubset.Subset, _private.0.Filter.mem_inf_iff_superset.match_1, Inter.inter, And, Set.Subset.rfl, And.intro, Iff.intro, Exists.intro, _private.0.Filter.mem_inf_iff_superset.match_2, Min.min
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s : Set α
⊢ s ∈ f \ g ↔ ∀ t ∈ g, s ∪ t ∈ f

Tactic:
⟨fun hs _ ht => hs (mem_of_superset ht subset_union_right) subset_union_left,
    fun h t htg hst => union_eq_right.2 hst ▸ h t htg⟩

Premises used: Iff.mpr, Set.subset_union_right, Eq.rec, Set.subset_union_left, Set.union_eq_right, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Filter α)
⊢ IsLUB s (sSup s)

Tactic:
⟨fun _ h₁ _ h₂ ↦ h₂ h₁, fun _ h₁ _ h₂ _ h₃ ↦ h₁ h₃ h₂⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Filter α)
⊢ IsGLB s (sInf s)

Tactic:
isLUB_lowerBounds.mp (Filter.sSup_lowerBounds _ ▸ Filter.isLUB_sSup _)

Premises used: isLUB_lowerBounds, Filter.sSup_lowerBounds, Eq.rec, Iff.mp, Filter.isLUB_sSup
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
hf : f.NeBot
⊢ f ≠ ⊥

Tactic:
hf.ne'

Premises used: Filter.NeBot.ne'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ ¬f.NeBot ↔ f = ⊥

Tactic:
neBot_iff.not_left

Premises used: Filter.neBot_iff, Iff.not_left
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
hf : f.NeBot
hg : f ≤ g
⊢ g.NeBot

Tactic:
⟨ne_bot_of_le_ne_bot hf.1 hg⟩

Premises used: ne_bot_of_le_ne_bot, Filter.NeBot.mk, Filter.NeBot.ne'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
hf : f.NeBot
hg : f ≤ g
⊢ g.NeBot

Tactic:
hf.mono hg

Premises used: Filter.NeBot.mono
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ (f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot

Tactic:
simp only [neBot_iff, not_and_or, Ne, sup_eq_bot_iff]

Premises used: Filter.neBot_iff, Ne, sup_eq_bot_iff, not_and_or
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
rw : ¬f = ⊥ ↔ f.NeBot
rw₁ rw₂ : ¬f = ⊥ ↔ f ≠ ⊥
⊢ ¬Disjoint f f ↔ f.NeBot

Tactic:
rw [disjoint_self, neBot_iff]

Premises used: Filter.neBot_iff, disjoint_self
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set (Set α)) (sets ⊥) univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ f = ⊥ ∨ f.NeBot

Tactic:
(eq_or_ne f ⊥).imp_right NeBot.mk

Premises used: Filter.NeBot.mk, Bot.bot, eq_or_ne, Or.imp_right
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ (f ⊔ g).sets = f.sets ∩ g.sets

Tactic:
(giGenerate α).gc.u_inf

Premises used: Filter.giGenerate, GaloisConnection.u_inf, GaloisInsertion.gc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Filter α)
⊢ (sSup s).sets = ⋂ f ∈ s, f.sets

Tactic:
(giGenerate α).gc.u_sInf

Premises used: Set.Mem, Set.iInter, Filter.giGenerate, OrderDual, GaloisConnection.u_sInf, GaloisInsertion.gc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ (iSup f).sets = ⋂ (i : ι), (f i).sets

Tactic:
(giGenerate α).gc.u_iInf

Premises used: Set.iInter, GaloisConnection.u_iInf, Filter.giGenerate, OrderDual, GaloisInsertion.gc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Filter α) (generate ∅) ⊤

Tactic:
(giGenerate α).gc.l_bot

Premises used: Filter.giGenerate, GaloisConnection.l_bot, OrderDual, GaloisInsertion.gc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Filter α) (generate univ) ⊥

Tactic:
bot_unique fun _ _ => GenerateSets.basic (mem_univ _)

Premises used: Set.mem_univ, bot_unique, Filter.GenerateSets.basic
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set (Set α)
⊢ generate (s ∪ t) = generate s ⊓ generate t

Tactic:
(giGenerate α).gc.l_sup

Premises used: Filter.giGenerate, OrderDual, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
s : ι → Set (Set α)
⊢ Eq.{u + 1} (α := Filter α) (generate (⋃ (i : ι), s i)) (⨅ (i : ι), generate (s i))

Tactic:
(giGenerate α).gc.l_iSup

Premises used: iInf, Filter.giGenerate, GaloisConnection.l_iSup, OrderDual, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s : Set α
⊢ s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s t : Set α
hs : s ∈ f
ht : t ∈ g
⊢ s ∪ t ∈ f ⊔ g

Tactic:
⟨mem_of_superset hs subset_union_left, mem_of_superset ht subset_union_right⟩

Premises used: Set.Mem, setOf, Set.subset_union_right, Set.subset_union_left, And.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
x : Set α
f : ι → Filter α
⊢ x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp only [← Filter.mem_sets, iSup_sets_eq, mem_iInter]

Premises used: Filter.mem_sets, Set.mem_iInter, Filter.iSup_sets_eq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ NeBot.{u} (α := α) (⨆ (i : ι), f i) ↔ ∃ (i : ι), (f i).NeBot

Tactic:
simp [neBot_iff]

Premises used: Filter.neBot_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
s : ι → Filter α
x : Filter α
⊢ x ≤ iInf s ↔ x ≤ generate (⋃ (i : ι), (s i).sets)

Tactic:
simp [le_generate_iff]

Premises used: Filter.le_generate_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
i : ι
s : Set α
hs : s ∈ f i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s

Tactic:
iInf_le f i hs

Premises used: Set.Mem, setOf, iInf_le
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
i : ι
s : Set α
hs : s ∈ f i
⊢ p s

Tactic:
simpa using ins hs uni
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
have : ∀ (p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s), p s
⊢ p s

Tactic:
have p_of_f : ∀ i, ∀ s ∈ f i, p s := fun i s hs ↦ by simpa using ins hs uni
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
⊢ Monotone q

Tactic:
have q_mono : Monotone q := fun a b hab ha ↦
    ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
right : ∀ (t' : Set α), s ∩ t ⊆ t' → p t'
⊢ q (s ∩ t)

Tactic:
use inter_mem (mem_iInf_of_mem _ hs) ht.1

Premises used: Filter.inter_mem, Filter.mem_iInf_of_mem, And.left
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
rwa : ∀ (hu : u ∪ s ∩ t = u), u = (u ∪ s) ∩ (u ∪ t)
rwa₁ : ∀ (hu : (u ∪ s) ∩ (u ∪ t) = u), u = (u ∪ s) ∩ (u ∪ t)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hu : u = (u ∪ s) ∩ (u ∪ t)), u = (u ∪ s) ∩ (u ∪ t)
⊢ u = (u ∪ s) ∩ (u ∪ t)

Tactic:
rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu

Premises used: Set.union_eq_left, eq_comm, Set.union_inter_distrib_left
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
right : ∀ (this : u = (u ∪ s) ∩ (u ∪ t)), p u
⊢ p u

Tactic:
have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
right : p ((u ∪ s) ∩ (u ∪ t))
⊢ p u

Tactic:
rw [this]
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p ((u ∪ s) ∩ (u ∪ t))

Tactic:
ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)

Premises used: Set.subset_union_right, And.right, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p ((u ∪ s) ∩ (u ∪ t))

Tactic:
exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)

Premises used: Set.subset_union_right, And.right, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
⊢ ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)

Tactic:
have A : ∀ i, ∀ s ∈ f i, ∀ t, q t → q (s ∩ t) := fun i s hs t ht ↦ by
    use inter_mem (mem_iInf_of_mem _ hs) ht.1
    intro u hu
    have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
    rw [this]
    exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∀ (t : Set α), q t → q (s ∩ t)} univ

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t_1 : Set α
hqs : q s
hqt : q t_1
x y : Set α
ha : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ (t : Set α), q t → q (s ∩ t)} x
hb : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ (t : Set α), q t → q (s ∩ t)} y
t : Set α
ht : q t
⊢ q (x ∩ y ∩ t)

Tactic:
simpa [inter_assoc] using ha _ (hb _ ht)

Premises used: Set.inter_assoc
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
let : q (s ∩ t)
⊢ q (s ∩ t)

Tactic:
let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
𝓕 : Filter α :=
  { sets := {s : Set α | ∀ (t : Set α), q t → q (s ∩ t)}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ q (s ∩ t)

Tactic:
(le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt

Premises used: Iff.mpr, le_iInf_iff, And.left
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
𝓕 : Filter α :=
  { sets := {s : Set α | ∀ (t : Set α), q t → q (s ∩ t)}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ q (s ∩ t)

Tactic:
exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt

Premises used: Iff.mpr, le_iInf_iff, And.left
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
⊢ ∀ (s t : Set α), q s → q t → q (s ∩ t)

Tactic:
have B : ∀ s t, q s → q t → q (s ∩ t) := fun s t hqs hqt ↦ by
    let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }
    exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
⊢ ∀ (i : ι), ∀ s ∈ f i, q s

Tactic:
have C : ∀ i, ∀ s ∈ f i, q s := fun i s hs ↦
    ⟨mem_iInf_of_mem _ hs, fun t hst ↦ p_of_f _ _ (mem_of_superset hs hst)⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
⊢ Membership.mem (γ := Set (Set α)) {t : Set α | q t} univ

Tactic:
simpa [q] using uni
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
𝓖 : Filter α := { sets := {t : Set α | q t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ 𝓖 ≤ iInf f

Tactic:
have : 𝓖 ≤ iInf f := le_iInf_iff.mpr C
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
𝓖 : Filter α := { sets := {t : Set α | q t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
this : 𝓖 ≤ iInf f
⊢ p s

Tactic:
(this hs).2 s subset_rfl

Premises used: And.right, subset_rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
𝓖 : Filter α := { sets := {t : Set α | q t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
this : 𝓖 ≤ iInf f
⊢ p s

Tactic:
exact (this hs).2 s subset_rfl

Premises used: And.right, subset_rfl