Theorem: SciLean.Prod.fst.arg_self.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_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (toMatrix K fun x => (f x).1) = fun iy ix => toMatrix K f (Sum.inl iy) ix
Tactic:
unfold toMatrix
State after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => (f x).1) ⅇ j)) = fun iy ix => ℼ(Sum.inl iy) (f ⅇ ix)

State before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => (f x).1) ⅇ j)) = fun iy ix => ℼ(Sum.inl iy) (f ⅇ ix)
Tactic:
simp[Basis.basis,Basis.proj]
State after:
no goals