-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
b₀ b₁ b₂ : LocallyDiscrete C
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
      ((fun (x : LocallyDiscrete C) ↦
          (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
            | { as := X } => { as := F.obj X } :
            LocallyDiscrete D))
        b₀)
      ((fun (x : LocallyDiscrete C) ↦
          (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
            | { as := X } => { as := F.obj X } :
            LocallyDiscrete D))
        b₂))
    ((fun {b b' : LocallyDiscrete C} (x : b ⟶ b') ↦
        (match (motive :=
            (b ⟶ b') →
              Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
                ((fun (x : LocallyDiscrete C) ↦
                    (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                      | { as := X } => { as := F.obj X } :
                      LocallyDiscrete D))
                  b)
                ((fun (x : LocallyDiscrete C) ↦
                    (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                      | { as := X } => { as := F.obj X } :
                      LocallyDiscrete D))
                  b'))
            x with
          | { as := f } => (F.map f).toLoc :
          Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
            ((fun (x : LocallyDiscrete C) ↦
                (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                  | { as := X } => { as := F.obj X } :
                  LocallyDiscrete D))
              b)
            ((fun (x : LocallyDiscrete C) ↦
                (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                  | { as := X } => { as := F.obj X } :
                  LocallyDiscrete D))
              b')))
      (f ≫ g))
    (CategoryStruct.comp (Y :=
      (fun (x : LocallyDiscrete C) ↦
          (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
            | { as := X } => { as := F.obj X } :
            LocallyDiscrete D))
        b₁)
      ((fun {b b' : LocallyDiscrete C} (x : b ⟶ b') ↦
          (match (motive :=
              (b ⟶ b') →
                Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
                  ((fun (x : LocallyDiscrete C) ↦
                      (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                        | { as := X } => { as := F.obj X } :
                        LocallyDiscrete D))
                    b)
                  ((fun (x : LocallyDiscrete C) ↦
                      (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                        | { as := X } => { as := F.obj X } :
                        LocallyDiscrete D))
                    b'))
              x with
            | { as := f } => (F.map f).toLoc :
            Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
              ((fun (x : LocallyDiscrete C) ↦
                  (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                    | { as := X } => { as := F.obj X } :
                    LocallyDiscrete D))
                b)
              ((fun (x : LocallyDiscrete C) ↦
                  (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                    | { as := X } => { as := F.obj X } :
                    LocallyDiscrete D))
                b')))
        f)
      ((fun {b b' : LocallyDiscrete C} (x : b ⟶ b') ↦
          (match (motive :=
              (b ⟶ b') →
                Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
                  ((fun (x : LocallyDiscrete C) ↦
                      (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                        | { as := X } => { as := F.obj X } :
                        LocallyDiscrete D))
                    b)
                  ((fun (x : LocallyDiscrete C) ↦
                      (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                        | { as := X } => { as := F.obj X } :
                        LocallyDiscrete D))
                    b'))
              x with
            | { as := f } => (F.map f).toLoc :
            Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
              ((fun (x : LocallyDiscrete C) ↦
                  (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                    | { as := X } => { as := F.obj X } :
                    LocallyDiscrete D))
                b)
              ((fun (x : LocallyDiscrete C) ↦
                  (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                    | { as := X } => { as := F.obj X } :
                    LocallyDiscrete D))
                b')))
        g))

Tactic:
simp