awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
inst : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s
h : Minimal P s
x : α
hxs : x ∈ s
hx : P (s.erase x)
⊢ False

Tactic:
simpa using h.le_of_le hx (erase_subset _ _) hxs

Premises used: Minimal.le_of_le, Finset.erase_subset
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : SupSet β
f : α → β
s : Finset α
⊢ Eq.{u_3 + 1} (α := β) (⨆ x ∈ (↑s : Set α), f x) (⨆ x ∈ s, f x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
a : α
s : α → β
⊢ ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) {a} x), s x = s a

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
o : Option α
f : α → β
⊢ Eq.{u_3 + 1} (α := β) (⨆ x ∈ o.toFinset, f x) (⨆ x ∈ o, f x)

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
⊢ Eq.{u_3 + 1} (α := β) (⨆ x ∈ s ∪ t, f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)

Tactic:
simpa using _root_.iSup_union

Premises used: iSup_union
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
inst_1 : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

Tactic:
simpa using _root_.iSup_insert

Premises used: iSup_insert
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice β
inst_1 : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ Eq.{u_3 + 1} (α := β) (⨆ x ∈ image f s, g x) (⨆ y ∈ s, g (f y))

Tactic:
simpa using iSup_image

Premises used: iSup_image
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
inst_1 : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
rw : update (β := fun (a : α) ↦ β) f x s x ⊔ ⨆ x_1 ∈ t, update (β := fun (a : α) ↦ β) f x s x_1 = s ⊔ ⨆ i ∈ t, f i
⊢ ⨆ i ∈ insert x t, update (β := fun (a : α) ↦ β) f x s i = s ⊔ ⨆ i ∈ t, f i

Tactic:
rw [Finset.iSup_insert]

Premises used: Finset.iSup_insert
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
inst_1 : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ update (β := fun (a : α) ↦ β) f x s x ⊔ ⨆ x_1 ∈ t, update (β := fun (a : α) ↦ β) f x s x_1 = s ⊔ ⨆ i ∈ t, f i

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CompleteLattice β
inst_1 : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → β
⊢ Eq.{u_3 + 1} (α := β) (⨆ y ∈ s.biUnion t, f y) (⨆ x ∈ s, ⨆ y ∈ t x, f y)

Tactic:
simp [@iSup_comm _ α, iSup_and]

Premises used: iSup_comm, iSup_and
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
s : Finset α
t : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ x ∈ (↑s : Set α), t x) (⋃ x ∈ s, t x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
s : Finset α
t : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ x ∈ (↑s : Set α), t x) (⋂ x ∈ s, t x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
a : α
s : α → Set β
⊢ ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) {a} x), s x = s a

Tactic:
iSup_singleton a s

Premises used: Finset.iSup_singleton, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
a : α
s : α → Set β
⊢ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Finset α) {a} x), s x = s a

Tactic:
iInf_singleton a s

Premises used: Set.iInter, Finset.iInf_singleton
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
f : α → β
s : Finset β
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' (↑s : Set β)

Tactic:
Set.biUnion_preimage_singleton f s

Premises used: Set.biUnion_preimage_singleton, SetLike.coe
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
o : Option α
f : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ x ∈ o.toFinset, f x) (⋃ x ∈ o, f x)

Tactic:
iSup_option_toFinset o f

Premises used: Finset.iSup_option_toFinset, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
o : Option α
f : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ x ∈ o.toFinset, f x) (⋂ x ∈ o, f x)

Tactic:
iInf_option_toFinset o f

Premises used: Set.iInter, Finset.iInf_option_toFinset
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
s : Finset α
f : α → Set β
x : α
h : x ∈ s
⊢ f x ≤ ⋃ (_ : x ∈ s), f x

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s t : Finset α
u : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ x ∈ s ∪ t, u x) ((⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x)

Tactic:
iSup_union

Premises used: Set.iUnion, Finset.iSup_union
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s t : Finset α
u : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ x ∈ s ∪ t, u x) ((⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x)

Tactic:
iInf_union

Premises used: Set.iInter, Finset.iInf_union
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
a : α
s : Finset α
t : α → Set β
⊢ ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Tactic:
iSup_insert a s t

Premises used: Finset.iSup_insert, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
a : α
s : Finset α
t : α → Set β
⊢ ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Tactic:
iInf_insert a s t

Premises used: Set.iInter, Finset.iInf_insert
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq α
f : γ → α
g : α → Set β
s : Finset γ
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ x ∈ image f s, g x) (⋃ y ∈ s, g (f y))

