From 8dcd9ce5a067b5cb30ae1899ae60bb51668e0199 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Thu, 28 Sep 2023 16:24:00 -0400
Subject: [PATCH] function transformation `toMatrix` turning linear map to
 matrix

---
 .../FunctionPropositions/IsLinearMap.lean     | 342 ++++++++++++++++++
 .../FunctionTransformations/ToMatrix.lean     | 285 +++++++++++++++
 SciLean/Core/Objects/FinVec.lean              |   5 +
 3 files changed, 632 insertions(+)
 create mode 100644 SciLean/Core/FunctionTransformations/ToMatrix.lean

diff --git a/SciLean/Core/FunctionPropositions/IsLinearMap.lean b/SciLean/Core/FunctionPropositions/IsLinearMap.lean
index e69de29b..067a9cdb 100644
--- a/SciLean/Core/FunctionPropositions/IsLinearMap.lean
+++ b/SciLean/Core/FunctionPropositions/IsLinearMap.lean
@@ -0,0 +1,342 @@
+import Mathlib.Algebra.Module.LinearMap
+import Mathlib.Algebra.Module.Prod
+import SciLean.Core.Objects.FinVec
+
+import SciLean.Tactic.FProp.Basic
+import SciLean.Tactic.FProp.Notation
+
+variable {R X Y Z ι : Type _} {E : ι → Type _}
+  [Semiring R] 
+  [AddCommGroup X] [Module R X]
+  [AddCommGroup Y] [Module R Y]
+  [AddCommGroup Z] [Module R Z]  
+  [∀ i, AddCommMonoid (E i)] [∀ i, Module R (E i)]
+
+
+--------------------------------------------------------------------------------
+
+namespace IsLinearMap
+
+variable (X R)
+theorem id_rule
+  : IsLinearMap R (fun x : X => x) := by sorry_proof
+  
+variable (Y)
+theorem const_zero_rule 
+  : IsLinearMap R (fun _ : X => (0 : Y))
+  := by sorry_proof
+variable {Y}
+
+theorem proj_rule (i : ι)
+  : IsLinearMap R (fun (x : (i : ι) → E i) => x i)
+  := by sorry_proof
+variable {X}
+
+theorem comp_rule
+  (f : Y → Z) (g : X → Y)
+  (hf : IsLinearMap R f) (hg : IsLinearMap R g)
+  : IsLinearMap R (fun x => f (g x)) := by sorry_proof
+
+theorem let_rule
+  (f : X → Y → Z) (g : X → Y)
+  (hf : IsLinearMap R (fun (x,y) => f x y)) (hg : IsLinearMap R g)
+  : IsLinearMap R (fun x => f x (g x)) := by sorry_proof
+
+
+theorem pi_rule
+  (f : X → (i : ι) → E i) (hf : ∀ i, IsLinearMap R (f · i))
+  : IsLinearMap R fun x i => f x i := by sorry_proof
+
+
+--------------------------------------------------------------------------------
+-- Register IsLinearMap --------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open Lean Meta SciLean FProp
+def fpropExt : FPropExt where
+  fpropName := ``IsLinearMap
+  getFPropFun? e := 
+    if e.isAppOf ``IsLinearMap then
+
+      if let .some f := e.getArg? 8 then
+        some f
+      else 
+        none
+    else
+      none
+
+  replaceFPropFun e f := 
+    if e.isAppOf ``IsLinearMap then
+      e.setArg 8  f
+    else          
+      e
+
+  identityRule    e := do
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``id_rule
+      origin := .decl ``id_rule
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  constantRule    e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``const_zero_rule
+      origin := .decl ``const_zero_rule
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  projRule e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``IsLinearMap.proj_rule 
+      origin := .decl ``IsLinearMap.proj_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  compRule e f g := do
+    let .some K := e.getArg? 0 | return none
+
+    let thm : SimpTheorem :=
+    {
+      proof  := ← mkAppM ``comp_rule #[K,f,g]
+      origin := .decl ``comp_rule
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  lambdaLetRule e f g := do
+    let .some K := e.getArg? 0 | return none
+
+    let thm : SimpTheorem :=
+    {
+      proof  := ← mkAppM ``let_rule #[K,f,g]
+      origin := .decl ``let_rule
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  lambdaLambdaRule e _ :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``pi_rule 
+      origin := .decl ``pi_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  discharger e := 
+    FProp.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption") e
+
+
+-- register fderiv
+#eval show Lean.CoreM Unit from do
+  modifyEnv (λ env => FProp.fpropExt.addEntry env (``IsLinearMap, fpropExt))
+
+
+end IsLinearMap
+
+
+variable {R X Y Z ι : Type _} {E : ι → Type _}
+  [Semiring R] 
+  [AddCommGroup X] [Module R X]
+  [AddCommGroup Y] [Module R Y]
+  [AddCommGroup Z] [Module R Z]  
+  [∀ i, AddCommGroup (E i)] [∀ i, Module R (E i)]
+
+
+
+-- Id --------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+
+@[fprop]
+theorem id.arg_a.IsLinearMap_rule
+  : IsLinearMap R (fun x : X => id x) := 
+by
+  sorry_proof
+ 
+-- Prod.mk ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop]
+theorem Prod.mk.arg_fstsnd.IsLinearMap_rule
+  (f : X → Z) (g : X → Y) 
+  (hf : IsLinearMap R f) (hg : IsLinearMap R g)
+  : IsLinearMap R fun x => (g x, f x) := 
+by
+  sorry_proof
+
+
+-- Prod.fst --------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop]
+theorem Prod.fst.arg_self.IsLinearMap_rule
+  (f : X → Y×Z) (hf : IsLinearMap R f)
+  : IsLinearMap R fun (x : X) => (f x).fst := 
+by
+  sorry_proof
+
+
+-- Prod.snd --------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop]
+theorem Prod.snd.arg_self.IsLinearMap_rule
+  (f : X → Y×Z) (hf : IsLinearMap R f)
+  : IsLinearMap R fun (x : X) => (f x).snd := 
+by
+  sorry_proof
+
+
+-- Neg.neg ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop]
+theorem Neg.neg.arg_a0.IsLinearMap_rule 
+  (f : X → Y) (hf : IsLinearMap R f)
+  : IsLinearMap R fun x => - f x := 
+by
+  sorry_proof
+
+
+-- HAdd.hAdd -------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop]
+theorem HAdd.hAdd.arg_a0a1.IsLinearMap_rule
+  (f g : X → Y) (hf : IsLinearMap R f) (hg : IsLinearMap R g)
+  : IsLinearMap R fun x => f x + g x :=
+by 
+  sorry_proof
+
+
+
+-- HSub.hSub -------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop]
+theorem HSub.hSub.arg_a0a1.IsLinearMap_rule 
+  (f g : X → Y) (hf : IsLinearMap R f) (hg : IsLinearMap R g)
+  : IsLinearMap R fun x => f x - g x :=
+by
+  sorry_proof
+
+
+-- -- HMul.hMul ---------------------------------------------------------------------
+-- -------------------------------------------------------------------------------- 
+
+-- @[fprop]
+-- theorem HMul.hMul.arg_a0.IsLinearMap_rule
+--   (f : X → Y) (hf : IsLinearMap R f)
+--   (y' : Y) 
+--   : IsLinearMap R fun x => f x * y'
+-- := 
+--   by_morphism (ContinuousLinearMap.comp (ContinuousLinearMap.mul_right y') (mk' R f hf))
+--   (by simp[ContinuousLinearMap.mul_right])
+
+
+-- @[fprop]
+-- theorem HMul.hMul.arg_a1.IsLinearMap_rule
+--   {R : Type _} [CommSemiring R] 
+--   {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+--   {Y : Type _} [TopologicalSpace Y] [Semiring Y] [Algebra R Y] [TopologicalSemiring Y] 
+--   (f : X → Y) (hf : IsLinearMap R f)
+--   (y' : Y) 
+--   : IsLinearMap R fun x => y' * f x
+-- := 
+--   by_morphism (ContinuousLinearMap.comp (ContinuousLinearMap.mul_left y') (mk' R f hf))
+--   (by simp[ContinuousLinearMap.mul_left])
+
+
+-- Smul.smul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop]
+theorem HSMul.hSMul.arg_a0.IsLinearMap_rule
+  (f : X → R) (y : Y) (hf : IsLinearMap R f)
+  : IsLinearMap R fun x => f x • y :=
+by 
+  sorry_proof
+
+@[fprop]
+theorem HSMul.hSMul.arg_a1.IsLinearMap_rule 
+  (c : R) (f : X → Y) (hf : IsLinearMap R f)
+  : IsLinearMap R fun x => c • f x :=
+by
+  sorry_proof
+
+@[fprop]
+theorem HSMul.hSMul.arg_a1.IsLinearMap_rule_nat
+  (c : ℕ) (f : X → Y) (hf : IsLinearMap R f)
+  : IsLinearMap R fun x => c • f x :=
+by
+  sorry_proof
+
+@[fprop]
+theorem HSMul.hSMul.arg_a1.IsLinearMap_rule_int
+  (c : ℤ) (f : X → Y) (hf : IsLinearMap R f)
+  : IsLinearMap R fun x => c • f x :=
+by
+  sorry_proof
+
+
+-- d/ite -----------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop]
+theorem ite.arg_te.IsLinearMap_rule
+  (c : Prop) [dec : Decidable c]
+  (t e : X → Y) (ht : IsLinearMap R t) (he : IsLinearMap R e)
+  : IsLinearMap R fun x => ite c (t x) (e x) := 
+by
+  induction dec
+  case isTrue h  => simp[h]; fprop
+  case isFalse h => simp[h]; fprop
+
+
+@[fprop]
+theorem dite.arg_te.IsLinearMap_rule
+  (c : Prop) [dec : Decidable c]
+  (t : c  → X → Y) (ht : ∀ p, IsLinearMap R (t p)) 
+  (e : ¬c → X → Y) (he : ∀ p, IsLinearMap R (e p))
+  : IsLinearMap R fun x => dite c (t · x) (e · x) := 
+by
+  induction dec
+  case isTrue h  => simp[h]; apply ht
+  case isFalse h => simp[h]; apply he
+
+
+namespace SciLean
+section OnFinVec 
+
+
+variable 
+  {K : Type _} [IsROrC K]
+  {IX : Type} [EnumType IX] {X : Type _} [FinVec IX K X]
+  {IY : Type} [EnumType IY] {Y : Type _} [FinVec IY K Y]
+  {IZ : Type} [EnumType IZ] {Z : Type _} [FinVec IZ K Z]
+
+@[fprop]
+theorem Basis.proj.arg_x.IsLinearMap_rule (i : IX)
+  : IsLinearMap K (fun x : X => ℼ i x) := by sorry_proof
+
+@[fprop]
+theorem DualBasis.dualProj.arg_x.IsLinearMap_rule (i : IX)
+  : IsLinearMap K (fun x : X => ℼ' i x) := by sorry_proof
+
+@[fprop]
+theorem BasisDuality.toDual.arg_x.IsLinearMap_rule
+  : IsLinearMap K (fun x : X => BasisDuality.toDual x) := by sorry_proof
+
+@[fprop]
+theorem BasisDuality.fromDual.arg_x.IsLinearMap_rule
+  : IsLinearMap K (fun x : X => BasisDuality.fromDual x) := by sorry_proof
+
+end OnFinVec
+end SciLean
diff --git a/SciLean/Core/FunctionTransformations/ToMatrix.lean b/SciLean/Core/FunctionTransformations/ToMatrix.lean
new file mode 100644
index 00000000..9866a5ec
--- /dev/null
+++ b/SciLean/Core/FunctionTransformations/ToMatrix.lean
@@ -0,0 +1,285 @@
+import SciLean.Core.Objects.FinVec
+import SciLean.Core.FunctionPropositions.IsLinearMap
+
+import SciLean.Tactic.FTrans.Basic
+import SciLean.Tactic.FProp.Basic
+
+namespace SciLean
+
+-- this ordering does not seem to work
+-- variable 
+--   {K : Type _} {IX IX IZ : Type} {X Y Z : Type _} 
+--   [IsROrC K]
+--   [EnumType IX] [FinVec IX K X]
+--   [EnumType IY] [FinVec IY K Y]
+--   [EnumType IZ] [FinVec IZ K Z]
+
+
+-- having index sets unverse polymorphic trips up simplifier
+variable 
+  {K : Type _} [IsROrC K]
+  {IX : Type} [EnumType IX] {X : Type _} [FinVec IX K X]
+  {IY : Type} [EnumType IY] {Y : Type _} [FinVec IY K Y]
+  {IZ : Type} [EnumType IZ] {Z : Type _} [FinVec IZ K Z]
+
+def mulMat (A : IZ → IY → K) (B : IY → IX → K) (i : IZ) (j : IX) : K := ∑ k, A i k * B k j
+def mulVec (A : IY → IX → K) (x : IX → K) (i : IY) : K := ∑ j, A i j * x j
+
+variable (K)
+def toMatrix (f : X → Y) (i : IY) (j : IX) : K := ℼ i (f (ⅇ j))
+
+namespace toMatrix
+--------------------------------------------------------------------------------
+
+variable (X)
+theorem id_rule 
+  : toMatrix K (fun x : X => x) 
+    =
+    fun i j => if i = j then 1 else 0 :=
+by
+  simp[toMatrix]
+
+
+variable (Y)
+theorem const_zero_rule 
+  : toMatrix K (fun x : X => (0 : Y)) 
+    =
+    fun i j => 0 :=
+by
+  simp[toMatrix]
+variable {Y}
+
+
+theorem proj_rule [EnumType ι] (i : ι)
+  : toMatrix K (fun f : ι → X => f i)
+    =
+    fun ix (j,jx) => (if j = i ∧ jx = ix then 1 else 0) :=  
+by
+  funext ix (j,jx)
+  simp[toMatrix,Basis.basis,Basis.proj]
+  sorry_proof
+
+
+theorem comp_rule 
+  (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) :=
+by
+  simp[toMatrix,mulMat]
+  funext i j
+  symm
+  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 -- simp[FinVec.is_basis]
+  
+
+-- Register `toMatrix` as function transformation ------------------------------
+--------------------------------------------------------------------------------
+
+open Lean Meta Qq
+
+def discharger (e : Expr) : SimpM (Option Expr) := do
+  withTraceNode `toMatrix_discharger (fun _ => return s!"discharge {← ppExpr e}") do
+  let cache := (← get).cache
+  let config : FProp.Config := {}
+  let state  : FProp.State := { cache := cache }
+  let (proof?, state) ← FProp.fprop e |>.run config |>.run state
+  modify (fun simpState => { simpState with cache := state.cache })
+  if proof?.isSome then
+    return proof?
+  else
+    -- if `fprop` fails try assumption
+    let tac := FTrans.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption")
+    let proof? ← tac e
+    return proof?
+
+
+open Lean Elab Term FTrans
+def ftransExt : FTransExt where
+  ftransName := ``toMatrix
+
+  getFTransFun? e := 
+    if e.isAppOf ``toMatrix then
+
+      if let .some f := e.getArg? 10 then
+        some f
+      else 
+        none
+    else
+      none
+
+  replaceFTransFun e f := 
+    if e.isAppOf ``toMatrix then
+      e.setArg 10 f
+    else          
+      e
+
+  idRule  e X := do
+    let .some K := e.getArg? 0 | return none
+    tryTheorems
+      #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ]
+      discharger e
+
+  constRule e X y := do
+    let .some K := e.getArg? 0 | return none
+    let Y ← inferType y
+    tryTheorems
+      #[ { proof := ← mkAppM ``const_zero_rule #[K, X, Y], origin := .decl ``const_zero_rule, rfl := false} ]
+      discharger e
+
+  projRule e X i := do
+    let .some K := e.getArg? 0 | return none
+    let X' := X.bindingBody!
+    if X'.hasLooseBVars then
+      trace[Meta.Tactic.ftrans.step] "can't handle this bvar app case, projection rule for dependent function of type {← ppExpr X} is not supported"
+      return none
+    tryTheorems
+      #[ { proof := ← mkAppM ``proj_rule #[K, X', i], origin := .decl ``proj_rule, rfl := false} ]
+      discharger e
+
+  compRule e f g := do
+    let .some K := e.getArg? 0 | return none
+    tryTheorems
+      #[ { proof := ← mkAppM ``comp_rule #[K, f, g], origin := .decl ``comp_rule, rfl := false} ]
+      discharger e
+
+  letRule e f g := do return none
+
+  piRule  e f := do return none
+
+  discharger := discharger
+
+
+-- register fderiv
+#eval show Lean.CoreM Unit from do
+  modifyEnv (λ env => FTrans.ftransExt.addEntry env (``toMatrix, ftransExt))
+
+
+end SciLean.toMatrix
+
+
+  
+open SciLean
+
+variable 
+  {K : Type _} [IsROrC K]
+  {IX : Type} [EnumType IX] {X : Type _} [FinVec IX K X]
+  {IY : Type} [EnumType IY] {Y : Type _} [FinVec IY K Y]
+  {IZ : Type} [EnumType IZ] {Z : Type _} [FinVec IZ K Z]
+  {IW : Type} [EnumType IW] {W : Type _} [FinVec IW K W]
+
+
+@[ftrans]
+theorem Prod.mk.arg_fstsnd.toMatrix_rule
+  (g : X → Y) (hg : IsLinearMap K g)
+  (f : X → Z) (hf : IsLinearMap K f)
+  : toMatrix K (fun x => (g x, f x))
+    =
+    fun i jx => 
+      match i with
+      | .inl iy => toMatrix K g iy jx 
+      | .inr iz => toMatrix K f iz jx :=   
+    -- this would be nice notation inspired by dex-lang
+    -- fun (iy|iz) jx => (toMatrix K g iy jx | toMatrix K f iz jx) := 
+by 
+  simp[toMatrix,Basis.basis,Basis.proj]
+  rfl
+
+
+@[ftrans]
+theorem Prod.fst.arg_self.toMatrix_rule
+  (f : X → Y×Z) (hf : IsLinearMap K f)
+  : toMatrix K (fun x => (f x).1)
+    =
+    fun iy ix => toMatrix K f (.inl iy) ix := 
+by 
+  simp[toMatrix,Basis.basis,Basis.proj]
+
+
+@[ftrans]
+theorem Prod.snd.arg_self.toMatrix_rule
+  (f : X → Y×Z) (hf : IsLinearMap K f)
+  : toMatrix K (fun x => (f x).2)
+    =
+    fun iz ix => toMatrix K f (.inr iz) ix := 
+by 
+  simp[toMatrix,Basis.basis,Basis.proj]
+
+
+
+-- id.arg_a.toMatrix_rule
+-- Function.comp.arg_f.toMatrix_rule
+-- Function.comp.arg_g.toMatrix_rule
+-- Function.comp.arg_x.toMatrix_rule
+
+@[ftrans]
+theorem HAdd.hAdd.arg_a0a1.toMatrix_rule
+  (f g : X → Y) (hf : IsLinearMap K f) (hg : IsLinearMap K g)
+  : (toMatrix K fun x => f x + g x)
+    =
+    fun i j => toMatrix K f i j + toMatrix K g i j := 
+by
+  simp[toMatrix, (Basis.proj.arg_x.IsLinearMap_rule _).map_add]
+
+
+@[ftrans]
+theorem HSub.hSub.arg_a0a1.toMatrix_rule
+  (f g : X → Y) (hf : IsLinearMap K f) (hg : IsLinearMap K g)
+  : (toMatrix K fun x => f x - g x)
+    =
+    fun i j => toMatrix K f i j - toMatrix K g i j := 
+by
+  simp[toMatrix, (Basis.proj.arg_x.IsLinearMap_rule _).map_sub]
+
+
+@[ftrans]
+theorem Neg.neg.arg_a0.toMatrix_rule
+  (f : X → Y) (hf : IsLinearMap K f) 
+  : (toMatrix K fun x => - f x)
+    =
+    fun i j => - toMatrix K f i j := 
+by
+  simp[toMatrix, (Basis.proj.arg_x.IsLinearMap_rule _).map_neg]
+
+
+@[ftrans]
+theorem HSMul.hSMul.arg_a1.toMatrix_rule
+  (k : K) (f : X → Y) (hf : IsLinearMap K f)
+  : (toMatrix K fun x => k • f x)
+    =
+    fun i j => k * toMatrix K f i j := 
+by
+  simp[toMatrix, (Basis.proj.arg_x.IsLinearMap_rule _).map_smul]
+
+
+@[ftrans]
+theorem HSMul.hSMul.arg_a0.toMatrix_rule
+  (f : X → K) (y : Y) (hf : IsLinearMap K f)
+  : (toMatrix K fun x => f x • y)
+    =
+    fun i j => f (ⅇ j) * ℼ i y := 
+by
+  simp[toMatrix, (Basis.proj.arg_x.IsLinearMap_rule _).map_smul]
+
+
+@[ftrans]
+theorem SciLean.EnumType.sum.arg_f.toMatrix_rule [EnumType ι]
+  (f : X → ι → Y) (hf : ∀ i, IsLinearMap K (f · i))
+  : toMatrix K (fun x => ∑ i, f x i)
+    =
+    fun i j => ∑ i', toMatrix K (f · i') i j := 
+by
+  simp[toMatrix]
+  sorry_proof
+
+
+@[ftrans]
+theorem SciLean.mulVec.arg_x_i.toMatrix_rule
+  (A : IY → IX → K) (x : W → IX → K) (hx : ∀ ix, IsLinearMap K (x · ix)) 
+  : toMatrix K (fun x' iy => mulVec A (x x') iy) 
+    =
+    fun _ iw => ∑ ix', A iy ix' * x (ⅇ iw) ix' := 
+by
+  sorry_proof
diff --git a/SciLean/Core/Objects/FinVec.lean b/SciLean/Core/Objects/FinVec.lean
index 64b1ff77..0cda9ccf 100644
--- a/SciLean/Core/Objects/FinVec.lean
+++ b/SciLean/Core/Objects/FinVec.lean
@@ -177,6 +177,11 @@ theorem proj_basis (i j : ι)
   : ℼ i (ⅇ[X] j) = if i=j then 1 else 0 :=
 by simp only [←inner_dualBasis_proj, inner_basis_dualBasis, eq_comm]; done
 
+@[simp]
+theorem proj_zero (i : ι)
+  : ℼ i (0 : X) = 0 :=
+by sorry_proof
+
 @[simp]
 theorem dualProj_dualBasis (i j : ι)
   : ℼ' i (ⅇ'[X] j) = if i=j then 1 else 0 :=