awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 l : Filter α
inst : CountableInterFilter l
S : Set (Set α)
hS : #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
a : ∀ s ∈ S, s ∈ l
rwa : #(↑S : Type u) ≤ ℵ₀
rwa₁ rwa₂ rwa₃ rwa₄ : #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
⊢ S.Countable

Tactic:
rwa [← le_aleph0_iff_set_countable, ← lt_aleph_one_iff]

Premises used: Cardinal.le_aleph0_iff_set_countable, Cardinal.lt_aleph_one_iff
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
l : Filter α
h : CardinalInterFilter l ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)
⊢ CountableInterFilter l

Tactic:
⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem (c := ℵ₁) S ?_ a⟩

Premises used: CardinalInterFilter.cardinal_sInter_mem, CountableInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
l : Filter α
h : CardinalInterFilter l ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)
refine :
  ∀ (S : Set (Set α)) (h : S.Countable) (a : ∀ s ∈ S, s ∈ l), #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
⊢ CountableInterFilter l

Tactic:
refine ⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem (c := ℵ₁) S ?_ a⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
l : Filter α
h_1 : CardinalInterFilter l ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)
S : Set (Set α)
h : S.Countable
a : ∀ s ∈ S, s ∈ l
rwa : #(↑S : Type u) ≤ ℵ₀
rwa₁ rwa₂ rwa₃ rwa₄ : S.Countable
⊢ #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1

Tactic:
rwa [lt_aleph_one_iff, le_aleph0_iff_set_countable]

Premises used: Cardinal.le_aleph0_iff_set_countable, Cardinal.lt_aleph_one_iff
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
a : Cardinal.{u}
hac : a < c
⊢ CardinalInterFilter l a

Tactic:
CardinalInterFilter.of_cardinalInterFilter_of_le l (hac.le)

Premises used: CardinalInterFilter.of_cardinalInterFilter_of_le, LT.lt.le
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
rw : ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l
⊢ ⋂ (i : ι), s i ∈ l ↔ ∀ (i : ι), s i ∈ l

Tactic:
rw [← sInter_range _]