Tactic:
iSup_finset_image

Premises used: Finset.iSup_finset_image, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq α
f : γ → α
g : α → Set β
s : Finset γ
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ x ∈ image f s, g x) (⋂ y ∈ s, g (f y))

Tactic:
iInf_finset_image

Premises used: Set.iInter, Finset.iInf_finset_image
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
x : α
t : Finset α
f : α → Set β
s : Set β
hx : x ∉ t
⊢ ⋃ i ∈ insert x t, update (β := fun (a : α) ↦ Set β) f x s i = s ∪ ⋃ i ∈ t, f i

Tactic:
iSup_insert_update f hx

Premises used: Finset.iSup_insert_update, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
x : α
t : Finset α
f : α → Set β
s : Set β
hx : x ∉ t
⊢ ⋂ i ∈ insert x t, update (β := fun (a : α) ↦ Set β) f x s i = s ∩ ⋂ i ∈ t, f i

Tactic:
iInf_insert_update f hx

Premises used: Set.iInter, Finset.iInf_insert_update
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ y ∈ s.biUnion t, f y) (⋃ x ∈ s, ⋃ y ∈ t x, f y)

Tactic:
iSup_biUnion s t f

Premises used: Finset.iSup_biUnion, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ y ∈ s.biUnion t, f y) (⋂ x ∈ s, ⋂ y ∈ t x, f y)

Tactic:
iInf_biUnion s t f

Premises used: Set.iInter, Finset.iInf_biUnion
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
ι : Sort u_3
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l.Subsingleton ↔ ∃ (i : ι), p i ∧ (s i).Subsingleton

Tactic:
h.exists_iff fun _ _ hsub h ↦ h.anti hsub

Premises used: Filter.HasBasis.exists_iff, Set.Subsingleton.anti, Filter.Subsingleton
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l l' : Filter α
hl : l.Subsingleton
hl' : l' ≤ l
⊢ l'.Subsingleton

Tactic:
let ⟨s, hsl, hs⟩ := hl; ⟨s, hl' hsl, hs⟩

Premises used: _private.0.Filter.Subsingleton.anti.match_1, And.intro, Exists.intro, Filter.Subsingleton
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : Subsingleton α
⊢ l.Subsingleton

Tactic:
⟨univ, univ_mem, subsingleton_univ⟩

Premises used: Set.subsingleton_univ, Set.univ, And.intro, Exists.intro, Filter.univ_mem, Filter.Subsingleton
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
β : Type u_2
l : Filter α
hl : l.Subsingleton
f : α → β
⊢ (Filter.map f l).Subsingleton

Tactic:
let ⟨s, hsl, hs⟩ := hl; ⟨f '' s, image_mem_map hsl, hs.image f⟩

