[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.op ≫ g.op = h.op ≫ f.op
[PROOFSTEP]
simp only [← op_comp, p.w]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.unop ≫ g.unop = h.unop ≫ f.unop
[PROOFSTEP]
simp only [← unop_comp, p.w]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
D : Type u_2
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i
[PROOFSTEP]
simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w
[GOAL]
C : Type u_1
inst✝ : Category.{?u.5324, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ p.op ≫ l.l.op = g.op
[PROOFSTEP]
rw [← op_comp, l.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.5324, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ l.l.op ≫ i.op = f.op
[PROOFSTEP]
rw [← op_comp, l.fac_left]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.6224, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ p.unop ≫ l.l.unop = g.unop
[PROOFSTEP]
rw [← unop_comp, l.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.6224, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ l.l.unop ≫ i.unop = f.unop
[PROOFSTEP]
rw [← unop_comp, l.fac_left]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7227, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse unop op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7227, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse unop op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.8602, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse op unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.8602, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse op unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.10063, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : LiftStruct sq
⊢ l₁ = l₂
[PROOFSTEP]
ext
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10063, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : LiftStruct sq
⊢ l₁.l = l₂.l
[PROOFSTEP]
rw [← cancel_epi i]
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10063, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : LiftStruct sq
⊢ i ≫ l₁.l = i ≫ l₂.l
[PROOFSTEP]
simp only [LiftStruct.fac_left]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.10732, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Mono p
l₁ l₂ : LiftStruct sq
⊢ l₁ = l₂
[PROOFSTEP]
ext
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10732, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Mono p
l₁ l₂ : LiftStruct sq
⊢ l₁.l = l₂.l
[PROOFSTEP]
rw [← cancel_mono p]
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10732, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Mono p
l₁ l₂ : LiftStruct sq
⊢ l₁.l ≫ p = l₂.l ≫ p
[PROOFSTEP]
simp only [LiftStruct.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ Nonempty (LiftStruct sq)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq → Nonempty (LiftStruct sq)
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) → HasLift sq
[PROOFSTEP]
exacts [fun h => h.exists_lift, fun h => mk h]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ HasLift (_ : CommSq g.op p.op i.op f.op)
[PROOFSTEP]
rw [iff, iff]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) ↔ Nonempty (LiftStruct (_ : CommSq g.op p.op i.op f.op))
[PROOFSTEP]
exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
sq✝ : CommSq f✝ i✝ p✝ g✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ HasLift (_ : CommSq g.unop p.unop i.unop f.unop)
[PROOFSTEP]
rw [iff, iff]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
sq✝ : CommSq f✝ i✝ p✝ g✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) ↔ Nonempty (LiftStruct (_ : CommSq g.unop p.unop i.unop f.unop))
[PROOFSTEP]
exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun
