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

State before:
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ a • Indexed.ofFn f = Indexed.ofFn fun i => a • f i
Tactic:
apply ArrayType.ext (Idx:=Idx)
State after:
case a
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ ∀ (i : Idx), (a • Indexed.ofFn f)[i] = (Indexed.ofFn fun i => a • f i)[i]

State before:
case a
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ ∀ (i : Idx), (a • Indexed.ofFn f)[i] = (Indexed.ofFn fun i => a • f i)[i]
Tactic:
simp[HSMul.hSMul, SMul.smul]
State after:
no goals