∀ {ρ : Type} [inst : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)]
  [inst_1 : Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)]
  [inst_2 : Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)]
  [inst_3 : Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)]
  (_x : (_ : Mathlib.Tactic.BicategoryLike.Mor₁) ×' Mathlib.Tactic.BicategoryLike.NormalExpr),
  Mathlib.Tactic.BicategoryLike.evalWhiskerLeft._unary _x =
    PSigma.casesOn _x fun a a_1 =>
      match a, a_1 with
      | f, Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α => do
        let __do_lift ← Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.whiskerLeftM f α
        let __do_lift ← Mathlib.Tactic.BicategoryLike.MonadNormalExpr.nilM __do_lift
        let __do_lift_1 ← Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftNil f α
        pure { expr := __do_lift, proof := __do_lift_1 }
      | Mathlib.Tactic.BicategoryLike.Mor₁.of f, Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs => do
        let η' ← Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft.whiskerLeftM f η
        let __discr ← Mathlib.Tactic.BicategoryLike.evalWhiskerLeft._unary ⟨Mathlib.Tactic.BicategoryLike.Mor₁.of f, ηs⟩
        match __discr with
          | { expr := θ, proof := e_θ } => do
            let __do_lift ←
              Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.whiskerLeftM (Mathlib.Tactic.BicategoryLike.Mor₁.of f) α
            let η'' ← Mathlib.Tactic.BicategoryLike.MonadNormalExpr.consM __do_lift η' θ
            let __do_lift ← Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftOfCons f α η ηs θ e_θ
            pure { expr := η'', proof := __do_lift }
      | Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g, η => do
        let __discr ← Mathlib.Tactic.BicategoryLike.evalWhiskerLeft._unary ⟨g, η⟩
        match __discr with
          | { expr := θ, proof := e_θ } => do
            let __discr ← Mathlib.Tactic.BicategoryLike.evalWhiskerLeft._unary ⟨f, θ⟩
            match __discr with
              | { expr := ι, proof := e_ι } => do
                let h ← η.srcM
                let h' ← η.tgtM
                let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.associatorInvM f g h'
                let __discr ← Mathlib.Tactic.BicategoryLike.evalComp ι __do_lift
                match __discr with
                  | { expr := ι', proof := e_ι' } => do
                    let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.associatorM f g h
                    let __discr ← Mathlib.Tactic.BicategoryLike.evalComp __do_lift ι'
                    match __discr with
                      | { expr := ι'', proof := e_ι'' } => do
                        let __do_lift ←
                          Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftComp f g η θ ι ι' ι'' e_θ e_ι
                              e_ι' e_ι''
                        pure { expr := ι'', proof := __do_lift }
      | Mathlib.Tactic.BicategoryLike.Mor₁.id e a, η => do
        let f ← η.srcM
        let g ← η.tgtM
        let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorInvM g
        let __discr ← Mathlib.Tactic.BicategoryLike.evalComp η __do_lift
        match __discr with
          | { expr := η', proof := e_η' } => do
            let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorM f
            let __discr ← Mathlib.Tactic.BicategoryLike.evalComp __do_lift η'
            match __discr with
              | { expr := η'', proof := e_η'' } => do
                let __do_lift ← Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftId η η' η'' e_η' e_η''
                pure { expr := η'', proof := __do_lift }