awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #(↑S : Type u) < c
h : ∀ s ∈ S, CardinalGenerateSets (c := c) g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), #(↑(T s a) : Type u) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ t' ∈ S, ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ t'

Tactic:
apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Premises used: Set.subset_iUnion₂, subset_trans, Set.sInter_subset_sInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
mp : ∀ {s : Set α} (hs : s ∈ g), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
mp₁ : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ Set.univ
mp₂ :
  ∀ {s t : Set α},
    CardinalGenerateSets (c := c) g s →
      s ⊆ t → ∀ (ih : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ t
mp₃ :
  ∀ {S : Set (Set α)} (Sct : #(↑S : Type u) < c),
    (∀ s ∈ S, CardinalGenerateSets (c := c) g s) →
      ∀ (ih : ∀ s ∈ S, ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s), ∃ S_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s

Tactic:
induction h with
    | @basic s hs =>
      refine ⟨{s}, singleton_subset_iff.mpr hs, ?_⟩
      simpa [subset_refl] using IsRegular.nat_lt hreg 1
    | univ =>
      exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩
    | superset _ _ ih => exact Exists.imp (by tauto) ih
    | @sInter S Sct _ ih =>
      choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa,
        (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
      apply subset_sInter
      apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Premises used: subset_refl, Set.subset_sInter, Cardinal.IsRegular.nat_lt, OfNat.ofNat, Set.sInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
mpr : ∀ (S : Set (Set α)) (Sg : S ⊆ g) (Sct : #(↑S : Type u) < c) (hS : ⋂₀ S ⊆ s), s ∈ cardinalGenerate g ⋯
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
rcases h with ⟨S, Sg, Sct, hS⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #(↑S : Type u) < c
hS : ⋂₀ S ⊆ s
⊢ CardinalInterFilter (cardinalGenerate g ⋯) c

Tactic:
have : CardinalInterFilter (cardinalGenerate g (IsRegular.nat_lt hreg 2)) c :=
    cardinalInter_ofCardinalGenerate _ _
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #(↑S : Type u) < c
hS : ⋂₀ S ⊆ s
this : CardinalInterFilter (cardinalGenerate g ⋯) c
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
mem_of_superset ((cardinal_sInter_mem Sct).mpr
    (fun s H => CardinalGenerateSets.basic (Sg H))) hS

Premises used: Iff.mpr, cardinal_sInter_mem, Filter.CardinalGenerateSets.basic, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #(↑S : Type u) < c
hS : ⋂₀ S ⊆ s
this : CardinalInterFilter (cardinalGenerate g ⋯) c
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
exact mem_of_superset ((cardinal_sInter_mem Sct).mpr
    (fun s H => CardinalGenerateSets.basic (Sg H))) hS

Premises used: Iff.mpr, cardinal_sInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
mp : f ≤ cardinalGenerate g hc → g ⊆ f.sets
mpr : g ⊆ f.sets → f ≤ cardinalGenerate g hc
⊢ f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : f ≤ cardinalGenerate g hc
⊢ g ⊆ f.sets

Tactic:
subset_trans (fun s => CardinalGenerateSets.basic) h

Premises used: subset_trans, Filter.CardinalGenerateSets.basic
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : f ≤ cardinalGenerate g hc
⊢ g ⊆ f.sets

Tactic:
exact subset_trans (fun s => CardinalGenerateSets.basic) h

Premises used: subset_trans
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s_1 : Set α
hs : s_1 ∈ g
⊢ s_1 ∈ f

Tactic:
h hs
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s_1 : Set α
hs : s_1 ∈ g
⊢ s_1 ∈ f

Tactic:
exact h hs
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
⊢ Set.univ ∈ f

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
⊢ Set.univ ∈ f

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s_1 t : Set α
h_1 : CardinalGenerateSets (c := c) g s_1
st : s_1 ⊆ t
ih : s_1 ∈ f
⊢ t ∈ f

Tactic:
mem_of_superset ih st

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s_1 t : Set α
h_1 : CardinalGenerateSets (c := c) g s_1
st : s_1 ⊆ t
ih : s_1 ∈ f
⊢ t ∈ f

Tactic:
exact mem_of_superset ih st

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : #(↑S : Type u) < c
h_1 : ∀ s ∈ S, CardinalGenerateSets (c := c) g s
ih : ∀ s ∈ S, s ∈ f
⊢ ⋂₀ S ∈ f

Tactic:
(cardinal_sInter_mem Sct).mpr ih

Premises used: Iff.mpr, cardinal_sInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : #(↑S : Type u) < c
h_1 : ∀ s ∈ S, CardinalGenerateSets (c := c) g s
ih : ∀ s ∈ S, s ∈ f
⊢ ⋂₀ S ∈ f

Tactic:
exact (cardinal_sInter_mem Sct).mpr ih

Premises used: Iff.mpr, cardinal_sInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
mpr : ∀ {s : Set α} (hs : s ∈ g), s ∈ f
mpr₁ : Set.univ ∈ f
mpr₂ : ∀ {s t : Set α}, CardinalGenerateSets (c := c) g s → ∀ (st : s ⊆ t) (ih : s ∈ f), t ∈ f
mpr₃ :
  ∀ {S : Set (Set α)} (Sct : #(↑S : Type u) < c),
    (∀ s ∈ S, CardinalGenerateSets (c := c) g s) → ∀ (ih : ∀ s ∈ S, s ∈ f), ⋂₀ S ∈ f
⊢ s ∈ f

Tactic:
induction hs with
  | basic hs => exact h hs
  | univ => exact univ_mem
  | superset _ st ih => exact mem_of_superset ih st
  | sInter Sct _ ih => exact (cardinal_sInter_mem Sct).mpr ih

Premises used: Filter.univ_mem, Set.sInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ IsGreatest {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)

Tactic:
⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩

Premises used: IsGreatest, And.intro, Filter.cardinalInter_ofCardinalGenerate, Filter.CardinalGenerateSets.basic
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
refine :
  Membership.mem (γ := Set (Filter α)) (upperBounds {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets})
    (cardinalGenerate g hc)
⊢ IsGreatest {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)

Tactic:
refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
f : Filter α
fct : CardinalInterFilter f c
hf rwa rwa₁ rwa₂ rwa₃ : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc

Tactic:
rwa [le_cardinalGenerate_iff_of_cardinalInterFilter]

Premises used: Filter.le_cardinalGenerate_iff_of_cardinalInterFilter
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
hUnion :
  ∀ (S : Set (Set α)),
    #(↑S : Type u) < c →
      (∀ s ∈ S, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s) →
        Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} (⋃₀ S)
hmono :
  ∀ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} t →
      ∀ s ⊆ t, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s
⊢ Filter α

Tactic:
apply ofCardinalUnion {s | Cardinal.mk s < c} (natCast_lt_aleph0.trans_le hreg.aleph0_le)

Premises used: setOf, Cardinal.mk, Cardinal.IsRegular.aleph0_le, Set.Elem, Cardinal.natCast_lt_aleph0, Filter.ofCardinalUnion, LT.lt.trans_le, LT.lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
⊢ ∀ (S : Set (Set α)),
    #(↑S : Type u) < c →
      (∀ s ∈ S, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s) →
        Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} (⋃₀ S)

Tactic:
fun s hS hSc ↦ lt_of_le_of_lt (mk_sUnion_le _) <| mul_lt_of_lt hreg.aleph0_le hS ?_

Premises used: Cardinal.mk_sUnion_le, lt_of_le_of_lt, Set.Mem, setOf, Cardinal.IsRegular.aleph0_le, Cardinal.mul_lt_of_lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
hUnion :
  ∀ (s : Set (Set α)) (hS : #(↑s : Type u) < c)
    (hSc : ∀ s_1 ∈ s, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s_1),
    ⨆ (s_1 : (↑s : Type u)), #(↑(↑s_1 : Set α) : Type u) < c
⊢ ∀ (S : Set (Set α)),
    #(↑S : Type u) < c →
      (∀ s ∈ S, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s) →
        Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} (⋃₀ S)

Tactic:
refine fun s hS hSc ↦ lt_of_le_of_lt (mk_sUnion_le _) <| mul_lt_of_lt hreg.aleph0_le hS ?_

Premises used: Cardinal.mk_sUnion_le, lt_of_le_of_lt, Cardinal.IsRegular.aleph0_le, Cardinal.mul_lt_of_lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
s : Set (Set α)
hS : #(↑s : Type u) < c
hSc : ∀ s_1 ∈ s, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s_1
apply : #(↑s : Type u) < c.ord.cof
⊢ ⨆ (s_1 : (↑s : Type u)), #(↑(↑s_1 : Set α) : Type u) < c

Tactic:
apply iSup_lt_of_lt_cof_ord _ fun i ↦ hSc i.1 i.2

Premises used: Cardinal.iSup_lt_of_lt_cof_ord
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
s : Set (Set α)
hS : #(↑s : Type u) < c
hSc : ∀ s_1 ∈ s, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s_1
rwa rwa₁ rwa₂ rwa₃ : #(↑s : Type u) < c
⊢ #(↑s : Type u) < c.ord.cof

Tactic:
rwa [hreg.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
⊢ ∀ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} t →
      ∀ s ⊆ t, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s

Tactic:
fun _ hSc _ ht ↦ lt_of_le_of_lt (mk_le_mk_of_subset ht) hSc

Premises used: lt_of_le_of_lt, Set.Mem, setOf, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
⊢ ∀ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} t →
      ∀ s ⊆ t, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s

Tactic:
exact fun _ hSc _ ht ↦ lt_of_le_of_lt (mk_le_mk_of_subset ht) hSc

Premises used: lt_of_le_of_lt, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
⊢ s ∈ cocardinal α hreg ↔ #(↑sᶜ : Type u) < c

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
⊢ cocardinal α isRegular_aleph0 = cofinite

Tactic:
aesop
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
grw : #(↑(compl '' S) : Type u) * ⨆ (s : (↑(compl '' S) : Type u)), #(↑(↑s : Set α) : Type u) < c
⊢ ⋂₀ S ∈ cocardinal α hreg

Tactic:
grw [mem_cocardinal, Set.compl_sInter, mk_sUnion_le]

Premises used: Cardinal.mk_sUnion_le, Set.compl_sInter, Filter.mem_cocardinal
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
apply : #(↑(compl '' S) : Type u) < c.ord.cof
apply₁ : ∀ (i : (↑(compl '' S) : Type u)), #(↑(↑i : Set α) : Type u) < c
⊢ #(↑(compl '' S) : Type u) * ⨆ (s : (↑(compl '' S) : Type u)), #(↑(↑s : Set α) : Type u) < c

Tactic:
apply mul_lt_of_lt hreg.aleph0_le (mk_image_le.trans_lt hS) (iSup_lt_of_lt_cof_ord ..)

Premises used: Cardinal.iSup_lt_of_lt_cof_ord, Cardinal.IsRegular.aleph0_le, Cardinal.mk_image_le, Cardinal.mul_lt_of_lt, LE.le.trans_lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
rw : #(↑(compl '' S) : Type u) < c
⊢ #(↑(compl '' S) : Type u) < c.ord.cof

Tactic:
rw [hreg.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #(↑(compl '' S) : Type u) < c

Tactic:
mk_image_le.trans_lt hS

Premises used: Cardinal.mk_image_le, LE.le.trans_lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #(↑(compl '' S) : Type u) < c

Tactic:
exact mk_image_le.trans_lt hS

Premises used: Cardinal.mk_image_le, LE.le.trans_lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ ∀ (i : (↑(compl '' S) : Type u)), #(↑(↑i : Set α) : Type u) < c

Tactic:
aesop
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
p : α → Prop
⊢ (∀ᶠ (x : α) in cocardinal α hreg, p x) ↔ #(↑{x : α | ¬p x} : Type u) < c

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
apply : #(↑sᶜ : Type u) ≤ #(↑_t : Type u)
⊢ #(↑sᶜ : Type u) < c

Tactic:
apply lt_of_le_of_lt _ htf

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
⊢ sᶜ ⊆ _t

Tactic:
rw [compl_subset_comm] at hts

Premises used: Set.compl_subset_comm
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : sᶜ ⊆ _t
⊢ #(↑sᶜ : Type u) ≤ #(↑_t : Type u)

Tactic:
apply Cardinal.mk_le_mk_of_subset hts

Premises used: Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
⊢ #(↑sᶜ : Type u) < c

Tactic:
have : #↑sᶜ < c := by
        apply lt_of_le_of_lt _ htf
        rw [compl_subset_comm] at hts
        apply Cardinal.mk_le_mk_of_subset hts
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
this : #(↑sᶜ : Type u) < c
⊢ s ∈ cocardinal α hreg

Tactic:
simp_all only [mem_cocardinal]

Premises used: Filter.mem_cocardinal
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
p : α → Prop
⊢ (∃ᶠ (x : α) in cocardinal α hreg, p x) ↔ c ≤ #(↑{x : α | p x} : Type u)

Tactic:
simp only [Filter.Frequently, eventually_cocardinal, not_not, coe_setOf, not_lt]

Premises used: Classical.not_not, Filter.Frequently, not_lt, Filter.eventually_cocardinal, Set.coe_setOf
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
⊢ (∃ᶠ (x : α) in cocardinal α hreg, x ∈ s) ↔ c ≤ #(↑s : Type u)

Tactic:
frequently_cocardinal

Premises used: Set.Mem, setOf, Filter.frequently_cocardinal
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
⊢ (cocardinal α hreg ⊓ 𝓟 s).NeBot ↔ c ≤ #(↑s : Type u)

Tactic:
frequently_mem_iff_neBot.symm.trans frequently_cocardinal

Premises used: Filter.frequently_cocardinal, Iff.trans, Filter.frequently_mem_iff_neBot, Iff.symm
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
hs : #(↑s : Type u) < c
⊢ sᶜ ∈ cocardinal α hreg

Tactic:
mem_cocardinal.2 <| (compl_compl s).symm ▸ hs

Premises used: Iff.mpr, compl_compl, Filter.mem_cocardinal, Eq.rec, Eq.symm
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
hs : s.Finite
⊢ sᶜ ∈ cocardinal α hreg

Tactic:
compl_mem_cocardinal_of_card_lt <| lt_of_lt_of_le (Finite.lt_aleph0 hs) (hreg.aleph0_le)

Premises used: Filter.compl_mem_cocardinal_of_card_lt, Cardinal.IsRegular.aleph0_le, Set.Finite.lt_aleph0, lt_of_lt_of_le
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
hs : #(↑s : Type u) < c
⊢ ∀ᶠ (x : α) in cocardinal α hreg, x ∉ s

Tactic:
compl_mem_cocardinal_of_card_lt hs

Premises used: Filter.compl_mem_cocardinal_of_card_lt, Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Finset α
⊢ ∀ᶠ (x : α) in cocardinal α hreg, x ∉ s

Tactic:
eventually_cocardinal_notMem_of_card_lt <| (finset_card_lt_aleph0 s).trans_le (hreg.aleph0_le)

Premises used: Cardinal.IsRegular.aleph0_le, LT.lt.trans_le, Filter.eventually_cocardinal_notMem_of_card_lt, Cardinal.finset_card_lt_aleph0
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
x : α
⊢ ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x

Tactic:
simpa [Set.finite_singleton x] using hreg.nat_lt 1

Premises used: Cardinal.IsRegular.nat_lt, OfNat.ofNat, Set.finite_singleton
-- Module: Mathlib.Order.Filter.Cocardinal
Goal:
α : Type u
s : Set α
rw : Membership.mem (γ := Filter α) cocountable s ↔ #(↑sᶜ : Type u) ≤ ℵ₀
rw₁ : #(↑sᶜ : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ↔ #(↑sᶜ : Type u) ≤ ℵ₀
rw₂ rw₃ : #(↑sᶜ : Type u) ≤ ℵ₀ ↔ #(↑sᶜ : Type u) ≤ ℵ₀
⊢ Membership.mem (γ := Filter α) cocountable s ↔ sᶜ.Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, mem_cocardinal, lt_aleph_one_iff]

Premises used: Cardinal.le_aleph0_iff_set_countable, Filter.mem_cocardinal, Cardinal.lt_aleph_one_iff
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
⊢ Membership.mem (γ := Filter α) cofinite s ↔ sᶜ.Finite

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Finite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
p : α → Prop
⊢ (∀ᶠ (x : α) in cofinite, p x) ↔ Set.Finite.{u_2} (α := α) {x : α | ¬p x}

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Finite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
⊢ HasBasis cofinite (fun (s : Set α) ↦ s.Finite) compl

Tactic:
⟨fun s =>
    ⟨fun h => ⟨sᶜ, h, (compl_compl s).subset⟩, fun ⟨_t, htf, hts⟩ =>
      htf.subset <| compl_subset_comm.2 hts⟩⟩

Premises used: Iff.mpr, compl_compl, Compl.compl, Membership.mem, Set.compl_subset_comm, _private.0.Filter.hasBasis_cofinite.match_1, Set.Finite.subset, Eq.subset, Filter.HasBasis.mk, And.intro, Iff.intro, Exists.intro, Filter.cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : Infinite α
⊢ NeBot.{u_2} (α := α) cofinite

Tactic:
hasBasis_cofinite.neBot_iff.2 fun hs => hs.infinite_compl.nonempty

Premises used: Iff.mpr, Filter.HasBasis.neBot_iff, Filter.hasBasis_cofinite, Set.Infinite.nonempty, Set.Finite.infinite_compl
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := Filter α) cofinite ⊥ ↔ Finite α

