-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.mk.injEq : ∀ {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)