smul_comp

smul_comp.lean

theorem CategoryTheory.Linear.smul_comp.{w, v₁, u₁} : ∀ {R : Type w} [inst : Semiring R] {C : Type u₁}
  [inst_1 : CategoryTheory.Category C] [inst_2 : @CategoryTheory.Preadditive C inst_1]
  [self : @CategoryTheory.Linear R inst C inst_1 inst_2] (X Y Z : C) (r : R)
  (f :
    @Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
  (g :
    @Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) Y Z),
  @Eq
    (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
    (@CategoryTheory.CategoryStruct.comp C (@CategoryTheory.Category.toCategoryStruct C inst_1) X Y Z
      (@HSMul.hSMul R
        (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1))
          X Y)
        (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1))
          X Y)
        (@instHSMul R
          (@Quiver.Hom C
            (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
          (@MulAction.toSMul R
            (@Quiver.Hom C
              (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
            (@Semiring.toMulOneClass R inst)
            (@DistribMulAction.toMulAction R
              (@Quiver.Hom C
                (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
              (@Semiring.toMulOneClass R inst)
              (@AddGroup.toAddMonoid
                (@Quiver.Hom C
                  (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
                (@CategoryTheory.Preadditive.homGroup C inst_1 inst_2 X Y))
              (@Module.toDistribMulAction R
                (@Quiver.Hom C
                  (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
                inst
                (@AddGroup.toAddMonoid
                  (@Quiver.Hom C
                    (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X
                    Y)
                  (@CategoryTheory.Preadditive.homGroup C inst_1 inst_2 X Y))
                (@CategoryTheory.Linear.homModule R inst C inst_1 inst_2 self X Y)))))
        r f)
      g)
    (@HSMul.hSMul R
      (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X
        Z)
      (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X
        Z)
      (@instHSMul R
        (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1))
          X Z)
        (@MulAction.toSMul R
          (@Quiver.Hom C
            (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
          (@Semiring.toMulOneClass R inst)
          (@DistribMulAction.toMulAction R
            (@Quiver.Hom C
              (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
            (@Semiring.toMulOneClass R inst)
            (@AddGroup.toAddMonoid
              (@Quiver.Hom C
                (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
              (@CategoryTheory.Preadditive.homGroup C inst_1 inst_2 X Z))
            (@Module.toDistribMulAction R
              (@Quiver.Hom C
                (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
              inst
              (@AddGroup.toAddMonoid
                (@Quiver.Hom C
                  (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
                (@CategoryTheory.Preadditive.homGroup C inst_1 inst_2 X Z))
              (@CategoryTheory.Linear.homModule R inst C inst_1 inst_2 self X Z)))))
      r (@CategoryTheory.CategoryStruct.comp C (@CategoryTheory.Category.toCategoryStruct C inst_1) X Y Z f g)) :=
fun (R : Type w) [inst : Semiring R] (C : Type u₁) [inst_1 : CategoryTheory.Category C]
    [inst_2 : @CategoryTheory.Preadditive C inst_1] [self : @CategoryTheory.Linear R inst C inst_1 inst_2] =>
  self.2