∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T] (sq : Lattice.BicartSq x₁ x₂ x₃ x₄),
  CategoryTheory.CommSq (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
    (CategoryTheory.homOfLE ⋯)