case mp
C : Type u_2
inst✝ : Category 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_2
inst✝ : Category 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
C : Type u_2
inst✝ : Category 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
constructor <;> intro
no goals
case mp
C : Type u_2
inst✝ : Category 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_2
inst✝ : Category 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
exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]