Premises used: Set.Subsingleton.image, Filter.map, Filter.image_mem_map, _private.0.Filter.Subsingleton.anti.match_1, And.intro, Exists.intro, Set.image, Filter.Subsingleton
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
β : Type u_2
l : Filter α
hl : l.Subsingleton
l' : Filter β
hl' : l'.Subsingleton
⊢ (l ×ˢ l').Subsingleton

Tactic:
let ⟨s, hsl, hs⟩ := hl; let ⟨t, htl', ht⟩ := hl'; ⟨s ×ˢ t, prod_mem_prod hsl htl', hs.prod ht⟩

Premises used: SProd.sprod, _private.0.Filter.Subsingleton.anti.match_1, And.intro, Exists.intro, Filter.prod_mem_prod, Set.Subsingleton.prod, Filter.Subsingleton
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
a : α
⊢ Filter.Subsingleton (pure a)

Tactic:
⟨{a}, rfl, subsingleton_singleton⟩

Premises used: Set.subsingleton_singleton, And.intro, Exists.intro, Singleton.singleton, Filter.Subsingleton, rfl
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
⊢ Filter.Subsingleton.{u_1} (α := α) ⊥

Tactic:
⟨∅, trivial, subsingleton_empty⟩

Premises used: trivial, Set.subsingleton_empty, And.intro, Exists.intro, EmptyCollection.emptyCollection, Filter.Subsingleton
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
hl : l.Subsingleton
rcases : ∀ (s : Set α) (hsl : s ∈ l) (hs : s.Subsingleton), ∃ (a : α), l = pure a
⊢ ∃ (a : α), l = pure a

Tactic:
rcases hl with ⟨s, hsl, hs⟩
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
s : Set α
hsl : s ∈ l
hs : s.Subsingleton
rcases : ∀ (a : α) (hsl : {a} ∈ l) (hs : Set.Subsingleton (α := α) {a}), ∃ (a : α), l = pure a
⊢ ∃ (a : α), l = pure a

Tactic:
rcases exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨nonempty_of_mem hsl, hs⟩ with ⟨a, rfl⟩

Premises used: Iff.mpr, Filter.nonempty_of_mem, Set.exists_eq_singleton_iff_nonempty_subsingleton, And.intro, rfl
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
a : α
hsl : {a} ∈ l
hs : Set.Subsingleton (α := α) {a}
⊢ ∃ (a : α), l = pure a

Tactic:
⟨a, (NeBot.le_pure_iff ‹_›).1 ?_⟩

Premises used: Filter.NeBot.le_pure_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
a : α
hsl : {a} ∈ l
hs : Set.Subsingleton (α := α) {a}
refine : l ≤ pure a
⊢ ∃ (a : α), l = pure a

Tactic:
refine ⟨a, (NeBot.le_pure_iff ‹_›).1 ?_⟩
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
a : α
hsl : {a} ∈ l
hs : Set.Subsingleton (α := α) {a}
rwa rwa₁ rwa₂ rwa₃ : {a} ∈ l
⊢ l ≤ pure a

Tactic:
rwa [le_pure_iff]

Premises used: Filter.le_pure_iff
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
⊢ l.Subsingleton ↔ l = ⊥ ∨ ∃ (a : α), l = pure a

Tactic:
⟨fun hl ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
refine_1 : ∀ (hl : l.Subsingleton), l = ⊥ ∨ ∃ (a : α), l = pure a
refine_2 : (l = ⊥ ∨ ∃ (a : α), l = pure a) → l.Subsingleton
⊢ l.Subsingleton ↔ l = ⊥ ∨ ∃ (a : α), l = pure a

Tactic:
refine ⟨fun hl ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l = ⊥ ∨ ∃ (a : α), l = pure a

Tactic:
(eq_or_neBot l).imp_right (@Subsingleton.exists_eq_pure _ _ · hl)

Premises used: Filter.Subsingleton.exists_eq_pure, Filter.eq_or_neBot, Or.imp_right
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l = ⊥ ∨ ∃ (a : α), l = pure a

Tactic:
exact (eq_or_neBot l).imp_right (@Subsingleton.exists_eq_pure _ _ · hl)

Premises used: Filter.Subsingleton.exists_eq_pure, Filter.eq_or_neBot, Or.imp_right
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
⊢ Filter.Subsingleton.{u_1} (α := α) ⊥

Tactic:
simp
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
a : α
⊢ Filter.Subsingleton (pure a)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : Nonempty α
inl : Filter.Subsingleton.{u_1} (α := α) ⊥ ↔ ∃ (a : α), LE.le (α := Filter α) ⊥ (pure a)
inr : ∀ (hbot : l.NeBot), l.Subsingleton ↔ ∃ (a : α), l ≤ pure a
⊢ l.Subsingleton ↔ ∃ (a : α), l ≤ pure a

Tactic:
rcases eq_or_neBot l with rfl | hbot

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
inst : Nonempty α
⊢ Filter.Subsingleton.{u_1} (α := α) ⊥ ↔ ∃ (a : α), LE.le (α := Filter α) ⊥ (pure a)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : Nonempty α
hbot : l.NeBot
⊢ l.Subsingleton ↔ ∃ (a : α), l ≤ pure a

Tactic:
simp [subsingleton_iff_bot_or_pure, ← hbot.le_pure_iff, hbot.ne]

Premises used: Filter.NeBot.ne, Filter.subsingleton_iff_bot_or_pure, Filter.NeBot.le_pure_iff
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
inst : Nonempty α
⊢ l.Subsingleton ↔ ∃ (a : α), {a} ∈ l

Tactic:
simp only [subsingleton_iff_exists_le_pure, le_pure_iff]

Premises used: Filter.le_pure_iff, Filter.subsingleton_iff_exists_le_pure
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
l : Filter α
hl : l.Subsingleton
inl : ∀ (hl : Filter.Subsingleton.{u_1} (α := α) ⊥), IsCountablyGenerated.{u_1} (α := α) ⊥
inr : ∀ (x : α) (hl : Filter.Subsingleton (pure x)), IsCountablyGenerated (pure x)
⊢ l.IsCountablyGenerated

Tactic:
rcases subsingleton_iff_bot_or_pure.1 hl with rfl | ⟨x, rfl⟩

Premises used: Filter.subsingleton_iff_bot_or_pure, Iff.mp, rfl
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
hl : Filter.Subsingleton.{u_1} (α := α) ⊥
⊢ IsCountablyGenerated.{u_1} (α := α) ⊥

Tactic:
isCountablyGenerated_bot

Premises used: Filter.isCountablyGenerated_bot
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
hl : Filter.Subsingleton.{u_1} (α := α) ⊥
⊢ IsCountablyGenerated.{u_1} (α := α) ⊥

Tactic:
exact isCountablyGenerated_bot

Premises used: Filter.isCountablyGenerated_bot
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
x : α
hl : Filter.Subsingleton (pure x)
⊢ IsCountablyGenerated (pure x)

Tactic:
isCountablyGenerated_pure x

Premises used: Filter.isCountablyGenerated_pure
-- Module: Mathlib.Order.Filter.Subsingleton
Goal:
α : Type u_1
x : α
hl : Filter.Subsingleton (pure x)
⊢ IsCountablyGenerated (pure x)

Tactic:
exact isCountablyGenerated_pure x

Premises used: Filter.isCountablyGenerated_pure
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
⊢ IsAtomic.{u} (Filter α)

Tactic:
IsAtomic.of_isChain_bounded fun c hc hne hb =>
    ⟨sInf c, (sInf_neBot_of_directed' hne (show IsChain (· ≥ ·) c from hc.symm).directedOn hb).ne,
      fun _ hx => sInf_le hx⟩

Premises used: IsChain.symm, Filter.NeBot.ne, IsChain.directedOn, Filter.sInf_neBot_of_directed', sInf_le, And.intro, IsAtomic.of_isChain_bounded, Exists.intro, InfSet.sInf
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
h : g ≤ (↑f : Filter α)
hne : g.NeBot
⊢ g = (↑f : Filter α)

Tactic:
le_antisymm h <| f.le_of_le g hne h

Premises used: le_antisymm, Ultrafilter.le_of_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
⊢ (↑f : Filter α).NeBot

Tactic:
f.neBot'

Premises used: Ultrafilter.neBot'
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
⊢ IsAtom (↑f : Filter α)

Tactic:
⟨f.neBot.ne, fun _ hgf => by_contra fun hg => hgf.ne <| f.unique hgf.le ⟨hg⟩⟩

Premises used: Filter.NeBot.ne, Ultrafilter.neBot, LT.lt.le, Filter.NeBot.mk, And.intro, IsAtom, by_contra, Ultrafilter.unique, LT.lt.ne
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s : Set α
⊢ s ∈ (↑f : Filter α) ↔ s ∈ f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
h₁ : f.NeBot
h₂ : ∀ (g : Filter α), g.NeBot → g ≤ f → f ≤ g
g : Filter α
neBot' : g.NeBot
le_of_le : ∀ (g_1 : Filter α), g_1.NeBot → g_1 ≤ g → g ≤ g_1
h :
  (↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ : Ultrafilter α } : Filter α) =
    (↑{ toFilter := g, neBot' := neBot', le_of_le := le_of_le } : Filter α)
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ : Ultrafilter α } =
    { toFilter := g, neBot' := neBot', le_of_le := le_of_le }

