-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 : Join.{v₁, v₂, u₁, u₂} C D
left :
  ∀ (a : C),
    Eq.{v₃ + 1} (α :=
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.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
              | Join.left x => F.obj x
              | right x => G.obj x :
              E)
            (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
              | Join.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 := Join.left a) (𝟙 (Join.left a)) :
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
            | Join.left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
            | Join.left x => F.obj x
            | right x => G.obj x :
            E))
      (𝟙
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
          | Join.left x => F.obj x
          | right x => G.obj x) :
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
            | Join.left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) Join.left a with
            | Join.left x => F.obj x
            | right x => G.obj x :
            E))
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
        | Join.left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
        | Join.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
            | Join.left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | Join.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) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E))
    (𝟙
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
        | Join.left x => F.obj x
        | right x => G.obj x) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E))
have right : ∀ (a : D),
  Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
        | Join.left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
        | Join.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
            | Join.left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | Join.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 := right a) (𝟙 (right a)) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E))
    (𝟙
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
        | Join.left x => F.obj x
        | right x => G.obj x) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | Join.left x => F.obj x
          | right x => G.obj x :
          E))
Tactic: cases x
Cleared hypotheses: x