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 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_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 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
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 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'
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 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_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 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
exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]