awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
rw :
  Eq (α := Opposite.op Y ⟶ pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
    (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.diagonal f.op)
⊢ Eq (α := Opposite.op Y ⟶ Opposite.op (codiagonalObj f))
    (Quiver.Hom.op (codiagonal f) : Opposite.op Y ⟶ Opposite.op (codiagonalObj f))
    (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
        (pullback.diagonal f.op) (Iso.hom (pullbackIsoOpPushout f.op f.op)) :
      Opposite.op Y ⟶ Opposite.op (pushout f.op.unop f.op.unop))

Tactic:
rw [← Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
h₀ :
  CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.fst f.op f.op) =
    CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.diagonal f.op) (pullback.fst f.op f.op)
h₁ :
  CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.snd f.op f.op) =
    CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.diagonal f.op) (pullback.snd f.op f.op)
⊢ Eq (α := Opposite.op Y ⟶ pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
    (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.diagonal f.op)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.fst f.op f.op) =
    CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.diagonal f.op) (pullback.fst f.op f.op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.snd f.op f.op) =
    CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.diagonal f.op) (pullback.snd f.op f.op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ IsSplitEpi (X := codiagonalObj f) (codiagonal f)

Tactic:
⟨⟨⟨pushout.inl _ _, inl_codiagonal f⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.pushout.inl_codiagonal, CategoryTheory.SplitEpi.mk, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Limits.pushout.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ IsSplitMono (Y := pushout f f) (inl f f)

Tactic:
⟨⟨⟨codiagonal f, inl_codiagonal f⟩⟩⟩

Premises used: CategoryTheory.Limits.pushout.codiagonal, CategoryTheory.SplitMono.mk, Nonempty.intro, CategoryTheory.Limits.pushout.inl_codiagonal, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ IsSplitMono (Y := pushout f f) (inr f f)

Tactic:
⟨⟨⟨codiagonal f, inr_codiagonal f⟩⟩⟩

Premises used: CategoryTheory.Limits.pushout.codiagonal, CategoryTheory.SplitMono.mk, CategoryTheory.Limits.pushout.inr_codiagonal, Nonempty.intro, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
inst_2 : Epi f
rw : IsIso (X := codiagonalObj f) (inv (inl f f))
⊢ IsIso (X := codiagonalObj f) (codiagonal f)

Tactic:
rw [(IsIso.inv_eq_of_hom_inv_id (inl_codiagonal f)).symm]

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id, CategoryTheory.Limits.pushout.inl_codiagonal, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
inst_2 : Epi f
⊢ IsIso (X := codiagonalObj f) (inv (inl f f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
H : IsIso (X := codiagonalObj f) (codiagonal f)
Z : C
x x_1 : Y ⟶ Z
e : f ≫ x = f ≫ x_1
⊢ CategoryStruct.comp (Y := codiagonalObj f) (inl f f) (codiagonal f) =
    CategoryStruct.comp (Y := codiagonalObj f) (inr f f) (codiagonal f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
H : IsIso (X := codiagonalObj f) (codiagonal f)
Z : C
x x_1 : Y ⟶ Z
e : f ≫ x = f ≫ x_1
rw : CategoryStruct.comp (Y := pushout f f) (inl f f) (desc x x_1 e) = x_1
rw₁ : CategoryStruct.comp (Y := pushout f f) (inr f f) (desc x x_1 e) = x_1
rw₂ rw₃ : x_1 = x_1
⊢ x = x_1

Tactic:
rw [← inl_desc _ _ e, (cancel_mono (g := inl f f) (h := inr f f)
    (codiagonal f)).mp (by simp), inr_desc]

Premises used: CategoryTheory.Limits.pushout.inr_desc, CategoryTheory.Limits.pushout.codiagonal, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Limits.pushout.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ i ≫ f = 𝟙 S ≫ i ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ i ≫ g = 𝟙 S ≫ i ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (i ≫ f) ≫ 𝟙 X = i ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (i ≫ g) ≫ 𝟙 Y = i ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
rw :
  IsPullback.{v_1, u_1} (C := Cᵒᵖ) (P := Opposite.op (pushout f g)) (X := Opposite.op T) (Y :=
    Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z := Opposite.op (pushout i i)) (Quiver.Hom.op (f ≫ pushout.inl f g))
    (Quiver.Hom.op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯)) (Quiver.Hom.op (pushout.codiagonal i))
    (Quiver.Hom.op (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯))
⊢ IsPushout (Z := pushout i i) (X := pushout (i ≫ f) (i ≫ g)) (P := pushout f g)
    (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯) (pushout.codiagonal i)
    (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯) (f ≫ pushout.inl f g)

Tactic:
rw [← IsPullback.op_iff]

Premises used: CategoryTheory.IsPullback.op_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
simp :
  IsPullback (P := Opposite.op (pushout f g)) (Y := Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z :=
    Opposite.op (pushout i i)) (Quiver.Hom.op (pushout.inl f g) ≫ f.op : Opposite.op (pushout f g) ⟶ Opposite.op T)
    (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op)
        (Iso.inv (pullbackIsoOpPushout f.op g.op))
        (CategoryStruct.comp (Y :=
          pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op)
            (g.op ≫ i.op))
          (pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯)
          (Iso.hom (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))) :
      Opposite.op (pushout f g) ⟶ Opposite.op (pushout (i ≫ f) (i ≫ g)))
    (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op S) i.op)
        (pullback.diagonal i.op) (Iso.hom (pullbackIsoOpPushout i.op i.op)) :
      Opposite.op T ⟶ Opposite.op (pushout i i))
    (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op))
        (Iso.inv (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))
        (CategoryStruct.comp (Y :=
          pullback.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op T) (Z := Opposite.op S) i.op i.op)
          (pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯)
          (Iso.hom (pullbackIsoOpPushout i.op i.op))) :
      Opposite.op (pushout (i ≫ f) (i ≫ g)) ⟶ Opposite.op (pushout i i))
