case left
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), universally P f → universally P (e.hom ≫ f)

case right
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), universally P f → universally P (f ≫ e.hom)
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
⊢ RespectsIso (universally P)
constructor
case left
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ P f'
case left
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), universally P f → universally P (e.hom ≫ f)
intro X Y Z e f hf X' Z' i₁ i₂ f' H
case left
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ P f'
case left
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ P f'
have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
  IsPullback.of_horiz_isIso
    ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
no goals
case left
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ P f'
exact hf _ _ _
  (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H)
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv
rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ IsPullback f' ?m.83573 ?m.83574 f
simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
⊢ P f'
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), universally P f → universally P (f ≫ e.hom)
intro X Y Z e f hf X' Z' i₁ i₂ f' H
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ P f'
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
⊢ P f'
have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv :=
  IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
no goals
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ P f'
exact hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id,
  Category.comp_id, Category.comp_id] using H.paste_horiz this)
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.81425
inst✝ : Category D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ IsPullback f' ?m.85108 ?m.85109 f
simpa only [Category.assoc, Iso.hom_inv_id,
Category.comp_id, Category.comp_id] using H.paste_horiz this