cardinality of product of two sets

Stream: general

[Huỳnh Trần Khanh]

should this be included in mathlib? I license this code under Apache License 2.0 so anyone can further work on it and get it into mathlib

import Mathlib
lemma jwk {α β : Type} (a : Set α) (b : Set β) : (Set.prod a b).encard = a.encard * b.encard := by
  have eqt : { p : α × β // p.1 ∈ a ∧ p.2 ∈ b } ≃ (↑a) × (↑b) := by
    constructor
    pick_goal 3
    · rintro ⟨⟨m, n⟩, o⟩
      simp only at o
      exact ⟨⟨m, o.1⟩, ⟨n, o.2⟩⟩
    pick_goal 3
    · rintro ⟨⟨m, q⟩, ⟨n, w⟩⟩
      exact ⟨⟨m, n⟩, ⟨q, w⟩⟩
    · rintro ⟨⟨m, n⟩, o⟩
      simp only
    · rintro ⟨⟨m, q⟩, ⟨n, w⟩⟩
      simp only
  by_cases x: a.Infinite
  · rw [Set.encard_eq_top x]
    by_cases y: b = ∅
    · rw [y]; simp only [Set.encard_empty, mul_zero, Set.encard_eq_zero]
      ext ka
      simp only [Set.mem_empty_iff_false, iff_false]
      obtain ⟨m, n⟩ := ka
      intro wut
      rw [Set.prod, Set.mem_setOf] at wut
      simp only [Set.mem_empty_iff_false, and_false] at wut
    · have wk : b.encard ≠ 0 := by
        intro aj
        exact y (by exact Set.encard_eq_zero.mp aj)
      simp only [ne_eq, wk, not_false_eq_true, ENat.top_mul, Set.encard_eq_top_iff]
      rw [←Set.infinite_coe_iff]
      simp only [Set.prod, Set.coe_setOf]
      rw [Equiv.infinite_iff eqt]
      simp only [infinite_prod]
      left
      constructor
      · exact Set.infinite_coe_iff.mpr x
      · exact Set.nonempty_iff_ne_empty'.mpr y
  have ty : a.Finite := by exact Set.not_infinite.mp x
  by_cases z : b.Infinite
  · by_cases t : a = ∅
    · rw [t]; simp only [Set.encard_empty, zero_mul, Set.encard_eq_zero]
      ext ka
      simp only [Set.mem_empty_iff_false, iff_false]
      obtain ⟨m, n⟩ := ka
      intro wut
      rw [Set.prod, Set.mem_setOf] at wut
      simp only [Set.mem_empty_iff_false, false_and] at wut
    · have wk : a.encard ≠ 0 := by
        intro aj
        exact t (by exact Set.encard_eq_zero.mp aj)
      have ue : b.encard = ⊤ := by exact Set.encard_eq_top_iff.mpr z
      simp only [ue, ne_eq, wk, not_false_eq_true, ENat.mul_top, Set.encard_eq_top_iff]
      rw [←Set.infinite_coe_iff]
      simp only [Set.prod, Set.coe_setOf]
      rw [Equiv.infinite_iff eqt]
      simp only [infinite_prod]
      right
      constructor
      · exact Set.nonempty_iff_ne_empty'.mpr t
      · exact Set.infinite_coe_iff.mpr z
  · have tb : b.Finite := by exact Set.not_infinite.mp z
    rw [Set.Finite.encard_eq_coe_toFinset_card ty, Set.Finite.encard_eq_coe_toFinset_card tb]
    norm_cast
    rw [←Finset.card_product]
    have ei : Finite (a.prod b) := by
      rw [Set.prod]
      simp only [Set.coe_setOf]
      rw [Equiv.finite_iff eqt]
      have jak : Finite a := by exact ty
      have yak : Finite b := tb
      apply Finite.instProd
    have di : (a.prod b).Finite := ei
    rw [Set.Finite.encard_eq_coe_toFinset_card di]
    norm_cast
    apply Finset.card_bijective id
    · exact Function.bijective_id
    · simp only [Set.Finite.mem_toFinset, id_eq, Finset.mem_product, Prod.forall]
      intros a1 b1
      simp only [Set.prod, Set.mem_setOf_eq]

[Aaron Liu]

You should not use Set.prod a b, but instead a ×ˢ b.

[Aaron Liu]

I golfed your proof

import Mathlib.Data.Finite.Prod
import Mathlib.Data.Set.Card

theorem Set.encard_prod {α β : Type*} (a : Set α) (b : Set β) :
    (a ×ˢ b).encard = a.encard * b.encard := by
  obtain rfl | hae := a.eq_empty_or_nonempty
  · simp
  obtain rfl | hbe := b.eq_empty_or_nonempty
  · simp
  obtain ha | ha := a.infinite_or_finite
  · rw [(ha.prod_left hbe).encard_eq, ha.encard_eq, ENat.top_mul hbe.encard_pos.ne']
  obtain hb | hb := b.infinite_or_finite
  · rw [(hb.prod_right hae).encard_eq, hb.encard_eq, ENat.mul_top hae.encard_pos.ne']
  rw [ha.encard_eq_coe_toFinset_card, hb.encard_eq_coe_toFinset_card]
  rw [(ha.prod hb).encard_eq_coe_toFinset_card, ← ENat.coe_mul, ENat.coe_inj]
  rw [← ha.toFinset_prod hb, Finset.card_product]

[Huỳnh Trần Khanh]

thank you! could you also get it into mathlib please? I don't have write access and I know I'm not supposed to fork it

[Aaron Liu]

You can ask for access in #mathlib4 > github permission

[Yury G. Kudryashov]

This should follow from the general version in Cardinal

[Huỳnh Trần Khanh]

yeah I thought theorems in Cardinal could help but then it turns out to be nontrivial. also there are already theorems for bijection and addition for Set.encard and Set.ncard, I guess adding one more theorem for multiplication isn't redundant

[Yury G. Kudryashov]

import Mathlib.Data.Set.Card

@[simp]
theorem ENat.card_prod (α β : Type*) : ENat.card (α × β) = .card α * .card β := by
simp [ENat.card]

@[simp]
theorem Set.ncard_prod {α β : Type*} (s : Set α) (t : Set β) : (s ×ˢ t).encard = s.encard * t.encard := by
simp [Set.encard, ENat.card_congr (Equiv.Set.prod ..)]

[Huỳnh Trần Khanh]

I guess you are intentionally giving me a chance to make a pull request, so here it is https://github.com/leanprover-community/mathlib4/pull/22676

[Huỳnh Trần Khanh]

it's been several years since I last contributed to mathlib and the process is still largely the same