Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case commf
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'

pp: case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'

pp: case comminl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'

pp: case comminr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'

Tactic:
· simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commf, Iso.inv_hom_id_assoc]

Goal state after:
case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'

case comminl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'

case comminr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'