-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toPrelaxFunctor : CategoryTheory.PrelaxFunctor B C}
  {map_id :
    autoParam
      (∀ (X : B),
        toPrelaxFunctor.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctor.obj X))
      CategoryTheory.StrictPseudofunctorPreCore.map_id._autoParam}
  {map_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toPrelaxFunctor.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctor.map f) (toPrelaxFunctor.map g))
      CategoryTheory.StrictPseudofunctorPreCore.map_comp._autoParam}
  {map₂_whisker_left :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (toPrelaxFunctor.map₂ η))
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left._autoParam}
  {map₂_whisker_right :
    autoParam
      (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η g) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor.map₂ η) (toPrelaxFunctor.map g))
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right._autoParam}
  {toPrelaxFunctor_1 : CategoryTheory.PrelaxFunctor B C}
  {map_id_1 :
    autoParam
      (∀ (X : B),
        toPrelaxFunctor_1.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctor_1.obj X))
      CategoryTheory.StrictPseudofunctorPreCore.map_id._autoParam}
  {map_comp_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toPrelaxFunctor_1.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctor_1.map f) (toPrelaxFunctor_1.map g))
      CategoryTheory.StrictPseudofunctorPreCore.map_comp._autoParam}
  {map₂_whisker_left_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
        toPrelaxFunctor_1.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor_1.map f) (toPrelaxFunctor_1.map₂ η))
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left._autoParam}
  {map₂_whisker_right_1 :
    autoParam
      (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
        toPrelaxFunctor_1.map₂ (CategoryTheory.Bicategory.whiskerRight η g) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor_1.map₂ η) (toPrelaxFunctor_1.map g))
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right._autoParam},
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
        map₂_whisker_right := map₂_whisker_right } =
      { toPrelaxFunctor := toPrelaxFunctor_1, map_id := map_id_1, map_comp := map_comp_1,
        map₂_whisker_left := map₂_whisker_left_1, map₂_whisker_right := map₂_whisker_right_1 } →
    toPrelaxFunctor = toPrelaxFunctor_1