Theorem: List.get_congr (Algdata/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
γ : Type w
x y : List α
i : Fin (length x)
j✝ : Fin (length y)
j : Fin (length x)
h : ↑i = ↑j
⊢ get x i = get x j
Tactic:
rw [Fin.eq_of_val_eq h]
State after:
no goals