how to deal with different instances of subsingletons?

Stream: general

[Eric Rodriguez]

#mwe:

import data.fintype.basic
import tactic

inductive foo
| bar : foo

open fintype foo

instance : subsingleton foo := ⟨λ a b, by cases a; cases b; simp⟩

def quiv : foo ≃ fin 1 :=
{ to_fun := λ _, 0,
  inv_fun := λ _, bar,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

example : card foo = card (fin 1) :=
begin
  rw of_equiv_card quiv,
end

If you try this, you'll get the incomprehensible error

rewrite tactic failed, did not find instance of the pattern in the target expression card (fin 1)

Now, this is because the two fintype instances are different (see with pp.implicit). However, fintype is a subsingleton, so there should be a simple way to get around this, adn yet I can't seem to. I tried equiv_rw and other things that had subsingleton in the name, but got nowhere without using >10 lines to deal with this. any advice?

[Scott Morrison]

example : card foo = card (fin 1) :=
begin
  convert of_equiv_card quiv.symm,
end

[Scott Morrison]

convert is the main tool for dealing with non-matching but subsingleton instances

[Eric Rodriguez]

amazing, thank you!

[Scott Morrison]

why of_equiv_card flips things over, I do not know :shrug:

[Scott Morrison]

Oh, you should be using card_congr in the first place.

[Scott Morrison]

example : card foo = card (fin 1) :=
begin
  rw card_congr quiv,
end

works fine

[Scott Morrison]

You were actually creating the instance mismatch yourself by using of_equiv_card, which doesn't assume an existing fintype instance on the LHS, and instead generates one by transporting the fintype instance on the RHS over the equiv.

[Eric Rodriguez]

ahh, I see - that's why there's two different lemmata for this

[Eric Wieser]

docs#fintype.of_equiv_card is so named because it is a lemma about docs#fintype.of_equiv