Tactic:
simp [← empty_mem_iff_bot, finite_univ_iff]

Premises used: Filter.empty_mem_iff_bot, Set.finite_univ_iff
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
inst : Finite α
⊢ Eq.{u_2 + 1} (α := Filter α) cofinite ⊥

Tactic:
cofinite_eq_bot_iff.2 ‹_›

Premises used: Iff.mpr, Filter.cofinite_eq_bot_iff
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ Set.Infinite.{u_2} (α := α) {x : α | p x}

Tactic:
simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]

Premises used: Classical.not_not, Filter.eventually_cofinite, Filter.Frequently, Set.Infinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
⊢ (∃ᶠ (x : α) in cofinite, x ∈ s) ↔ s.Infinite

Tactic:
frequently_cofinite_iff_infinite

Premises used: Filter.frequently_cofinite_iff_infinite, Set.Mem, setOf
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
⊢ (cofinite ⊓ 𝓟 s).NeBot ↔ s.Infinite

Tactic:
frequently_mem_iff_neBot.symm.trans frequently_cofinite_mem_iff_infinite

Premises used: Filter.frequently_cofinite_mem_iff_infinite, Iff.trans, Filter.frequently_mem_iff_neBot, Iff.symm
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
hs : s.Finite
⊢ Membership.mem (γ := Filter α) cofinite sᶜ

