-- Module: Mathlib.CategoryTheory.Sums.Basic
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
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
          | Sum.inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y_1 with
          | inl X => F.obj X
          | Sum.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
              | Sum.inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | Sum.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
            | Sum.inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y_1 with
            | inl X => F.obj X
            | Sum.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
          | Sum.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
                | Sum.inr X => G.obj X :
                C)
              (match (motive := A ⊕ B → C) x_1 with
                | inl X => F.obj X
                | Sum.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
                | Sum.inr X => G.obj X :
                C)
              (match (motive := A ⊕ B → C) x_1 with
                | inl X => F.obj X
                | Sum.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
            | Sum.inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y_1 with
            | inl X => F.obj X
            | Sum.inr X => G.obj X :
            C))
⊢ 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
        | Sum.inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) z with
        | inl X => F.obj X
        | Sum.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
            | Sum.inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | Sum.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
          | Sum.inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) z with
          | inl X => F.obj X
          | Sum.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
        | Sum.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
              | Sum.inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | Sum.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
              | Sum.inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | Sum.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
          | Sum.inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) z with
          | inl X => F.obj X
          | Sum.inr X => G.obj X :
          C))

Tactic:
cases g