α : Type u
n : ℕ
f g : Fin n → α
h : { fst := n, snd := f } = { fst := n, snd := g }
⊢ HEq f g
α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ HEq f g
rw [ofFn_inj'] at h
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ HEq f f
α : Type u
n : ℕ
f g : Fin n → α
h : { fst := n, snd := f } = { fst := n, snd := g }
⊢ HEq f g
cases h
no goals
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ HEq f f
rfl