stuck on cast

Stream: general

[deepest recursion]

hey peeps . it seems like lean gets stuck on casts that change type

set_option pp.proofs true in
example {P:A->Type}{p1: i = v}{m : (i : A) → P i}:
  @cast (P i) (P v) (congrArg P k) (m i) = m v
:= by
  let x : (P i) = (P v) := congrArg P k
  -- let eq : cast x = (by rw [x]; exact id) := by
  --   simp only [eq_mpr_eq_cast]
  --   rw [id.eq_1]
  --   -- id : P i -> P v ???
  --   admit
  admit

Can anything be done about it?

[Eric Wieser]

cases p1; rfl is enough

[deepest recursion]

Can anything be done to unstuck cast in this case?

import Mathlib


set_option pp.proofs true in
example
  {n1:Rat}
  {t_eq:@Eq Type { i // n1 = i } { i // (2:Rat) = i }}
  {k1: (n1:Rat) = @Eq.rec Type
    { i // n1 = i } (fun x x_1 => {b : x} → { i // n1 = i }) (fun {b} => b) { i // 2 = i }
    t_eq
    ⟨2, (Eq.refl 2)⟩}
: n1 = 2
:= by
  unfold Subtype.val at k1



  admit

[Eric Wieser]

I think #new members > ✔ Are parametric type constructors injective? @ 💬 might be relevant here

[deepest recursion]

Thanks for the reference, although I think my question is somewhat more specific. It ends up being about if it is possible to do something with casts that change type. If cast could be eliminated in the example here it would be great

[Eric Wieser]

Note there is no need to link to the web editor, every code block on zulip comes with such a link