-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x y : C
f : x ⟶ y
d : D
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclLeft C D) x with
        | left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right d with
        | left x => F.obj x
        | right x => G.obj x :
        E))
    (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
            | left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | left x => F.obj x
            | right x => G.obj x :
            E))
        (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g) fun (c : C) (d : D) ↦
        α.app (c, d) (x := obj (inclLeft C D) x) (y := right d) (map (inclLeft C D) f ≫ edge y d) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclLeft C D) x with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right d with
          | left x => F.obj x
          | right x => G.obj x :
          E))
    (CategoryStruct.comp (Y :=
        match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclLeft C D) y with
        | left x => F.obj x
        | right x => G.obj x)
        (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
              | left x => F.obj x
              | right x => G.obj x :
              E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
              | left x => F.obj x
              | right x => G.obj x :
              E))
          (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g) fun (c : C) (d : D) ↦
          α.app (c, d) (x := obj (inclLeft C D) x) (map (inclLeft C D) f))
        (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
              | left x => F.obj x
              | right x => G.obj x :
              E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
              | left x => F.obj x
              | right x => G.obj x :
              E))
          (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g)
          (fun (c : C) (d : D) ↦ α.app (c, d)) (edge y d)) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) obj (inclLeft C D) x with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right d with
          | left x => F.obj x
          | right x => G.obj x :
          E))

Tactic:
simpa using (α.naturality <| (Prod.sectL _ d).map f).symm

Premises used: CategoryTheory.Functor.map, CategoryTheory.Prod.sectL, CategoryTheory.NatTrans.naturality, Eq.symm