Tactic:
congr
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f g : Ultrafilter α
h : (↑f : Filter α) ≤ (↑g : Filter α)
⊢ f = g

Tactic:
coe_injective (g.unique h)

Premises used: Ultrafilter.unique, Ultrafilter.coe_injective
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f g : Ultrafilter α
⊢ (↑f : Filter α) ≤ (↑g : Filter α) ↔ f = g

Tactic:
⟨fun h => eq_of_le h, fun h => h ▸ le_rfl⟩

Premises used: le_rfl, Eq.rec, Iff.intro, Ultrafilter.eq_of_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f g : Ultrafilter α
⊢ (↑f : Filter α) = (↑g : Filter α) ↔ f = g

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, Ultrafilter.coe_injective
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f g : Ultrafilter α
h : ∀ (s : Set α), s ∈ f ↔ s ∈ g
⊢ f = g

Tactic:
coe_injective <| Filter.ext h

Premises used: Filter.ext, Ultrafilter.coe_injective
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
hg : ((↑f : Filter α) ⊓ g).NeBot
⊢ (↑f : Filter α) ≤ g

Tactic:
le_of_inf_eq (f.unique inf_le_left hg)

Premises used: le_of_inf_eq, Ultrafilter.unique, inf_le_left
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ (↑f : Filter α)).NeBot
rwa rwa₁ rwa₂ rwa₃ : (g ⊓ (↑f : Filter α)).NeBot
⊢ ((↑f : Filter α) ⊓ g).NeBot

