Theorem: SciLean.toMatrix.comp_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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (toMatrix K fun x => f (g x)) = mulMat (toMatrix K f) (toMatrix K g)
Tactic:
unfold toMatrix mulMat
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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f (g x)) ⅇ j)) = fun i j =>
     ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k 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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f (g x)) ⅇ j)) = fun i j =>
     ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j
Tactic:
funext i j
State after:
case h.h
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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢ ℼ i ((fun x => f (g x)) ⅇ j) = ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j

State before:
case h.h
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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢ ℼ i ((fun x => f (g x)) ⅇ j) = ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j
Tactic:
symm
State after:
case h.h
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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢  ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j = ℼ i ((fun x => f (g x)) ⅇ j)

State before:
case h.h
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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢  ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j = ℼ i ((fun x => f (g x)) ⅇ j)
Tactic:
calc ∑ k, ℼ i (f ⅇ k) * ℼ k (g ⅇ j)
  _ = ℼ i (f (∑ k, ℼ k (g ⅇ j) • ⅇ k)) := by sorry_proof
  _ = ℼ i (f (g ⅇ j)) := by sorry_proof
State after:
no goals

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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢  ∑ k, ℼ i (f ⅇ k) * ℼ k (g ⅇ j) = ℼ i (f ( ∑ k, ℼ k (g ⅇ j) • ⅇ k))
Tactic:
sorry_proof
State after:
no goals

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_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢ ℼ i (f ( ∑ k, ℼ k (g ⅇ j) • ⅇ k)) = ℼ i (f (g ⅇ j))
Tactic:
sorry_proof
State after:
no goals