-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
/-- Informally, this is a special case of `pullback_map_diagonal_isPullback` for `T = X`. -/
lemma pullback_lift_diagonal_isPullback (g : Y ⟶ X) (f : X ⟶ S) :
    IsPullback g (pullback.lift (𝟙 Y) g (by simp)) (diagonal f)
      (pullback.map (g ≫ f) f f f g (𝟙 X) (𝟙 S) (by simp) (by simp))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯)).symm
⊢ IsPullback g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
apply IsPullback.of_iso_pullback _
    (e ≪≫ pullbackDiagonalMapIdIso (T := X) (S := S) g (𝟙 X) f ≪≫ asIso (pullback.fst _ _)).symm

Result:
case w₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯)).symm
⊢ (e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
      fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    g

case w₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯)).symm
⊢ (e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯

C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯)).symm
⊢ CommSq g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Proof state:
C : Type u_1
inst✝⁵ : Category.{?u.943176, u_1} C
X Y Z : 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) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ (g ≫ f) ≫ 𝟙 S = 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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯)).symm
⊢ g ≫ diagonal f = lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯)).symm
⊢ (e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
      fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    g

Tactic:
simp [e]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
⊢ IsPullback g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
let i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom rfl (by simp)

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ IsPullback g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)