Premises used: Set.sInter_range
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
apply : (∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l
⊢ ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l

Tactic:
apply (cardinal_sInter_mem (lt_of_le_of_lt Cardinal.mk_range_le hic)).trans

Premises used: cardinal_sInter_mem, lt_of_le_of_lt, Cardinal.mk_range_le, Iff.trans
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ (∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l

Tactic:
forall_mem_range

Premises used: Set.forall_mem_range
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ (∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l

Tactic:
exact forall_mem_range

Premises used: Set.forall_mem_range
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s : (i : ι) → i ∈ S → Set α
rw : ⋂ (x : (↑S : Type u)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
⊢ ⋂ (i : ι), ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
rw [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ (x : (↑S : Type u)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
(cardinal_iInter_mem hS).trans Subtype.forall

Premises used: Subtype.forall, Filter.cardinal_iInter_mem, Iff.trans
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ (x : (↑S : Type u)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
exact (cardinal_iInter_mem hS).trans Subtype.forall

Premises used: Subtype.forall, Filter.cardinal_iInter_mem, Iff.trans
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
simp : ⋂ (i : ι), {x : α | p x i} ∈ l ↔ ∀ (i : ι), {x : α | p x i} ∈ l
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simp only [Filter.Eventually, setOf_forall]

Premises used: Filter.Eventually, Set.setOf_forall
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ ⋂ (i : ι), {x : α | p x i} ∈ l ↔ ∀ (i : ι), {x : α | p x i} ∈ l

Tactic:
cardinal_iInter_mem hic

Premises used: Filter.cardinal_iInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ ⋂ (i : ι), {x : α | p x i} ∈ l ↔ ∀ (i : ι), {x : α | p x i} ∈ l

Tactic:
exact cardinal_iInter_mem hic

Premises used: Filter.cardinal_iInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
p : α → (i : ι) → i ∈ S → Prop
simp : ⋂ (i : ι), ⋂ (i_1 : i ∈ S), {x : α | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x : α | p x i hi} ∈ l
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
simp only [Filter.Eventually, setOf_forall]

Premises used: Filter.Eventually, Set.setOf_forall
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
p : α → (i : ι) → i ∈ S → Prop
⊢ ⋂ (i : ι), ⋂ (i_1 : i ∈ S), {x : α | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x : α | p x i hi} ∈ l

Tactic:
cardinal_bInter_mem hS

Premises used: Filter.cardinal_bInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
p : α → (i : ι) → i ∈ S → Prop
⊢ ⋂ (i : ι), ⋂ (i_1 : i ∈ S), {x : α | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x : α | p x i hi} ∈ l

Tactic:
exact cardinal_bInter_mem hS

Premises used: Filter.cardinal_bInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s t : ι → Set α
hic : #ι < c
h : ∀ (i : ι), s i ≤ᶠ[l] t i
⊢ ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i

Tactic:
((eventually_cardinal_forall hic).2 h).mono fun _ hst hs => mem_iUnion.2 <|
    (mem_iUnion.1 hs).imp hst

Premises used: Iff.mpr, Filter.eventually_cardinal_forall, Set.mem_iUnion, Exists.imp, Filter.Eventually.mono, Iff.mp, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s t : ι → Set α
hic : #ι < c
h : ∀ (i : ι), s i =ᶠ[l] t i
⊢ ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i

Tactic:
(EventuallyLE.cardinal_iUnion hic fun i => (h i).le).antisymm
    (EventuallyLE.cardinal_iUnion hic fun i => (h i).symm.le)

Premises used: Filter.EventuallyLE.cardinal_iUnion, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
simp : ⋃ (x : (↑S : Type u)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u)), t (↑x : ι) ⋯
⊢ ⋃ (i : ι), ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h

Tactic:
simp only [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ (x : (↑S : Type u)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u)), t (↑x : ι) ⋯

Tactic:
EventuallyLE.cardinal_iUnion hS fun i => h i i.2

Premises used: Filter.EventuallyLE.cardinal_iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ (x : (↑S : Type u)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u)), t (↑x : ι) ⋯

Tactic:
exact EventuallyLE.cardinal_iUnion hS fun i => h i i.2

Premises used: Filter.EventuallyLE.cardinal_iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
⊢ ⋃ (i : ι), ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h

Tactic:
(EventuallyLE.cardinal_bUnion hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.cardinal_bUnion hS fun i hi => (h i hi).symm.le)

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.cardinal_bUnion, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s t : ι → Set α
hic : #ι < c
h : ∀ (i : ι), s i ≤ᶠ[l] t i
⊢ ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i

Tactic:
((eventually_cardinal_forall hic).2 h).mono fun _ hst hs =>
    mem_iInter.2 fun i => hst _ (mem_iInter.1 hs i)

Premises used: Iff.mpr, Filter.eventually_cardinal_forall, Set.mem_iInter, Filter.Eventually.mono, Iff.mp, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s t : ι → Set α
hic : #ι < c
h : ∀ (i : ι), s i =ᶠ[l] t i
⊢ ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i

Tactic:
(EventuallyLE.cardinal_iInter hic fun i => (h i).le).antisymm
    (EventuallyLE.cardinal_iInter hic fun i => (h i).symm.le)

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyLE.cardinal_iInter, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
simp : ⋂ (x : (↑S : Type u)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u)), t (↑x : ι) ⋯
⊢ ⋂ (i : ι), ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ (x : (↑S : Type u)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u)), t (↑x : ι) ⋯

Tactic:
EventuallyLE.cardinal_iInter hS fun i => h i i.2

Premises used: Filter.EventuallyLE.cardinal_iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ (x : (↑S : Type u)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u)), t (↑x : ι) ⋯

Tactic:
exact EventuallyLE.cardinal_iInter hS fun i => h i i.2

Premises used: Filter.EventuallyLE.cardinal_iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
⊢ ⋂ (i : ι), ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h

Tactic:
(EventuallyLE.cardinal_bInter hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.cardinal_bInter hS fun i hi => (h i hi).symm.le)

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.cardinal_bInter, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
apply : #(↑{s, t} : Type u) < c
⊢ ⋂₀ {s, t} ∈ l

Tactic:
apply hl _ (?_) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ #(↑{s, t} : Type u) ≤ #(↑{t} : Type u) + 1

Tactic:
Cardinal.mk_insert_le

Premises used: Cardinal.mk_insert_le
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ #(↑{t} : Type u) + 1 = 2

Tactic:
norm_num
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
_ : #(↑{t} : Type u) + 1 = 2
⊢ #(↑{s, t} : Type u) ≤ 2

Tactic:
calc
      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
      _ = 2 := by norm_num

Premises used: Cardinal.mk_insert_le, Singleton.singleton
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ #(↑{s, t} : Type u) ≤ 2

Tactic:
have : #({s, t} : Set (Set α)) ≤ 2 := by
      calc
      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
      _ = 2 := by norm_num
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
this : #(↑{s, t} : Type u) ≤ 2
⊢ #(↑{s, t} : Type u) < c

Tactic:
lt_of_le_of_lt this hc

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
this : #(↑{s, t} : Type u) ≤ 2
⊢ #(↑{s, t} : Type u) < c

Tactic:
exact lt_of_le_of_lt this hc

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
⊢ CardinalInterFilter (ofCardinalInter l hc hl h_mono) c

Tactic:
⟨hl⟩

Premises used: CardinalInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s : Set α
⊢ s ∈ ofCardinalInter l hc hl h_mono ↔ s ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
refine_1 :
  ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hSp : S ⊆ {s : Set α | sᶜ ∈ l}),
    Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)
