-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
theorem pullback_map [HasPullbacks C]
    [IsStableUnderBaseChange P] [P.IsStableUnderComposition] {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₂ (𝟙 _) ((Category.comp_id _).trans e₁)
        ((Category.comp_id _).trans e₂))

Proof state:
case hf
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left

case hg
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P ((Over.pullback g').map (Over.homMk i₁ ⋯)).left

Tactic:
exacts [baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
  baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left

Tactic:
ext <;> dsimp <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
rw [this]

Result:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯)

Tactic:
have :
  pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁)
      ((Category.comp_id _).trans e₂) =
    ((pullbackSymmetry _ _).hom ≫
        ((Over.pullback _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
      (pullbackSymmetry _ _).hom ≫
        ((Over.pullback g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := by
  ext <;> dsimp <;> simp

Result:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left)

Tactic:
apply P.comp_mem <;> rw [P.cancel_left_of_respectsIso]

Result:
case hf
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left

case hg
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
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) ⋯ ⋯ =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
⊢ P ((Over.pullback g').map (Over.homMk i₁ ⋯)).left