A selected canonical component map factors through its full-square singleton

import Definitions.Def_mme_dwz_step1_source_address_projectors
import Definitions.Def_mme_dwz_basis_label_projection
import Definitions.Def_mme_dwz_cw_square_fine_split_grading

open MME Module PiTensorProduct
open MME.DWZStep1Support
open MME.DWZSourceAligned

universe u

set_option autoImplicit false

theorem mme_dwz_canonicalComponent_selected_fullMap_factor
    {K : Type u} [Field K] (s : Fin 15)
    (selected : ∀ i : Fin 3,
      MME.DWZComponentRestriction.LiftedCoarsePair.{u} 6
        (cwSquareBlockType
          (MME.DWZSquare.shapeX s)
          (MME.DWZSquare.shapeY s)
          (MME.DWZSquare.shapeZ s) i))
    {W : Fin 3 → Type u}
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (post : ∀ i,
      (MME.DWZComponentRestriction.canonicalComponentBlock K s).V i →ₗ[K]
        W i)
    (i : Fin 3) :
    let componentMap := (post i).comp
      (MME.DWZComponentRestriction.basisLabelProjection
        (canonicalComponentModeBasis K s i) id {selected i})
    let fullMap := componentMap.comp
      ((cwSquareCanonicalGrading K 6).blockProj i
        (cwSquareBlockType
          (MME.DWZSquare.shapeX s)
          (MME.DWZSquare.shapeY s)
          (MME.DWZSquare.shapeZ s) i))
    fullMap.comp
        (MME.DWZComponentRestriction.basisLabelProjection
          (cwSquareCanonicalBasis K 6 i) id {(selected i).down.1}) =
      fullMap := by
  sorry