∀ {𝕜 : Type u_3} [inst : NontriviallyNormedField 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_9} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_6}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_10} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (N : Type u_2) [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {E'' : Type u_5} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E''] {H'' : Type u_7}
  [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {n : WithTop ℕ∞} {R' : Type u_8}
  [inst_12 : Ring R'] [inst_13 : TopologicalSpace R'] [inst_14 : ChartedSpace H' R'] [inst_15 : ContMDiffRing I' n R']
  {R'' : Type u_1} [inst_16 : Ring R''] [inst_17 : TopologicalSpace R''] [inst_18 : ChartedSpace H'' R'']
  [inst_19 : ContMDiffRing I'' n R''] (φ : R' →+* R'') (hφ : ContMDiff I' I'' n ⇑φ),
  (↑(ContMDiffMap.compLeftAddMonoidHom I N φ.toAddMonoidHom hφ)).toFun 0 = 0