-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback_map_diagonal_isPullback :
    IsPullback (pullback.fst _ _ ≫ f)
      (pullback.map f g (f ≫ i) (g ≫ i) _ _ i (Category.id_comp _).symm (Category.id_comp _).symm)
      (diagonal i)
      (pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 _) (Category.comp_id _) (Category.comp_id _))

Proof state:
case w₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) = fst f g ≫ f

Tactic:
simp

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (fst f g ≫ f) ≫ diagonal i = map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯

Tactic:
ext <;> simp [condition]

Result:
no goals

Proof state:
case w₂
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ CommSq (fst f g ≫ f) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)

Tactic:
constructor

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (fst f g ≫ f) ≫ diagonal i = map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ IsPullback (fst f g ≫ f) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯) (diagonal i)
    (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)

Tactic:
apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm

Result:
case w₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) = fst f g ≫ f

case w₂
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯

C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ CommSq (fst f g ≫ f) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)