∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} {h : x ⟶ c},
  Nonempty ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan →
    CategoryTheory.Bicategory.LanLift.CommuteWith f g h