Easy cardinal question

Stream: mathlib4

[Josha Dekker]

Hi, I'm trying to get the following proof to work, but I'm probably missing some insight in how to work with cardinals. I need to show basic stuff, but because Lean interprets '1' and '2' as cardinals, I can't really get everything to work properly. Any pointers / ways to get the code to work?

import Mathlib.Order.Filter.Basic
import Mathlib.Order.Filter.CountableInter
import Mathlib.SetTheory.Cardinal.Ordinal

open Set Filter Cardinal
universe u
variable {c : Cardinal.{u}}
variable {α : Type u}

def Filter.ofCardinalInter (l : Set (Set α)) (hc : 2 < c)
    (hp : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
  sets := l
  univ_sets := @sInter_empty α ▸ hp _ ((mk_eq_zero _).trans_lt hc) (empty_subset _) -- I need 0 < 2 here, which is apperently hard in Cardinal world?
  sets_of_superset := h_mono _ _
  inter_sets {s t} hs ht := sInter_pair s t ▸ by
    apply hp _ (?_) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
    have : #({s, t} : Set (Set α)) ≤ 2 := by
      rw [Cardinal.mk_insert] -- is this really the way to go?
      · sorry -- this becomes weird to prove, as it interprets '1' and '2' as cardinals...
      · sorry -- can be solved by_cases, but is ugly
    exact lt_of_le_of_lt this hc

[Richard Osborn]

I believe the first sorry can be solved with simp only [mk_fintype]; norm_cast

[Richard Osborn]

This was the cleanest way I found to prove #({s, t} : Set (Set α)) ≤ 2. I'm sure someone can come up with something more clever.

have : #({s, t} : Set (Set α)) ≤ 2 := by
  by_cases h : s = t
  · simp [h]
  · rw [Cardinal.mk_insert (by exact h)]
    simp only [mk_fintype]; norm_cast

[Josha Dekker]

Thanks!

[Ruben Van de Velde]

You found a missing lemma:

import Mathlib

open Cardinal

lemma Cardinal.mk_insert_le {α : Type u} {s : Set α} {a : α} : #↑(insert a s) ≤ #↑s + 1 := by
  by_cases h : a ∈ s
  · simp [h]
  · rw [Cardinal.mk_insert h]

example : #({s, t} : Set (Set α)) ≤ 2 := by
  calc
    _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
    _ = 1 + 1 := by rw [Cardinal.mk_singleton]
    _ = 2 := by norm_num

[Josha Dekker]

Ruben Van de Velde said:

You found a missing lemma:

import Mathlib

open Cardinal

lemma Cardinal.mk_insert_le {α : Type u} {s : Set α} {a : α} : #↑(insert a s) ≤ #↑s + 1 := by
  by_cases h : a ∈ s
  · simp [h]
  · rw [Cardinal.mk_insert h]

example : #({s, t} : Set (Set α)) ≤ 2 := by
  calc
    _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
    _ = 1 + 1 := by rw [Cardinal.mk_singleton]
    _ = 2 := by norm_num

Do you want me to squeeze it in with my PR that I’m working on, or will you add this?

[Josha Dekker]

If so, what file should it go in? Probably the same as Cardinal.mk_insert?

[Ruben Van de Velde]

I can add it

[Josha Dekker]

great, thanks!