[GOAL]
C : Type u_1
inst✝ : Category.{?u.598, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
hip : HasLiftingProperty i p
⊢ CommSq.HasLift sq
[PROOFSTEP]
apply hip.sq_hasLift
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift sq
[PROOFSTEP]
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift (_ : CommSq g.unop i p f.unop)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [CommSq.HasLift.iff_op]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i.unop.op p.unop.op f.op)
[PROOFSTEP]
simp only [Quiver.Hom.op_unop]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i p f.op)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.3772, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ inv i ≫ f = f
[PROOFSTEP]
simp only [IsIso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.3772, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (inv i ≫ f) ≫ p = g
[PROOFSTEP]
simp only [sq.w, assoc, IsIso.inv_hom_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4638, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ g ≫ inv p = f
[PROOFSTEP]
simp only [← sq.w_assoc, IsIso.hom_inv_id, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4638, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (g ≫ inv p) ≫ p = g
[PROOFSTEP]
simp only [assoc, IsIso.inv_hom_id, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
⊢ CommSq.HasLift sq
[PROOFSTEP]
have fac := sq.w
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = (i ≫ i') ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [assoc] at fac 
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact
  CommSq.HasLift.mk'
    { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
      fac_left := by simp only [assoc, CommSq.fac_left]
      fac_right := by simp only [CommSq.fac_right] }
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ (i ≫ i') ≫ CommSq.lift (_ : CommSq (CommSq.lift (_ : CommSq f i p (i' ≫ g))) i' p g) = f
[PROOFSTEP]
simp only [assoc, CommSq.fac_left]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.5681, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ CommSq.lift (_ : CommSq (CommSq.lift (_ : CommSq f i p (i' ≫ g))) i' p g) ≫ p = g
[PROOFSTEP]
simp only [CommSq.fac_right]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
⊢ CommSq.HasLift sq
[PROOFSTEP]
have fac := sq.w
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : f ≫ p ≫ p' = i ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [← assoc] at fac 
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
let _ := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
x✝ : B ⟶ X := CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g)))
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact
  CommSq.HasLift.mk'
    { l := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
      fac_left := by simp only [CommSq.fac_left]
      fac_right := by simp only [CommSq.fac_right_assoc, CommSq.fac_right] }
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
x✝ : B ⟶ X := CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g)))
⊢ i ≫ CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g))) = f
[PROOFSTEP]
simp only [CommSq.fac_left]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.7264, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i p'
f : A ⟶ X
g : B ⟶ Y'
sq : CommSq f i (p ≫ p') g
fac : (f ≫ p) ≫ p' = i ≫ g
x✝ : B ⟶ X := CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g)))
⊢ CommSq.lift (_ : CommSq f i p (CommSq.lift (_ : CommSq (f ≫ p) i p' g))) ≫ p ≫ p' = g
[PROOFSTEP]
simp only [CommSq.fac_right_assoc, CommSq.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p
[PROOFSTEP]
rw [Arrow.iso_w' e]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty (e.inv.left ≫ i ≫ e.hom.right) p
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i p'
[PROOFSTEP]
rw [Arrow.iso_w' e]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i (e.inv.left ≫ p ≫ e.hom.right)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p → HasLiftingProperty i' p
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i' p → HasLiftingProperty i p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i' p
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B'✝ X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i'✝ : B✝ ⟶ B'✝
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i' p
⊢ HasLiftingProperty i p
[PROOFSTEP]
exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i p'
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p → HasLiftingProperty i p'
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p' → HasLiftingProperty i p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i p'
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ B' X✝ Y✝ Y'✝ : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p'✝ : Y✝ ⟶ Y'✝
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p'
⊢ HasLiftingProperty i p
[PROOFSTEP]
exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]
