noob question about cardinal

Stream: new members

[Kenny Lau]

import set_theory.cardinal

example (α : Type*) (S T : set α)
  (HS : set.finite S) (HT : set.finite T)
  (H : finset.card (set.finite.to_finset HS) ≤ finset.card (set.finite.to_finset HT)) :
  cardinal.mk S ≤ cardinal.mk T :=
sorry

[Chris Hughes]

open cardinal

example (α : Type*) (S T : set α)
  (HS : set.finite S) (HT : set.finite T)
  (H : finset.card (set.finite.to_finset HS) ≤ finset.card (set.finite.to_finset HT)) :
  cardinal.mk S ≤ cardinal.mk T :=
begin
  haveI := classical.choice HS,
  haveI := classical.choice HT,
  rwa [fintype_card S, fintype_card T, nat_cast_le,
    set.card_fintype_of_finset' (set.finite.to_finset HS),
    set.card_fintype_of_finset' (set.finite.to_finset HT)];
  simp
end

[Kenny Lau]

import set_theory.cardinal

example (α : Type*) (S T : set α)
  (HS : set.finite S) (HT : set.finite T)
  (H : finset.card (set.finite.to_finset HS) ≤ finset.card (set.finite.to_finset HT)) :
  cardinal.mk S ≤ cardinal.mk T :=
begin
  tactic.unfreeze_local_instances,
  cases HS, cases HT,
  rw [cardinal.fintype_card, cardinal.fintype_card, cardinal.nat_cast_le],
  rw [← fintype.card_coe, ← fintype.card_coe] at H,
  convert H;
  { ext z, rw [finset.mem_coe, set.finite.mem_to_finset] }
end

[Kenny Lau]

anyway why do we need so many lines