[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a
[PROOFSTEP]
rcases lt_or_le a ℵ₀ with ha | ha
[GOAL]
case inl
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : a < ℵ₀
⊢ #↑t ≤ a
[PROOFSTEP]
obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
[GOAL]
case inl.intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
⊢ #↑t ≤ ↑n
[PROOFSTEP]
apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
⊢ Finset.card s ≤ n
[PROOFSTEP]
have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
⊢ Finset.card s ≤ n
[PROOFSTEP]
have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
⊢ Finset.card s ≤ n
[PROOFSTEP]
rcases B.exists with ⟨i, hi⟩
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
⊢ Finset.card s ≤ n
[PROOFSTEP]
have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
⊢ Finset.card s ≤ n
[PROOFSTEP]
let u : Finset α := (f i).toFinset
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
⊢ Finset.card s ≤ n
[PROOFSTEP]
have I1 : s.card ≤ u.card :=
  by
  have : s ⊆ u := fun x hx ↦ by simpa only [Set.mem_toFinset] using hi x hx
  exact Finset.card_le_of_subset this
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
⊢ Finset.card s ≤ Finset.card u
[PROOFSTEP]
have : s ⊆ u := fun x hx ↦ by simpa only [Set.mem_toFinset] using hi x hx
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
x : α
hx : x ∈ s
⊢ x ∈ u
[PROOFSTEP]
simpa only [Set.mem_toFinset] using hi x hx
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this✝ : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
this : s ⊆ u
⊢ Finset.card s ≤ Finset.card u
[PROOFSTEP]
exact Finset.card_le_of_subset this
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
⊢ Finset.card s ≤ n
[PROOFSTEP]
have I2 : (u.card : Cardinal) ≤ n := by convert h'f i; simp only [Set.toFinset_card, mk_fintype]
[GOAL]
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
⊢ ↑(Finset.card u) ≤ ↑n
[PROOFSTEP]
convert h'f i
[GOAL]
case h.e'_3
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
⊢ ↑(Finset.card u) = #↑(f i)
[PROOFSTEP]
simp only [Set.toFinset_card, mk_fintype]
[GOAL]
case intro
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ (x : α), x ∈ s → ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → x ∈ f i
i : ι
hi : ∀ (x : α), x ∈ s → x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := toFinset (f i)
I1 : Finset.card s ≤ Finset.card u
I2 : ↑(Finset.card u) ≤ ↑n
⊢ Finset.card s ≤ n
[PROOFSTEP]
exact
  I1.trans
    (Nat.cast_le.1 I2)
      -- case `a` infinite:
[GOAL]
case inr
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
⊢ #↑t ≤ a
[PROOFSTEP]
have : t ⊆ ⋃ i, f i := by
  intro x hx
  obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
  exact mem_iUnion_of_mem i hi
[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
⊢ t ⊆ ⋃ (i : ι), f i
[PROOFSTEP]
intro x hx
[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
⊢ x ∈ ⋃ (i : ι), f i
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
[GOAL]
case intro
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ (i : ι), f i
[PROOFSTEP]
exact mem_iUnion_of_mem i hi
[GOAL]
case inr
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ #↑t ≤ a
[PROOFSTEP]
calc
  #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
  _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
  _ ≤ sum (fun _ ↦ a) := (sum_le_sum _ _ h'f)
  _ = #ι * a := by simp
  _ ≤ ℵ₀ * a := (mul_le_mul_right' mk_le_aleph0 a)
  _ = a := aleph0_mul_eq ha
[GOAL]
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ (sum fun x => a) = #ι * a
[PROOFSTEP]
simp
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a
[PROOFSTEP]
let g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (ULift.down ⁻¹' ·) ∘ f ∘ ULift.down
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
⊢ #↑t ≤ a
[PROOFSTEP]
suffices #(ULift.down.{v} ⁻¹' t) ≤ Cardinal.lift.{v, u} a by simpa
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
this : #↑(ULift.down ⁻¹' t) ≤ lift a
⊢ #↑t ≤ a
[PROOFSTEP]
simpa
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
⊢ #↑(ULift.down ⁻¹' t) ≤ lift a
[PROOFSTEP]
let l' : Filter (ULift.{u} ι) := Filter.map ULift.up l
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
⊢ #↑(ULift.down ⁻¹' t) ≤ lift a
[PROOFSTEP]
have : NeBot l' := map_neBot
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
⊢ #↑(ULift.down ⁻¹' t) ≤ lift a
[PROOFSTEP]
apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
[GOAL]
case ht
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
⊢ ∀ (x : ULift α), x ∈ ULift.down ⁻¹' t → ∀ᶠ (i : ULift ι) in l', x ∈ g i
[PROOFSTEP]
intro x hx
[GOAL]
case ht
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
x : ULift α
hx : x ∈ ULift.down ⁻¹' t
⊢ ∀ᶠ (i : ULift ι) in l', x ∈ g i
[PROOFSTEP]
simpa only [Function.comp_apply, mem_preimage, eventually_map] using ht _ hx
[GOAL]
case h'f
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
⊢ ∀ (i : ULift ι), #↑(g i) ≤ lift a
[PROOFSTEP]
intro i
[GOAL]
case h'f
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
t : Set α
ht : ∀ (x : α), x ∈ t → ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift ι → Set (ULift α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift ι) := Filter.map ULift.up l
this : NeBot l'
i : ULift ι
⊢ #↑(g i) ≤ lift a
[PROOFSTEP]
simpa using h'f i.down
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #α ≤ a
[PROOFSTEP]
rw [← mk_univ]
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑Set.univ ≤ a
[PROOFSTEP]
exact mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f
[GOAL]
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α = a
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α ≤ a
[PROOFSTEP]
apply mk_le_of_countable_eventually_mem ht (fun i ↦ (h'f i).le)
[GOAL]
case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ a ≤ #α
[PROOFSTEP]
obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l
[GOAL]
case a.intro
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
i : ι
⊢ a ≤ #α
[PROOFSTEP]
rw [← (h'f i)]
[GOAL]
case a.intro
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : NeBot l
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
i : ι
⊢ #↑(f i) ≤ #α
[PROOFSTEP]
exact mk_set_le (f i)