Tactic:
rwa [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
⊢ ((↑f : Filter α) ⊓ g).NeBot ↔ (↑f : Filter α) ≤ g

Tactic:
⟨le_of_inf_neBot f, fun h => (inf_of_le_left h).symm ▸ f.neBot⟩

Premises used: inf_of_le_left, Ultrafilter.neBot, Eq.rec, Ultrafilter.le_of_inf_neBot, Iff.intro, Eq.symm
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
rw : Disjoint (↑f : Filter α) g ↔ ¬((↑f : Filter α) ⊓ g).NeBot
rw₁ : Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ⊓ g ≠ ⊥
rw₂ : Disjoint (↑f : Filter α) g ↔ ¬¬(↑f : Filter α) ⊓ g = ⊥
rw₃ : Disjoint (↑f : Filter α) g ↔ (↑f : Filter α) ⊓ g = ⊥
rw₄ rw₅ : (↑f : Filter α) ⊓ g = ⊥ ↔ (↑f : Filter α) ⊓ g = ⊥
⊢ Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ≤ g

Tactic:
rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]

Premises used: Ultrafilter.inf_neBot_iff, Classical.not_not, disjoint_iff, Filter.neBot_iff, Ne
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h rwa rwa₁ rwa₂ rwa₃ : (↑f : Filter α) ⊓ 𝓟 s = ⊥
⊢ (↑f : Filter α) ⊓ 𝓟 sᶜᶜ = ⊥

