Theorem: SciLean.Prod.mk.arg_fstsnd.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 (max u_2 u_3)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_2 u_3)
inst✝ : FinVec IZ K Z
g : X → Y
f : X → Z
⊢ (toMatrix K fun x => (g x, f x)) = fun i jx =>
    match i with
    | Sum.inl iy => toMatrix K g iy jx
    | Sum.inr iz => toMatrix K f iz jx
Tactic:
simp[toMatrix,Basis.basis,Basis.proj]
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 (max u_2 u_3)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_2 u_3)
inst✝ : FinVec IZ K Z
g : X → Y
f : X → Z
⊢ (toMatrix K fun x => (g x, f x)) = fun i jx =>
    match i with
    | Sum.inl iy => ℼ iy (g ⅇ jx)
    | Sum.inr iz => ℼ iz (f ⅇ jx)

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 (max u_2 u_3)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_2 u_3)
inst✝ : FinVec IZ K Z
g : X → Y
f : X → Z
⊢ (toMatrix K fun x => (g x, f x)) = fun i jx =>
    match i with
    | Sum.inl iy => ℼ iy (g ⅇ jx)
    | Sum.inr iz => ℼ iz (f ⅇ jx)
Tactic:
rfl
State after:
no goals