C : Type u_1
inst✝ : Category C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
h : HasLiftingProperty i p
f : Y.op ⟶ B.op
g : X.op ⟶ A.op
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift (_ : CommSq g.unop i p f.unop)
C : Type u_1
inst✝ : Category C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
h : HasLiftingProperty i p
f : Y.op ⟶ B.op
g : X.op ⟶ A.op
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift sq
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
no goals
C : Type u_1
inst✝ : Category C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
h : HasLiftingProperty i p
f : Y.op ⟶ B.op
g : X.op ⟶ A.op
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift (_ : CommSq g.unop i p f.unop)
infer_instance