⊢ IsPullback.{v_1, u_1} (C := Cᵒᵖ) (P := Opposite.op (pushout f g)) (X := Opposite.op T) (Y :=
    Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z := Opposite.op (pushout i i)) (Quiver.Hom.op (f ≫ pushout.inl f g))
    (Quiver.Hom.op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯)) (Quiver.Hom.op (pushout.codiagonal i))
    (Quiver.Hom.op (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯))

Tactic:
simp only [op_pushoutMap, Quiver.Hom.unop_op, op_comp, unop_comp, op_id, pushout.op_codiagonal]

Premises used: CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.Limits.op_pushoutMap, CategoryTheory.unop_comp, CategoryTheory.Limits.pushout.op_codiagonal, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ Eq (α := pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op ⟶ Opposite.op T)
    ((pullback.fst f.op g.op ≫ f.op) ≫ Iso.hom (Iso.refl (Opposite.op T)))
    (Iso.hom (pullbackIsoOpPushout f.op g.op) ≫ Quiver.Hom.op (pushout.inl f g) ≫ f.op)

Tactic:
simp [← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ Eq (α :=
    pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op ⟶
      Opposite.op (pushout (i ≫ f) (i ≫ g)))
    (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op))
        (pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯)
        (Iso.hom (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op))) :
      pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op ⟶
        Opposite.op (pushout (i ≫ f) (i ≫ g)))
    (Iso.hom (pullbackIsoOpPushout f.op g.op) ≫
        CategoryStruct.comp (Y :=
          pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op)
          (Iso.inv (pullbackIsoOpPushout f.op g.op))
          (CategoryStruct.comp (Y :=
            pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op)
              (g.op ≫ i.op))
            (pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯)
            (Iso.hom (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))) :
      pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op ⟶
        Opposite.op (pushout (i ≫ f) (i ≫ g)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ Eq (α := Opposite.op T ⟶ Opposite.op (pushout i i))
    (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op S) i.op)
        (pullback.diagonal i.op) (Iso.hom (pullbackIsoOpPushout i.op i.op)) :
      Opposite.op T ⟶ Opposite.op (pushout i i))
    (Iso.hom (Iso.refl (Opposite.op T)) ≫
        CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op S) i.op)
          (pullback.diagonal i.op) (Iso.hom (pullbackIsoOpPushout i.op i.op)) :
      Opposite.op T ⟶ Opposite.op (pushout i i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ Eq (α :=
    pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op) ⟶
      Opposite.op (pushout i i))
    (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op S) i.op)
        (pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯)
        (Iso.hom (pullbackIsoOpPushout i.op i.op)) :
      pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op) ⟶
        Opposite.op (pushout i i))
    (Iso.hom (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)) ≫
        CategoryStruct.comp (Y :=
          pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op)
            (g.op ≫ i.op))
          (Iso.inv (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))
          (CategoryStruct.comp (Y :=
            pullback.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op T) (Z := Opposite.op S) i.op i.op)
            (pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯)
            (Iso.hom (pullbackIsoOpPushout i.op i.op))) :
      pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op) ⟶
        Opposite.op (pushout i i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPullback (P := Opposite.op (pushout f g)) (Y := Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z :=
    Opposite.op (pushout i i)) (Quiver.Hom.op (pushout.inl f g) ≫ f.op : Opposite.op (pushout f g) ⟶ Opposite.op T)
    (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op)
        (Iso.inv (pullbackIsoOpPushout f.op g.op))
        (CategoryStruct.comp (Y :=
          pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op)
            (g.op ≫ i.op))
          (pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯)
          (Iso.hom (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))) :
      Opposite.op (pushout f g) ⟶ Opposite.op (pushout (i ≫ f) (i ≫ g)))
    (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op S) i.op)
        (pullback.diagonal i.op) (Iso.hom (pullbackIsoOpPushout i.op i.op)) :
      Opposite.op T ⟶ Opposite.op (pushout i i))
    (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op))
        (Iso.inv (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))
        (CategoryStruct.comp (Y :=
          pullback.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op T) (Z := Opposite.op S) i.op i.op)
          (pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯)
          (Iso.hom (pullbackIsoOpPushout i.op i.op))) :
      Opposite.op (pushout (i ≫ f) (i ≫ g)) ⟶ Opposite.op (pushout i i))

