C : Type u_4
D : Type u_1
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Nonempty
      (LiftStruct
        (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))) ↔
    Nonempty (LiftStruct sq)
C : Type u_4
D : Type u_1
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v)) ↔
    HasLift sq
simp only [HasLift.iff]
no goals
C : Type u_4
D : Type u_1
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Nonempty
      (LiftStruct
        (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))) ↔
    Nonempty (LiftStruct sq)
exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm