{P : Sort u} →
  {e : Lean.Expr} →
    {isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift} →
      {f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁} →
        {η θ : Mathlib.Tactic.BicategoryLike.Mor₂} →
          {e' : Lean.Expr} →
            {isoLift?' : Option Mathlib.Tactic.BicategoryLike.IsoLift} →
              {f₁' g₁' f₂' g₂' : Mathlib.Tactic.BicategoryLike.Mor₁} →
                {η' θ' : Mathlib.Tactic.BicategoryLike.Mor₂} →
                  Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ =
                      Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e' isoLift?' f₁' g₁' f₂' g₂' η' θ' →
                    (e = e' → isoLift? = isoLift?' → f₁ = f₁' → g₁ = g₁' → f₂ = f₂' → g₂ = g₂' → η = η' → θ = θ' → P) →
                      P