C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g'))
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g'))
have :
  pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁)
      ((Category.comp_id _).trans e₂) =
    ((pullbackSymmetry _ _).hom ≫
        ((baseChange _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
      (pullbackSymmetry _ _).hom ≫
        ((baseChange g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left :=
  by apply pullback.hom_ext <;> dsimp <;> simp
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left)
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g'))
rw [this]
case a
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left

case a
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((baseChange g').map (Over.homMk i₁)).left
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left)
apply hP' <;> rw [hP.respectsIso.cancel_left_isIso]
no goals
case a
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left

case a
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((baseChange g').map (Over.homMk i₁)).left
exacts [hP.baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
  hP.baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.32461
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
apply pullback.hom_ext <;> dsimp <;> simp