∀ (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddCommGroup V2] [inst_3 : Module k V1] [inst_4 : Module k V2] [inst_5 : Semiring R] [inst_6 : Module R V2]
  [inst_7 : SMulCommClass k R V2] (p : V2 × (V1 →ₗ[k] V2)),
  (AffineMap.toConstProdLinearMap R).symm p = p.2.toAffineMap + AffineMap.const k V1 p.1