application type mismatch ⋯.mp argument on congrArg

Stream: new members

[thielema]

I am trying to prove the following:

import Mathlib

theorem congr_getElem_left (k : Nat) {xs ys : List α} (hkxs : k < xs.length)
  (h : xs = ys)
  : have hkys : k < ys.length := by rwa [h] at hkxs
    xs[k] = ys[k]
  := by simp only [h]

theorem surjective_of_map_finRange (f : Fin n → Fin n)
  (ixs : List (Fin n)) (perm : ixs.map f = List.finRange n)
  : Function.Surjective f
  := by
  intro k
  have length_map_xs : (List.map f ixs).length = n := by
      apply congrArg List.length at perm
      rwa [List.length_finRange] at perm
  have := k.isLt
  simp only [← length_map_xs] at this
  apply congr_getElem_left k this at perm
  simp at perm

At the "simp at perm" I get the error:

application type mismatch
  ⋯.mp
argument
  congrArg (fun x ↦ x = (List.finRange n)[↑k]) (List.getElem_map f)
has type
  ((List.map f ixs)[↑k] = (List.finRange n)[↑k]) = (f ixs[↑k] = (List.finRange n)[↑k]) : Prop
but is expected to have type
  ?α = ?β : Prop

I am surprised that calling "simp" can cause an error, at all. Am I doing something wrong or is this a Lean4 bug? I use Lean4.14.

[Ruben Van de Velde]

Fun, that does seem like a lean bug

[thielema]

I have just checked: The same happens with List.get_of_eq.

[llllvvuu]

might actually be an issue with apply at; it works with have:

import Mathlib.Tactic.ApplyAt

theorem congr_getElem_left (k : Nat) {xs ys : List α} (hkxs : k < xs.length)
  (h : xs = ys)
  : xs[k] = ys[k]'(by rwa [h] at hkxs)
  := by simp only [h]

set_option pp.all true in
example (a : List Nat) (k : Nat) (hk : k < a.length) :
    a[k] = (a.map id)[k]'(by simp [hk]) := by
  have : a = a.map id := by simp
  apply congr_getElem_left k hk at this
  fail_if_success simp at this

  have : a = a.map id := by simp
  have := congr_getElem_left k hk this
  simp at this

  simp

it looks like apply at leaves a metavariable in place of where this✝ should be.

Maybe forallMetaTelescopeReducing is struggling with the metavariable in congr_getElem_left k hk for the implicit variable ys?

[llllvvuu]

fix available: #20623