Theorem: SciLean.toMatrix.apply_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
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
⊢ (toMatrix K fun f => f i) = fun ix x =>
    match x with
    | (j, jx) => if j = i ∧ jx = ix then 1 else 0
Tactic:
funext ix (j,jx)
State after:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ toMatrix K (fun f => f i) ix (j, jx) =
    match (j, jx) with
    | (j, jx) => if j = i ∧ jx = ix then 1 else 0

State before:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ toMatrix K (fun f => f i) ix (j, jx) =
    match (j, jx) with
    | (j, jx) => if j = i ∧ jx = ix then 1 else 0
Tactic:
simp[toMatrix,Basis.basis,Basis.proj]
State after:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ ℼ ix (if j = i then ⅇ jx else 0) = if j = i ∧ jx = ix then 1 else 0

State before:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ ℼ ix (if j = i then ⅇ jx else 0) = if j = i ∧ jx = ix then 1 else 0
Tactic:
sorry_proof
State after:
no goals