∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η : Mathlib.Tactic.BicategoryLike.Mor₂) (e_1 : Lean.Expr) (isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift)
  (f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (η_1 : Mathlib.Tactic.BicategoryLike.Mor₂),
  (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η =
      Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e_1 isoLift?_1 f_1 g_1 h_1 η_1) =
    (e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1)