refine_2 :
  ∀ (s t : Set α) (ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s) (hsub : s ⊆ t),
    Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} t
⊢ Filter α

Tactic:
refine .ofCardinalInter {s | sᶜ ∈ l} hc (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
refine_1 : ⋃₀ (compl '' S) ∈ l
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)

Tactic:
rw [mem_setOf_eq, compl_sInter]

Premises used: Set.compl_sInter, Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
refine_1 : ∀ s ∈ compl '' S, s ∈ l
⊢ ⋃₀ (compl '' S) ∈ l

Tactic:
apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)

Premises used: lt_of_le_of_lt, Compl.compl, Cardinal.mk_image_le, Set.image
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
s : Set α
hs : s ∈ compl '' S
⊢ ∃ x ∈ S, xᶜ = s

Tactic:
rw [mem_image] at hs

Premises used: Set.mem_image
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
refine_1 : ∀ (t : Set α) (ht : t ∈ S), tᶜ ∈ l
⊢ s ∈ l

Tactic:
rcases hs with ⟨t, ht, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
t : Set α
ht : t ∈ S
⊢ tᶜ ∈ l

Tactic:
apply hSp ht
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : s ⊆ t
refine_2 : tᶜ ∈ l
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} t

Tactic:
rw [mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : s ⊆ t
⊢ tᶜ ⊆ sᶜ

Tactic:
rw [← compl_subset_compl] at hsub

Premises used: Set.compl_subset_compl
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l

Tactic:
hmono sᶜ ht tᶜ hsub

Premises used: Compl.compl
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l

Tactic:
exact hmono sᶜ ht tᶜ hsub

Premises used: Compl.compl
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
h₁ : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
h₂ : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ CardinalInterFilter (ofCardinalUnion l hc h₁ h₂) c

Tactic:
cardinalInter_ofCardinalInter ..

Premises used: Filter.cardinalInter_ofCardinalInter, Filter.ofCardinalUnion
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
l : Set (Set α)
hc : 2 < c
hunion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s : Set α
⊢ s ∈ ofCardinalUnion l hc hunion hmono ↔ l sᶜ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : Set α
⊢ CardinalInterFilter (𝓟 s) c

Tactic:
⟨fun _ _ hS => subset_sInter hS⟩

Premises used: Set.subset_sInter, CardinalInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
rw : CardinalInterFilter (α := α) (𝓟 ∅) c
⊢ CardinalInterFilter (α := α) ⊥ c

Tactic:
rw [← principal_empty]

Premises used: Filter.principal_empty
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
⊢ CardinalInterFilter (α := α) (𝓟 ∅) c

Tactic:
apply cardinalInterFilter_principal

Premises used: Filter.cardinalInterFilter_principal
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
rw : CardinalInterFilter (α := α) (𝓟 Set.univ) c
⊢ CardinalInterFilter (α := α) ⊤ c

Tactic:
rw [← principal_univ]

Premises used: Filter.principal_univ
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
⊢ CardinalInterFilter (α := α) (𝓟 Set.univ) c

Tactic:
apply cardinalInterFilter_principal

Premises used: Filter.cardinalInterFilter_principal
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (comap f l) c

Tactic:
⟨fun S hSc hS => ?_⟩

Premises used: CardinalInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
refine : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ comap f l), ⋂₀ S ∈ comap f l
⊢ CardinalInterFilter (comap f l) c

Tactic:
refine ⟨fun S hSc hS => ?_⟩