Eq.recOn

Stream: mathlib4

[Maxwell Thum]

I'm porting Data.Fin.Tuple.Basic and I'm having issues with Eq.recOn.

[Maxwell Thum]

Here I get the error

type mismatch
  eq_rec_compose ?m.49854 ?m.49855 ?m.49856
has type
  Eq.recOn ?m.49854 (Eq.recOn ?m.49855 ?m.49856) = Eq.recOn (_ : ?m.49851 = ?m.49853) ?m.49856 : Prop
but is expected to have type
  _root_.cast (_ : α (↑castSucc.toEmbedding (castLt j (_ : ↑j < n))) = α j) (_root_.cast C2 y) = _root_.cast C1 y : Prop

[Maxwell Thum]

Here and in the line below, I get the error

failed to elaborate eliminator, invalid motive
  fun x x_1 => α x

[Maxwell Thum]

Maxwell Thum said:

Here I get the error

type mismatch
  eq_rec_compose ?m.49854 ?m.49855 ?m.49856
has type
  Eq.recOn ?m.49854 (Eq.recOn ?m.49855 ?m.49856) = Eq.recOn (_ : ?m.49851 = ?m.49853) ?m.49856 : Prop
but is expected to have type
  _root_.cast (_ : α (↑castSucc.toEmbedding (castLt j (_ : ↑j < n))) = α j) (_root_.cast C2 y) = _root_.cast C1 y : Prop

For this it turned out I just needed to fill in the blanks: exact eq_rec_compose (Eq.trans C2.symm C1) C2 y. Not sure why Lean 4 can't do this when Lean 3 could.

[Maxwell Thum]

Maxwell Thum said:

Here and in the line below, I get the error

failed to elaborate eliminator, invalid motive
  fun x x_1 => α x

Replacing Eq.recOn (succAbove_castLt hlt) (p _) with @Eq.recOn _ _ (fun x _ ↦ α x) _ (succAbove_castLt hlt) (p _) (and analogous for the line below) works for some reason

[Eric Wieser]

I tried to leave a comment on #port-status for data.fin.tuple.basic saying "please wait for a mathlib3 PR (#10346)", but the comment seems to be lost. @Johan Commelin, what's the mechanism to write those comments? I thought I did what #port-wiki requested

[Johan Commelin]

@Eric Wieser https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit

[Eric Wieser]

Ugh I forgot the .basic at the end of this filename