Theorem: SciLean.SciLean.EnumType.sum.arg_f.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_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (toMatrix K fun x =>  ∑ i, f x i) = fun i j =>  ∑ i', toMatrix K (fun x => f x i') 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_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ((fun x =>  ∑ i, f x i) ⅇ j)) = fun i j =>  ∑ i', ℼ i ((fun x => f x i') ⅇ j)

State before:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ((fun x =>  ∑ i, f x i) ⅇ j)) = fun i j =>  ∑ i', ℼ i ((fun x => f x i') ⅇ j)
Tactic:
simp
State after:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ( ∑ i, f (ⅇ j) i)) = fun i j =>  ∑ i', ℼ i (f (ⅇ j) i')

State before:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ( ∑ i, f (ⅇ j) i)) = fun i j =>  ∑ i', ℼ i (f (ⅇ j) i')
Tactic:
sorry_proof
State after:
no goals