-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Types.Coyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq (α :=
    tensorObj (𝒞 := types)
        (tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y))
        (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z) ⟶
      Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
        (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := types)
        (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) (tensorObj.{v, u} (𝒞 := inst) X Y))
        (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z))
      ((fun (X Y : C) ↦
            (↾fun
                  (p :
                    tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
              tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                  (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                  (tensorObj.{v, u} (𝒞 := inst) X Y)))
          X Y ⊗ₘ
        𝟙 (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z))
      ((fun (X Y : C) ↦
            (↾fun
                  (p :
                    tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
              tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                  (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                  (tensorObj.{v, u} (𝒞 := inst) X Y)))
          (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≫
        Functor.map (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) (Iso.hom (α_ X Y Z))))
    (Iso.hom
        (α_ (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)
          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
            (tensorObj.{v, u} (𝒞 := inst) Y Z)))
        (𝟙 (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X) ⊗ₘ
          (fun (X Y : C) ↦
              (↾fun
                    (p :
                      tensorObj (𝒞 := types)
                        (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                        (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                  Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
                tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                    (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                  Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                    (tensorObj.{v, u} (𝒞 := inst) X Y)))
            Y Z)
        ((fun (X Y : C) ↦
            (↾fun
                  (p :
                    tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
              tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                  (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                  (tensorObj.{v, u} (𝒞 := inst) X Y)))
          X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
have h : ∀ (h : Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z)
  (f : Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
  (g : Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y),
  Eq (α :=
    Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
      (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := types)
            (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
              (tensorObj.{v, u} (𝒞 := inst) X Y))
            (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z))
          ((fun (X Y : C) ↦
                (↾fun
                      (p :
                        tensorObj (𝒞 := types)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
                  tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                    Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                      (tensorObj.{v, u} (𝒞 := inst) X Y)))
              X Y ⊗ₘ
            𝟙 (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z))
          ((fun (X Y : C) ↦
                (↾fun
                      (p :
                        tensorObj (𝒞 := types)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
                  tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                    Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                      (tensorObj.{v, u} (𝒞 := inst) X Y)))
              (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≫
            Functor.map (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) (Iso.hom (α_ X Y Z)))))
      ((f, g), h))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            (α_ (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
              (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)
              (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Z)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
              (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                (tensorObj.{v, u} (𝒞 := inst) Y Z)))
            (𝟙 (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X) ⊗ₘ
              (fun (X Y : C) ↦
                  (↾fun
                        (p :
                          tensorObj (𝒞 := types)
                            (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                            (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                      Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
                    tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                        (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                      Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                        (tensorObj.{v, u} (𝒞 := inst) X Y)))
                Y Z)
            ((fun (X Y : C) ↦
                (↾fun
                      (p :
                        tensorObj (𝒞 := types)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                          (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y)) ↦
                    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (p.1 ⊗ₘ p.2) :
                  tensorObj (𝒞 := types) (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) X)
                      (Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst)))) Y) ⟶
                    Functor.obj (Functor.obj coyoneda (op (tensorUnit.{v, u} C (𝒞 := inst))))
                      (tensorObj.{v, u} (𝒞 := inst) X Y)))
              X (tensorObj.{v, u} (𝒞 := inst) Y Z))))
      ((f, g), h))
Tactic: ext ⟨⟨f, g⟩, h⟩