strange type issue in mathlib4#1685

Stream: mathlib4

[Arien Malec]

I've been staring at this issue in mathlib4#1685 for a bit -- I assume there's some obvious implicit issues going on but I've had no luck with the usual working though of implicits, etc.

import Mathlib.Data.Fintype.Card

open Set

universe u v w

variable {α : Type u} {β : Type v} {ι : Sort w}

theorem Finite.of_injective_finite_range {f : ι → α} (hf : Function.Injective f)
    [Finite (range f)] : Finite ι :=
  Finite.of_injective (Set.rangeFactorization f) (hf.codRestrict _)

gives a host of issues. As far as I can tell, there's no change from mathlib, and this should JustWork(tm)

The issues are:

application type mismatch
  Function.Injective.codRestrict ?m.671 hf
argument
  hf
has type
  Function.Injective f : Prop
but is expected to have type
  Function.Injective ?m.669 : Prop

application type mismatch
  of_injective (rangeFactorization f) (Function.Injective.codRestrict ?m.671 ?m.701)
argument
  Function.Injective.codRestrict ?m.671 ?m.701
has type
  Function.Injective (codRestrict ?m.669 ?m.670 ?m.671) : Prop
but is expected to have type
  Function.Injective (rangeFactorization f) : Prop

[Arien Malec]

(and if you're in the file and have a fix, just push it, please!)

[Ruben Van de Velde]

I'm not at lean, but I commented on the pr

[Arien Malec]

Thanks, makes sense of the issues I was seeing.

[Arien Malec]

I fixed the upstream file in the PR