Tactic:
mem_cofinite.2 <| (compl_compl s).symm ▸ hs

Premises used: Iff.mpr, Filter.mem_cofinite, compl_compl, Eq.rec, Eq.symm
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
hs : s.Finite
⊢ ∀ᶠ (x : α) in cofinite, x ∉ s

Tactic:
hs.compl_mem_cofinite

Premises used: Set.Mem, Filter.Eventually, setOf, Set.Finite.compl_mem_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Finset α
⊢ ∀ᶠ (x : α) in cofinite, x ∉ s

Tactic:
s.finite_toSet.eventually_cofinite_notMem

Premises used: Set.Finite.eventually_cofinite_notMem, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
⊢ s.Infinite ↔ ∃ᶠ (x : α) in cofinite, x ∈ s

Tactic:
frequently_cofinite_iff_infinite.symm

Premises used: Filter.frequently_cofinite_iff_infinite, Set.Mem, setOf, Iff.symm
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
x : α
⊢ ∀ᶠ (a : α) in cofinite, a ≠ x

Tactic:
(Set.finite_singleton x).eventually_cofinite_notMem

Premises used: Set.Mem, setOf, Set.Finite.eventually_cofinite_notMem, Set.singleton, Set.finite_singleton
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l

Tactic:
⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩

Premises used: Set.Finite.compl_mem_cofinite, Iff.intro, Set.finite_singleton