Tactic:
rwa [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
p : α → Prop
⊢ (∃ᶠ (x : α) in (↑f : Filter α), p x) ↔ ∀ᶠ (x : α) in (↑f : Filter α), p x

Tactic:
compl_notMem_iff

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Frequently, Ultrafilter.compl_notMem_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s : Set α
rw : sᶜᶜ ∉ f ↔ s ∉ f
rw₁ rw₂ : s ∉ f ↔ s ∉ f
⊢ sᶜ ∈ f ↔ s ∉ f

Tactic:
rw [← compl_notMem_iff, compl_compl]

Premises used: compl_compl, Ultrafilter.compl_notMem_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
s t : Set α
f : Ultrafilter α
⊢ s \ t ∈ f ↔ s ∈ f ∧ t ∉ f

Tactic:
inter_mem_iff.trans <| and_congr Iff.rfl compl_mem_iff_notMem

Premises used: Set.Mem, Set.diff, Iff.rfl, setOf, Iff.trans, Ultrafilter.compl_mem_iff_notMem, Filter.inter_mem_iff, Not, and_congr
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h : ∀ (s : Set α), sᶜ ∉ f ↔ s ∈ f
hf : f = ⊥
⊢ False

Tactic:
simp [hf] at h
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s : Set α
hs : s ∈ f
⊢ s.Nonempty

Tactic:
Filter.nonempty_of_mem hs

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s : Set α
hs : s ∈ f
⊢ s ≠ ∅

Tactic:
(nonempty_of_mem hs).ne_empty

Premises used: Set.Nonempty.ne_empty, Ultrafilter.nonempty_of_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
⊢ ∅ ∉ f

Tactic:
Filter.empty_notMem (f : Filter α)

Premises used: Filter.empty_notMem, Ultrafilter.toFilter
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
u : Ultrafilter α
f g : Filter α
⊢ ¬(↑u : Filter α) ≤ f ⊔ g ↔ ¬((↑u : Filter α) ≤ f ∨ (↑u : Filter α) ≤ g)

Tactic:
simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

Premises used: disjoint_sup_right, not_or, Ultrafilter.disjoint_iff_not_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s t : Set α
⊢ s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

Tactic:
simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]

Premises used: Filter.sup_principal, Filter.le_principal_iff, Ultrafilter.le_sup_iff, Ultrafilter.mem_coe
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
s : Set α
⊢ s ∈ f ∨ sᶜ ∈ f

Tactic:
or_iff_not_imp_left.2 compl_mem_iff_notMem.2

Premises used: Iff.mpr, Classical.or_iff_not_imp_left, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
p : α → Prop
⊢ (∀ᶠ (x : α) in (↑f : Filter α), p x) ∨ ∀ᶠ (x : α) in (↑f : Filter α), ¬p x

Tactic:
f.mem_or_compl_mem { x | p x }

Premises used: Set.Mem, Filter.Eventually, setOf, Ultrafilter.mem_or_compl_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
p q : α → Prop
⊢ (∀ᶠ (x : α) in (↑f : Filter α), p x ∨ q x) ↔ (∀ᶠ (x : α) in (↑f : Filter α), p x) ∨ ∀ᶠ (x : α) in (↑f : Filter α), q x

Tactic:
union_mem_iff

Premises used: Set.union, Set.Mem, Filter.Eventually, setOf, Ultrafilter.union_mem_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
p : α → Prop
⊢ (∀ᶠ (x : α) in (↑f : Filter α), ¬p x) ↔ ¬∀ᶠ (x : α) in (↑f : Filter α), p x

Tactic:
compl_mem_iff_notMem

Premises used: Set.Mem, Filter.Eventually, setOf, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
p q : α → Prop
⊢ (∀ᶠ (x : α) in (↑f : Filter α), p x → q x) ↔ (∀ᶠ (x : α) in (↑f : Filter α), p x) → ∀ᶠ (x : α) in (↑f : Filter α), q x

Tactic:
simp only [imp_iff_not_or, eventually_or, eventually_not]

Premises used: Ultrafilter.eventually_not, Ultrafilter.eventually_or, imp_iff_not_or
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
f : Ultrafilter α
⊢ (↑(map m f) : Filter β) = Filter.map m (↑f : Filter α)

Tactic:
rfl

Premises used: Filter.map, rfl
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
f : Ultrafilter α
s : Set β
⊢ s ∈ map m f ↔ m ⁻¹' s ∈ f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
⊢ map id f = f

Tactic:
coe_injective map_id

Premises used: Filter.map_id, Ultrafilter.coe_injective