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