[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ↑(Adjunction.homEquiv adj A X) u ≫ F.map p = i ≫ ↑(Adjunction.homEquiv adj B Y) v
[PROOFSTEP]
simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ NatTrans.app adj.unit A ≫ F.map (G.map i ≫ v) = i ≫ NatTrans.app adj.unit B ≫ F.map v
[PROOFSTEP]
rw [F.map_comp, Adjunction.unit_naturality_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct sq
⊢ i ≫ ↑(Adjunction.homEquiv adj B X) l.l = ↑(Adjunction.homEquiv adj A X) u
[PROOFSTEP]
rw [← adj.homEquiv_naturality_left, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct sq
⊢ ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = ↑(Adjunction.homEquiv adj B Y) v
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_right, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = u
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_left_symm, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ ↑(Adjunction.homEquiv adj A X).symm (↑(Adjunction.homEquiv adj A X) u) = u
[PROOFSTEP]
apply (adj.homEquiv _ _).left_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = v
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ ↑(Adjunction.homEquiv adj B Y).symm (↑(Adjunction.homEquiv adj B Y) v) = v
[PROOFSTEP]
apply (adj.homEquiv _ _).left_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.LeftInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
        fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X) l.l,
      fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = ↑(Adjunction.homEquiv adj A X) u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = ↑(Adjunction.homEquiv adj B Y) v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.RightInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
        fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X) l.l,
      fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = ↑(Adjunction.homEquiv adj A X) u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = ↑(Adjunction.homEquiv adj B Y) v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v)) ↔ HasLift sq
[PROOFSTEP]
simp only [HasLift.iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty (LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))) ↔
    Nonempty (LiftStruct sq)
[PROOFSTEP]
exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.8583, u_1} C
inst✝¹ : Category.{?u.8587, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
[PROOFSTEP]
rw [right_adjoint_hasLift_iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.8583, u_1} C
inst✝¹ : Category.{?u.8587, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ HasLift ?sq
case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.8583, u_1} C
inst✝¹ : Category.{?u.8587, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ CommSq u (G.map i) p v
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} 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
⊢ ↑(Adjunction.homEquiv adj A X).symm u ≫ p = G.map i ≫ ↑(Adjunction.homEquiv adj B Y).symm v
[PROOFSTEP]
simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} 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
⊢ G.map u ≫ NatTrans.app adj.counit X ≫ p = G.map (u ≫ F.map p) ≫ NatTrans.app adj.counit Y
[PROOFSTEP]
rw [G.map_comp, assoc, Adjunction.counit_naturality]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
l : LiftStruct sq
⊢ G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = ↑(Adjunction.homEquiv adj A X).symm u
[PROOFSTEP]
rw [← adj.homEquiv_naturality_left_symm, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
l : LiftStruct sq
⊢ ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = ↑(Adjunction.homEquiv adj B Y).symm v
[PROOFSTEP]
rw [← adj.homEquiv_naturality_right_symm, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ i ≫ ↑(Adjunction.homEquiv adj B X) l.l = u
[PROOFSTEP]
rw [← adj.homEquiv_naturality_left, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ ↑(Adjunction.homEquiv adj A X) (↑(Adjunction.homEquiv adj A X).symm u) = u
[PROOFSTEP]
apply (adj.homEquiv _ _).right_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = v
[PROOFSTEP]
rw [← adj.homEquiv_naturality_right, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ ↑(Adjunction.homEquiv adj B Y) (↑(Adjunction.homEquiv adj B Y).symm v) = v
[PROOFSTEP]
apply (adj.homEquiv _ _).right_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
⊢ Function.LeftInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X) l.l, fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
      fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = ↑(Adjunction.homEquiv adj A X).symm u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = ↑(Adjunction.homEquiv adj B Y).symm v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} 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
⊢ Function.RightInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X) l.l, fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
      fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = ↑(Adjunction.homEquiv adj A X).symm u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = ↑(Adjunction.homEquiv adj B Y).symm v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} 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
[PROOFSTEP]
simp only [HasLift.iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} 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)
[PROOFSTEP]
exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.18083, u_1} C
inst✝¹ : Category.{?u.18087, u_2} 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
inst✝ : HasLift sq
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
[PROOFSTEP]
rw [left_adjoint_hasLift_iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.18083, u_1} C
inst✝¹ : Category.{?u.18087, u_2} 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
inst✝ : HasLift sq
⊢ HasLift ?sq
case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.18083, u_1} C
inst✝¹ : Category.{?u.18087, u_2} 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
inst✝ : HasLift sq
⊢ CommSq u i (F.map p) v
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p → HasLiftingProperty i (F.map p)
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i (F.map p) → HasLiftingProperty (G.map i) p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ HasLiftingProperty i (F.map p)
[PROOFSTEP]
constructor
[GOAL]
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ HasLiftingProperty (G.map i) p
[PROOFSTEP]
constructor
[GOAL]
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), CommSq.HasLift sq
[PROOFSTEP]
intro f g sq
[GOAL]
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), CommSq.HasLift sq
[PROOFSTEP]
intro f g sq
[GOAL]
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [← sq.left_adjoint_hasLift_iff adj]
[GOAL]
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X).symm f) (G.map i) p (↑(homEquiv adj B Y).symm g))
[PROOFSTEP]
infer_instance
[GOAL]
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [← sq.right_adjoint_hasLift_iff adj]
[GOAL]
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X) f) i (F.map p) (↑(homEquiv adj B Y) g))
[PROOFSTEP]
infer_instance
