∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [inst_7 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E H')
  (M : Type u) [inst_8 : TopologicalSpace M] [inst_9 : ChartedSpace HM M] (A A' : Type u) [inst_10 : TopologicalSpace A]
  [inst_11 : ChartedSpace H A] [inst_12 : TopologicalSpace A'] [inst_13 : ChartedSpace H' A'] [inst_14 : CommGroup A]
  [inst_15 : CommGroup A'] [inst_16 : LieGroup I (↑⊤) A] [inst_17 : LieGroup I' (↑⊤) A'] (φ : A →* A')
  (hφ : ContMDiff I I' ↑⊤ ⇑φ),
  smoothSheafCommGroup.compLeft IM I I' M A A' φ hφ =
    {
      val :=
        { app := fun x => CommGrpCat.ofHom (ContMDiffMap.compLeftMonoidHom IM (↥(Opposite.unop x)) φ hφ),
          naturality := ⋯ } }