n m : ℕ
α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < k) }
n m : ℕ
α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < l) }
subst h
no goals
n m : ℕ
α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < k) }
simp [Function.funext_iff]