Theorem: SciLean.HAdd.hAdd.arg_a0a1.toMatrix_rule (SciLean/Core/FunctionTransformations/ToMatrix.lean)

State before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.36134
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (toMatrix K fun x => f x + g x) = fun i j => toMatrix K f i j + toMatrix K g i j
Tactic:
unfold toMatrix
State after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.36134
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f x + g x) ⅇ j)) = fun i j => ℼ i (f ⅇ j) + ℼ i (g ⅇ j)

State before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.36134
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f x + g x) ⅇ j)) = fun i j => ℼ i (f ⅇ j) + ℼ i (g ⅇ j)
Tactic:
simp[(Basis.proj.arg_x.IsLinearMap_rule _).map_add]
State after:
no goals