-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalWhiskerLeft.eq_def : ∀ {ρ : 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₁) (x_1 : Mathlib.Tactic.BicategoryLike.NormalExpr),
  Mathlib.Tactic.BicategoryLike.evalWhiskerLeft x x_1 =
    match x, x_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 __x ← Mathlib.Tactic.BicategoryLike.evalWhiskerLeft (Mathlib.Tactic.BicategoryLike.Mor₁.of f) ηs
      match __x 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 __x ← Mathlib.Tactic.BicategoryLike.evalWhiskerLeft g η
      match __x with
        | { expr := θ, proof := e_θ } => do
          let __x ← Mathlib.Tactic.BicategoryLike.evalWhiskerLeft f θ
          match __x with
            | { expr := ι, proof := e_ι } => do
              let h ← η.srcM
              let h' ← η.tgtM
              let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.associatorInvM f g h'
              let __x ← Mathlib.Tactic.BicategoryLike.evalComp ι __do_lift
              match __x with
                | { expr := ι', proof := e_ι' } => do
                  let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.associatorM f g h
                  let __x ← Mathlib.Tactic.BicategoryLike.evalComp __do_lift ι'
                  match __x 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 __x ← Mathlib.Tactic.BicategoryLike.evalComp η __do_lift
      match __x with
        | { expr := η', proof := e_η' } => do
          let __do_lift ← Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorM f
          let __x ← Mathlib.Tactic.BicategoryLike.evalComp __do_lift η'
          match __x with
            | { expr := η'', proof := e_η'' } => do
              let __do_lift ← Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftId η η' η'' e_η' e_η''
              pure { expr := η'', proof := __do_lift }