apply ArrayType.ext (Idx:=Idx)
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Neg Elem
f : Idx → Elem
⊢ -Indexed.ofFn f = Indexed.ofFn fun i => -f i
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Neg Elem
f : Idx → Elem
⊢ ∀ (i : Idx), (-Indexed.ofFn f)[i] = (Indexed.ofFn fun i => -f i)[i]