set.card_to_finset_prod

Stream: Is there code for X?

[Patrick Johnson]

What is the easiest way to prove this? I have a very low-level proof, so I hope there is a better way.

import tactic
import tactic.induction

noncomputable theory
open_locale classical

def mk (W H : ℕ) : set (ℕ × ℕ) :=
{p : ℕ × ℕ | p.fst < W ∧ p.snd < H}

instance {W H : ℕ} : fintype (mk W H) := by
{ apply set.finite.fintype, rw mk,
  apply @set.finite.prod ℕ ℕ {x | x < W} {y | y < H};
  apply set.finite_lt_nat }

example {W H : ℕ} : (mk W H).to_finset.card = W * H :=
begin
  sorry
end

Proof

example {W H : ℕ} : (mk W H).to_finset.card = W * H :=
begin
  have ha : ∀ {a b c : ℕ} (h : b < c), (a * c + b) / c = a,
  { intros, induction b with b ih,
    { rw add_zero, exact nat.mul_div_left _ h },
    { specialize ih (nat.lt_of_succ_lt h),
      rw [nat.add_succ, nat.succ_div], split_ifs with h₁,
      { rw [add_assoc, nat.dvd_add_right (dvd_mul_left c a)] at h₁,
        contrapose! h, exact nat.le_of_dvd (dec_trivial) h₁ },
      { exact ih }}},
  fapply finset.card_eq_of_bijective,
  { rintro i h, exact ⟨i % W, i / W⟩ },
  { rintro ⟨x, y⟩ h₁, use y * W + x, simp [set.mem_to_finset, mk] at h₁,
    cases h₁ with h₁ h₂, fsplit,
    { obtain ⟨a, rfl⟩ := nat.exists_eq_add_of_lt h₁,
      obtain ⟨b, rfl⟩ := nat.exists_eq_add_of_lt h₂,
      nth_rewrite 1 mul_comm, nth_rewrite 2 add_assoc,
      rw add_mul, apply add_lt_add_left,
      rw [add_mul, add_comm, mul_add, one_mul],
      simp_rw one_mul, apply nat.lt_add_right, rw add_assoc,
      nth_rewrite 1 add_comm, rw ←add_assoc,
      apply nat.lt_add_right, apply nat.lt_succ_self },
    { simp, split,
      { rw nat.add_mod, simp, exact nat.mod_eq_of_lt h₁ },
      { exact ha h₁ }}},
  { rintro i h, simp [mk], split,
    { apply nat.mod_lt, by_contra' h₁, cases h₁, rw zero_mul at h, cases h },
    { exact nat.div_lt_of_lt_mul h }},
  { simp [mk], rintro i j h₁ h₂ h₃ h₄,
    have h₅ := (nat.div_add_mod' i W).symm,
    have h₆ := (nat.div_add_mod' j W).symm,
    rw [h₅, h₆], simp * at *},
end

[Eric Wieser]

This is much less bad:

import tactic
import tactic.induction

noncomputable theory
open_locale classical

def mk (W H : ℕ) : set (ℕ × ℕ) :=
{p : ℕ × ℕ | p.fst < W ∧ p.snd < H}

def mk_fin (W H : ℕ) : finset (ℕ × ℕ) :=
(finset.range W).product (finset.range H)

lemma coe_mk_fin (W H : ℕ) : ↑(mk_fin W H) = mk W H :=
by { ext, simp [mk_fin, mk] }

instance {W H : ℕ} : fintype (mk W H) :=
fintype.of_equiv (mk_fin W H) $ equiv.set_congr (coe_mk_fin _ _)

example {W H : ℕ} : (mk W H).to_finset.card = W * H :=
begin
  simp_rw ←coe_mk_fin,
  -- or just `simp`
  simp_rw [mk_fin, set.to_finset_card, finset.coe_sort_coe, fintype.card_coe,
    finset.card_product, finset.card_range],
end

[Eric Wieser]

Of course, it would be easier to just use the finset in the first place

[Patrick Johnson]

Do we have this?

example {α : Type} {s t : finset α} (h : s ≃ t) : s.card = t.card :=
begin
  sorry
end

[Patrick Johnson]

Or this?

import set_theory.cardinal.basic
open_locale cardinal

example {α : Type} {s t : set α} [fintype s] [fintype t]
  (h : # s = # t) : s.to_finset.card = t.to_finset.card :=
begin
  sorry
end

[Eric Wieser]

docs#fintype.card_congr and docs#cardinal.eq will make progress on the second one

[Eric Wieser]

docs#fintype.card_coe in reverse basically closes the first one