Type cast proof

Stream: lean4

[Jure Taslak]

How could I show the following thing involving type casts via ▸?

example {n : Nat} {l : List (Fin n)} {l_len : n = l.length} {i : Fin n}
  {h : ∃ j, l.get j = i} : ∃ j, l.get (l_len ▸ j) = i := by
  sorry

I tried using subst l_len but it gives me the error tactic 'subst' failed, 'n' occurs at List.length l, which I don't really know how to proceed from.

[Eric Wieser]

I think you can get there by first proving the more general

example {n : Nat} {l : List X} {l_len : n = l.length} {i : X}
  {h : ∃ j, l.get j = i} : ∃ j, l.get (l_len ▸ j) = i := by
  sorry

where subst l_len will work

[Jure Taslak]

This indeed worked. Thank you very much!
The proof is just

example {X : Type} {n : Nat} {l : List X} {l_len : n = l.length} {i : X}
  {h : ∃ j, l.get j = i} : ∃ j, l.get (l_len ▸ j) = i := by
  subst l_len
  simp [h]

[Kyle Miller]

Here's a way to power through your original example:

import Mathlib.Tactic

example {n : Nat} {l : List (Fin n)} {l_len : n = l.length} {i : Fin n}
    {h : ∃ j, l.get j = i} : ∃ j, l.get (l_len ▸ j) = i := by
  obtain ⟨⟨j, h⟩, rfl⟩ := h
  use! j
  · convert h
  · congr
    generalize Fin n = X at l
    subst l_len
    rfl

[Kyle Miller]

I'd suggest using docs#Fin.cast rather than the triangle. It's got better properties. Usually it's that there are better simp lemmas, but rfl somehow closes the goal in this case.

example {n : Nat} {l : List (Fin n)} {l_len : n = l.length} {i : Fin n}
    {h : ∃ j, l.get j = i} : ∃ j : Fin n, l.get (j.cast l_len) = i := by
  obtain ⟨⟨j, h⟩, rfl⟩ := h
  use! j
  · rwa [l_len] -- alternative to `convert h`
  · rfl