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

Tactic:
simp