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