-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
x : Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a)) (op (left a_1))
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a)))
      (obj
        (Functor.leftOp
            (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
              { app := fun (x : C × D) ↦ Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                naturality := ⋯ :
                NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                  (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
          mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
            {
              app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
              naturality := ⋯ :
              NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D)) (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
        (op (left a_1))))
    (map (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≫
      Iso.hom
        ((fun (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦
            (match (motive :=
                (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) →
                  obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                    obj
                      (Functor.leftOp
                          (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                            {
                              app := fun (x : C × D) ↦
                                Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                              naturality := ⋯ :
                              NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                                (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                        mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                          {
                            app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                              Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                            naturality := ⋯ :
                            NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                              (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                      x)
                x with
              | op (left a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (left a)))
              | op (right a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a))) :
              obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                obj
                  (Functor.leftOp
                      (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                        {
                          app := fun (x : C × D) ↦
                            Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                          naturality := ⋯ :
                          NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                            (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                    mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                      {
                        app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                          Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                        naturality := ⋯ :
                        NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                          (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                  x))
          (op (left a_1))))
    (Iso.hom
        ((fun (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦
            (match (motive :=
                (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) →
                  obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                    obj
                      (Functor.leftOp
                          (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                            {
                              app := fun (x : C × D) ↦
                                Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                              naturality := ⋯ :
                              NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                                (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                        mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                          {
                            app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                              Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                            naturality := ⋯ :
                            NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                              (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                      x)
                x with
              | op (left a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (left a)))
              | op (right a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a))) :
              obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                obj
                  (Functor.leftOp
                      (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                        {
                          app := fun (x : C × D) ↦
                            Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                          naturality := ⋯ :
                          NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                            (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                    mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                      {
                        app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                          Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                        naturality := ⋯ :
                        NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                          (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                  x))
          (op (right a))) ≫
      map
        (Functor.leftOp
            (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
              { app := fun (x : C × D) ↦ Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                naturality := ⋯ :
                NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                  (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
          mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
            {
              app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
              naturality := ⋯ :
              NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D)) (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
        x)
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a)))
      (obj
        (Functor.leftOp
            (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
              { app := fun (x : C × D) ↦ Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                naturality := ⋯ :
                NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                  (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
          mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
            {
              app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
              naturality := ⋯ :
              NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D)) (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
        (op (left a_1))))
    (map (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≫
      Iso.hom
        ((fun (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦
            (match (motive :=
                (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) →
                  obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                    obj
                      (Functor.leftOp
                          (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                            {
                              app := fun (x : C × D) ↦
                                Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                              naturality := ⋯ :
                              NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                                (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                        mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                          {
                            app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                              Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                            naturality := ⋯ :
                            NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                              (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                      x)
                x with
              | op (left a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (left a)))
              | op (right a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a))) :
              obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                obj
                  (Functor.leftOp
                      (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                        {
                          app := fun (x : C × D) ↦
                            Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                          naturality := ⋯ :
                          NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                            (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                    mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                      {
                        app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                          Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                        naturality := ⋯ :
                        NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                          (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                  x))
          (op (left a_1))))
    (Iso.hom
        ((fun (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦
            (match (motive :=
                (x : (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) →
                  obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                    obj
                      (Functor.leftOp
                          (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                            {
                              app := fun (x : C × D) ↦
                                Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                              naturality := ⋯ :
                              NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                                (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                        mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                          {
                            app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                              Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                            naturality := ⋯ :
                            NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                              (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                      x)
                x with
              | op (left a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (left a)))
              | op (right a) => Iso.refl (obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (op (right a))) :
              obj (𝟭 (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) x ≅
                obj
                  (Functor.leftOp
                      (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
                        {
                          app := fun (x : C × D) ↦
                            Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                          naturality := ⋯ :
                          NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                            (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
                    mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
                      {
                        app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                          Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
                        naturality := ⋯ :
                        NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D))
                          (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
                  x))
          (op (right a))) ≫
      map
        (Functor.leftOp
            (mkFunctor (Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ)) (Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ))
              { app := fun (x : C × D) ↦ Quiver.Hom.op (edge (op (obj (Prod.snd C D) x)) (op (obj (Prod.fst C D) x))),
                naturality := ⋯ :
                NatTrans (Prod.fst C D ⋙ Functor.rightOp (inclRight Dᵒᵖ Cᵒᵖ))
                  (Prod.snd C D ⋙ Functor.rightOp (inclLeft Dᵒᵖ Cᵒᵖ)) }) ⋙
          mkFunctor (Functor.op (inclRight C D)) (Functor.op (inclLeft C D))
            {
              app := fun (x : Prod.{u₂, u₁} Dᵒᵖ Cᵒᵖ) ↦
                Quiver.Hom.op (edge (unop (obj (Prod.snd Dᵒᵖ Cᵒᵖ) x)) (unop (obj (Prod.fst Dᵒᵖ Cᵒᵖ) x))),
              naturality := ⋯ :
              NatTrans (Prod.fst Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclRight C D)) (Prod.snd Dᵒᵖ Cᵒᵖ ⋙ Functor.op (inclLeft C D)) })
        x)

Tactic:
cat_disch