-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} A C
G : Functor.{v₂, v₃, u₂, u₃} B C
x : A ⊕ B
inl :
  ∀ (val : A),
    Eq.{v₃ + 1} (α :=
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
      (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := C)
            (match (motive := A ⊕ B → C) x with
              | Sum.inl X => F.obj X
              | inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | Sum.inl X => F.obj X
              | inr X => G.obj X :
              C))
          (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := Sum.inl val)
          (𝟙 (Sum.inl val)) :
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) Sum.inl val with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) Sum.inl val with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C))
      (𝟙
          (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X) :
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) Sum.inl val with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) Sum.inl val with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C))
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) x with
        | Sum.inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) x with
        | Sum.inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g) (𝟙 x) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) x with
        | Sum.inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
have inr : ∀ (val : B),
  Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) inr val with
        | Sum.inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) inr val with
        | Sum.inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := inr val) (𝟙 (inr val)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inr val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inr val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) inr val with
        | Sum.inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) inr val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) inr val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
Tactic: cases x
Cleared hypotheses: x