Fintype.card of a `Set ℕ`

Stream: mathlib4

[David Renshaw]

This works in mathlib3:

import data.nat.interval
import data.fintype.card

def foo (m : ℕ) (A : set ℕ) (hA : A = {n | n < m}) : fintype A :=
begin
  rw[hA],
  exact infer_instance
end

theorem bar (m : ℕ) (A : set ℕ) (hA : A = {n | n < m}) :
    @fintype.card A (foo m A hA) = m :=
begin
  simp_rw[hA],
  simp[hA]
end

However, I have not been able to figure out how to make it work in mathlib4:

import Mathlib.Data.Nat.Interval
import Mathlib.Data.Fintype.Card

def foo (m : ℕ) (A : Set ℕ) (hA : A = {n | n < m}) : Fintype A := by
  rw[hA]
  exact inferInstance

theorem bar (m : ℕ) (A : Set ℕ) (hA : A = {n | n < m}) :
    @Fintype.card A (foo m A hA) = m := by
  simp_rw[hA] -- does not do anything
  sorry

Does this indicate the existence of a bug? Or maybe I'm abusing Fintype.card, and this shouldn't be expected to work anyways?

[Eric Wieser]

This works:

@[congr]
lemma Fintype.card_congr'' {A B : Type _} {iA : Fintype A} {iB : Fintype B} (h : A = B) :
  @Fintype.card _ iA = @Fintype.card _ iB := Fintype.card_congr' h

theorem bar (m : ℕ) (A : Set ℕ) (hA : A = {n | n < m}) :
    @Fintype.card A (foo m A hA) = m := by
  simp_rw[hA] -- works
  sorry

[Eric Wieser]

It looks like somehow docs4#Fintype.card_congr' isn't firing

[David Renshaw]

cool, and then simp only [Fintype.card_ofFinset, Finset.card_range] closes that sorry

[David Renshaw]

but now I'm confused about why in the mathlib3 version, the simp picks up the finset.card_range lemma, which is not tagged as [simp].

[David Renshaw]

The difference between Fintype.card_congr' and your Fintype.card_congr'' seems to be that the former uses [] brackets for the Fintype premises, while the latter uses {} brackets.

[Eric Wieser]

Yes, I suspect this is because Lean4 chooses to be stubborn and not fill [] by unification even if it knows it can

[Eric Wieser]

I don't know whether the solution is to teach @[congr] to use unification, or to change Fintype.card_congr' to use {} and add a porting note. Probably the thing to do is open an issue about the former, and then reference it in a comment in the latter