-- 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 y z : A ⊕ B
f : x ⟶ y
g : y ⟶ z
inl :
  ∀ (x y : A) (f : x ⟶ y) (g : obj (Sum.inl_ A B) y ⟶ z),
    Eq.{v₃ + 1} (α :=
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) z 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)
          (map (Sum.inl_ A B) f ≫ g) :
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) x with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) z with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C))
      (CategoryStruct.comp (Y :=
          match (motive := A ⊕ B → C) obj (Sum.inl_ A B) y with
          | Sum.inl X => F.obj X
          | inr X => G.obj X)
          (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 :=
            obj (Sum.inl_ A B) x) (map (Sum.inl_ A B) f))
          (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) g) :
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) x with
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) z 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) z 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) (f ≫ g) :
      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) z with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := A ⊕ B → C) y with
        | Sum.inl X => F.obj X
        | inr X => G.obj X)
        (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) f)
        (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) g) :
      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) z with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
have inr : ∀ (x y : B) (f : x ⟶ y) (g : obj (Sum.inr_ A B) y ⟶ z),
  Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) x with
        | Sum.inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) z 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) (map (Sum.inr_ A B) f ≫ g) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) z with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y with
        | Sum.inl X => F.obj X
        | inr X => G.obj X)
        (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 := obj (Sum.inr_ A B) x)
          (map (Sum.inr_ A B) f))
        (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) g) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) x with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) z with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
Tactic: cases f
Cleared hypotheses: x, y, f, g