Theorem: SciLean.ArrayType.sub_ofFn (SciLean/Data/ArrayType/Basic.lean)

State before:
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✝ : Sub Elem
f g : Idx → Elem
⊢ Indexed.ofFn f - Indexed.ofFn g = Indexed.ofFn fun i => f i - g i
Tactic:
apply ArrayType.ext (Idx:=Idx)
State after:
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✝ : Sub Elem
f g : Idx → Elem
⊢ ∀ (i : Idx), (Indexed.ofFn f - Indexed.ofFn g)[i] = (Indexed.ofFn fun i => f i - g i)[i]

State before:
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✝ : Sub Elem
f g : Idx → Elem
⊢ ∀ (i : Idx), (Indexed.ofFn f - Indexed.ofFn g)[i] = (Indexed.ofFn fun i => f i - g i)[i]
Tactic:
simp[HSub.hSub, Sub.sub]
State after:
no goals