∀ {S : Type u_1} {R : Type u_3} {M : Type u_2} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_4}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (_F : TrivSqZeroExt R M →ₐ[S] A),
  TrivSqZeroExt.lift
      (↑⟨(_F.comp (TrivSqZeroExt.inlAlgHom S R M), _F.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M)), ⋯⟩).1
      (↑⟨(_F.comp (TrivSqZeroExt.inlAlgHom S R M), _F.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M)), ⋯⟩).2 ⋯ ⋯ ⋯ =
    _F