Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
      Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))

pp: case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P ((pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))

Tactic:
<;>

Goal state after:
case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
      Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))

case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this✝ : HasPullbacksAlong (Over.mk f).hom
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))
⊢ P ((pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))