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

case right
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.diagonal P f → MorphismProperty.diagonal P (f ≫ e.hom)
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ RespectsIso (MorphismProperty.diagonal P)
constructor
case left
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ MorphismProperty.diagonal P (e.hom ≫ f)
case left
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.diagonal P f → MorphismProperty.diagonal P (e.hom ≫ f)
introv H
no goals
case left
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ MorphismProperty.diagonal P (e.hom ≫ f)
rwa [diagonal_iff, pullback.diagonal_comp, hP.cancel_left_isIso, hP.cancel_left_isIso,
  ← hP.cancel_right_isIso _
    (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)),
  ← pullback.condition, hP.cancel_left_isIso]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f
simp
no goals
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f
simp
case right
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : MorphismProperty.diagonal P f
⊢ MorphismProperty.diagonal P (f ≫ e.hom)
case right
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.diagonal P f → MorphismProperty.diagonal P (f ≫ e.hom)
introv H
case right
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : MorphismProperty.diagonal P f
⊢ P (pullback.diagonal (f ≫ e.hom))
case right
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : MorphismProperty.diagonal P f
⊢ MorphismProperty.diagonal P (f ≫ e.hom)
delta diagonal
no goals
case right
C : Type u
inst✝² : Category C
D : Type ?u.69245
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : MorphismProperty.diagonal P f
⊢ P (pullback.diagonal (f ≫ e.hom))
rwa [pullback.diagonal_comp, hP.cancel_right_isIso]