nat.eq_of_fin_equiv

Stream: Is there code for X?

[Adam Topaz]

Do we have something like this?

example {m n : ℕ} : fin m ≃ fin n → m = n := sorry

[Yury G. Kudryashov]

It seems that we don't have it. The proof can be extracted from src#invariant_basis_number_field

[Adam Topaz]

example {m n : ℕ} : fin m ≃ fin n → m = n := λ h,
begin
  rw (show m = fintype.card (fin m), by simp),
  rw (show n = fintype.card (fin n), by simp),
  apply fintype.card_congr h
end

[Yury G. Kudryashov]

or just by simpa using card_congr h

[Adam Topaz]

Okay, I'll add it as part of a PR for the category of finite sets. I need that lemma to show that the "Skeleton" is actually skeletal :)

[Mario Carneiro]

iff is better!

[Adam Topaz]

But how?! (the equivalence is not a prop)

[Mario Carneiro]

hm, good point

[Adam Topaz]

I also wanted to make it an iff. I guess using nonempty?

[Mario Carneiro]

yeah, at that point it's basically the same as the lemma in cardinal

[Adam Topaz]

Which lemma?

[Mario Carneiro]

src#cardinal.nat_cast_inj is the nearest

[Adam Topaz]

Oh, I see.

[Adam Topaz]

Okay, so you think the following is better?

lemma nat.fin_equiv_iff_eq {m n : ℕ} : nonempty (fin m ≃ fin n) ↔ m = n :=
  ⟨λ ⟨h⟩, by simpa using fintype.card_congr h, λ h, ⟨equiv.cast $ h ▸ rfl ⟩ ⟩

[Eric Wieser]

The non-prop form of iff is (fin m ≃ fin n) ≃ (m = n), right?

[Floris van Doorn]

No, since fin n ≃ fin n has cardinality n! and n = n has cardinality 1.

[Eric Wieser]

Oops

[Yury G. Kudryashov]

The on-prop form is trunc (fin m ≃ fin n) ≃ (m = n)