Tactic:
exact .of_iso (pullback_map_diagonal_isPullback f.op g.op i.op)
    (pullbackIsoOpPushout _ _) (.refl _) (pullbackIsoOpPushout _ _) (pullbackIsoOpPushout _ _)
    (by simp [← Iso.inv_comp_eq]) (by simp) (by simp) (by simp)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
⊢ ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i

Tactic:
have heq (i) : d.inj i ≫ e.hom.hom = c.inj i := e.hom.w ⟨i⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
refine : t.fst ≫ c.inj i = t.snd ≫ c.inj j
⊢ t.pt ⟶ (s hij).pt

Tactic:
refine PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ?_

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.IsLimit.lift, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
⊢ t.fst ≫ c.inj i = t.snd ≫ c.inj j

Tactic:
simp [← heq, t.condition_assoc]

Premises used: CategoryTheory.Limits.PullbackCone.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
u : t.pt ⟶ (s hij).pt := PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ⋯
⊢ Nonempty (IsInitial.{v, u} t.pt)

Tactic:
⟨(H hij).ofIso ⟨(H hij).to t.pt, u, (H hij).hom_ext _ _, ?_⟩⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Iso.mk, CategoryTheory.Limits.Cone.pt, Nonempty.intro, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.IsInitial.ofIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
u : t.pt ⟶ (s hij).pt := PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ⋯
refine : u ≫ (H hij).to t.pt = 𝟙 t.pt
⊢ Nonempty (IsInitial.{v, u} t.pt)

Tactic:
refine ⟨(H hij).ofIso ⟨(H hij).to t.pt, u, (H hij).hom_ext _ _, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
u : t.pt ⟶ (s hij).pt := PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ⋯
⊢ u ≫ (H hij).to t.pt = 𝟙 t.pt

Tactic:
PullbackCone.IsLimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
u : t.pt ⟶ (s hij).pt := PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ⋯
refine_1 : (u ≫ (H hij).to t.pt) ≫ t.fst = 𝟙 t.pt ≫ t.fst
refine_2 : (u ≫ (H hij).to t.pt) ≫ t.snd = 𝟙 t.pt ≫ t.snd
⊢ u ≫ (H hij).to t.pt = 𝟙 t.pt

Tactic:
refine PullbackCone.IsLimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
u : t.pt ⟶ (s hij).pt := PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ⋯
⊢ (u ≫ (H hij).to t.pt) ≫ t.fst = 𝟙 t.pt ≫ t.fst

Tactic:
simp [show (H hij).to (X i) = (s hij).fst from (H hij).hom_ext _ _, u]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.IsInitial.to