Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, 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 ≫ i = (g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)

pp: case refine_1.refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, 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) ⋯ ⋯)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i

pp: case refine_1.refine_4
C : Type u_1
inst✝⁵ : Category.{v_1, 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) ⋯ ⋯)
⊢ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i) =
    (congrHom ⋯ ?refine_1.refine_2).hom ≫
      map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯

pp: case refine_1.refine_5
C : Type u_1
inst✝⁵ : Category.{v_1, 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) ⋯ ⋯)
⊢ IsIso
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
      (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
      (𝟙 T) (congrHom ⋯ ?refine_1.refine_2).hom (𝟙 (diagonalObj i)) ?refine_1.refine_3 ?refine_1.refine_4)

Tactic:
· rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]

Goal state after:
case refine_1.refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, 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) ⋯ ⋯)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i

case refine_1.refine_4
C : Type u_1
inst✝⁵ : Category.{v_1, 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) ⋯ ⋯)
⊢ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i) =
    (congrHom ⋯ ⋯).hom ≫
      map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯

case refine_1.refine_5
C : Type u_1
inst✝⁵ : Category.{v_1, 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) ⋯ ⋯)
⊢ IsIso
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
      (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
      (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ?refine_1.refine_3 ?refine_1.refine_4)