## Stream: Is there code for X?

### Topic: nat.eq_of_fin_equiv

#### Adam Topaz (Oct 27 2020 at 19:52):

Do we have something like this?

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


#### Yury G. Kudryashov (Oct 27 2020 at 19:58):

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

#### Adam Topaz (Oct 27 2020 at 19:58):

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 (Oct 27 2020 at 19:58):

or just by simpa using card_congr h

#### Adam Topaz (Oct 27 2020 at 20:06):

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 :)

iff is better!

#### Adam Topaz (Oct 27 2020 at 20:07):

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

hm, good point

#### Adam Topaz (Oct 27 2020 at 20:09):

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

#### Mario Carneiro (Oct 27 2020 at 20:09):

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

Which lemma?

#### Mario Carneiro (Oct 27 2020 at 20:12):

src#cardinal.nat_cast_inj is the nearest

Oh, I see.

#### Adam Topaz (Oct 27 2020 at 20:18):

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 (Oct 28 2020 at 21:41):

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

#### Floris van Doorn (Oct 28 2020 at 21:42):

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

Oops

#### Yury G. Kudryashov (Oct 28 2020 at 22:38):

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

Last updated: May 17 2021 at 16:26 UTC