awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ Eq (α := Y ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Y ⟶ pushout f (g ≫ g'))
    (pushout.inl f (g ≫ g') : Y ⟶ pushout f (g ≫ g'))

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_hom (pasteHorizIsPushout _ _ _) _ WalkingSpan.left

Premises used: CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.pasteHorizIsPushout, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
rw :
  Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
rw₁ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    ((g' ≫ pushout.inr f (g ≫ g')) ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
rw₂ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    (g' ≫ pushout.inr f (g ≫ g') ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
rw₃ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    (g' ≫ pushout.inr (pushout.inr f g) g')
rw₄ rw₅ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (g' ≫ pushout.inr (pushout.inr f g) g')
    (g' ≫ pushout.inr (pushout.inr f g) g')
⊢ Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.condition, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ HasPushout (f ≫ f') g

Tactic:
HasColimit.mk {
    cocone := (pushout.cocone f g).pasteVert (pushout.cocone f' (pushout.inl f g)) rfl
    isColimit := pasteVertIsPushout rfl (pushout.isColimit f g)
      (pushout.isColimit f' (pushout.inl f g))
  }

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.PushoutCocone.pasteVert, CategoryTheory.Limits.pushout.isColimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pasteVertIsPushout, CategoryTheory.Limits.pushout.inl, CategoryTheory.Limits.pushout.cocone, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ Eq (α := W ⟶ pushout (Z := pushout f g) f' (pushout.inl f g))
    (pushout.inl (f ≫ f') g ≫ Iso.inv (pushoutRightPushoutInlIso f g f')) (pushout.inl f' (pushout.inl f g))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
rw :
  Eq (α := Z ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
        (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Z ⟶ pushout (f ≫ f') g)
    (pushout.inr (f ≫ f') g : Z ⟶ pushout (f ≫ f') g)
⊢ Eq (α := Z ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Z ⟶ pushout (f ≫ f') g)
    (pushout.inr (f ≫ f') g : Z ⟶ pushout (f ≫ f') g)

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ Eq (α := Z ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
        (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Z ⟶ pushout (f ≫ f') g)
    (pushout.inr (f ≫ f') g : Z ⟶ pushout (f ≫ f') g)

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_hom (pasteVertIsPushout rfl _ _) _ WalkingSpan.right

Premises used: CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.pasteVertIsPushout, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ Eq (α := Z ⟶ pushout (Z := pushout f g) f' (pushout.inl f g))
    (pushout.inr (f ≫ f') g ≫ Iso.inv (pushoutRightPushoutInlIso f g f'))
    (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ WalkingSpan.right

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ Eq (α := W ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inl f' (pushout.inl f g))
        (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      W ⟶ pushout (f ≫ f') g)
    (pushout.inl (f ≫ f') g : W ⟶ pushout (f ≫ f') g)

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom (pasteVertIsPushout rfl _ _) _ WalkingSpan.left

Premises used: CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.pasteVertIsPushout, CategoryTheory.Limits.span, rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
rw :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
        (pushout.inl f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
rw₁ :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (f' ≫ pushout.inl f' (pushout.inl f g))
        (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
rw₂ :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (f' ≫
        CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inl f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
rw₃ rw₄ : Eq (α := Y ⟶ pushout (f ≫ f') g) (f' ≫ pushout.inl (f ≫ f') g) (f' ≫ pushout.inl (f ≫ f') g)
⊢ Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)

Tactic:
rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.condition, CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
⊢ (F.map f₁).app X₂ ≫ (F.obj Y₁).map f₂ = (F.obj X₁).map f₂ ≫ (F.map f₁).app Y₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
⊢ sq.inl ≫ sq.ι = (F.obj Y₁).map f₂

Tactic:
simp [ι]

Premises used: CategoryTheory.Functor.PushoutObjObj.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
⊢ sq.inr ≫ sq.ι = (F.map f₁).app Y₂

Tactic:
simp [ι]

Premises used: CategoryTheory.Functor.PushoutObjObj.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
X₃ : C₃
f g : sq.pt ⟶ X₃
hₗ : sq.inl ≫ f = sq.inl ≫ g
hᵣ : sq.inr ≫ f = sq.inr ≫ g
⊢ f = g

Tactic:
sq.isPushout.hom_ext hₗ hᵣ

Premises used: CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₀ : sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
h₁ : sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι
⊢ sq.flip.ι = sq.ι

Tactic:
apply sq.flip.isPushout.hom_ext

Premises used: CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.Functor.PushoutObjObj.flip, CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₀ : (F.flip.obj Y₂).map f₁ = sq.flip.inl ≫ sq.ι
h₁ : (F.flip.obj Y₂).map f₁ = sq.inr ≫ sq.ι
h₂ : (F.flip.obj Y₂).map f₁ = (F.map f₁).app Y₂
h₃ h₄ : (F.map f₁).app Y₂ = (F.map f₁).app Y₂
⊢ sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι

Tactic:
rw [inl_ι, flip_inl, inr_ι, flip_obj_map]

Premises used: CategoryTheory.Functor.PushoutObjObj.inr_ι, CategoryTheory.Functor.PushoutObjObj.flip_inl, CategoryTheory.Functor.flip_obj_map, CategoryTheory.Functor.PushoutObjObj.inl_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₁ : (F.flip.map f₂).app Y₁ = sq.flip.inr ≫ sq.ι
h₂ : (F.flip.map f₂).app Y₁ = sq.inl ≫ sq.ι
h₃ : (F.flip.map f₂).app Y₁ = (F.obj Y₁).map f₂
h₄ h₅ : (F.obj Y₁).map f₂ = (F.obj Y₁).map f₂
⊢ sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι

Tactic:
rw [inr_ι, flip_inr, inl_ι, flip_map_app]

Premises used: CategoryTheory.Functor.PushoutObjObj.inr_ι, CategoryTheory.Functor.PushoutObjObj.flip_inr, CategoryTheory.Functor.PushoutObjObj.inl_ι, CategoryTheory.Functor.flip_map_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ (F.map f₁).app X₂ ≫ ((e.app Y₁).app X₂).hom = ((e.app X₁).app X₂).hom ≫ (F'.map f₁).app X₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ (F.obj X₁).map f₂ ≫ ((e.app X₁).app Y₂).hom = ((e.app X₁).app X₂).hom ≫ (F'.obj X₁).map f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ sq.inl ≫ Iso.hom (Iso.refl sq.pt) = ((e.app Y₁).app X₂).hom ≫ (e.inv.app Y₁).app X₂ ≫ sq.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ sq.inr ≫ Iso.hom (Iso.refl sq.pt) = ((e.app X₁).app Y₂).hom ≫ (e.inv.app X₁).app Y₂ ≫ sq.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
hₗ : sq.inl ≫ (sq.ofNatIso e).ι = sq.inl ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂
hᵣ : sq.inr ≫ (sq.ofNatIso e).ι = sq.inr ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂
⊢ (sq.ofNatIso e).ι = sq.ι ≫ (e.hom.app Y₁).app Y₂

Tactic:
apply sq.hom_ext

Premises used: CategoryTheory.Functor.PushoutObjObj.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ sq.inl ≫ (sq.ofNatIso e).ι = sq.inl ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂

Tactic:
simp [← (sq.ofNatIso e).inl_ι]

Premises used: CategoryTheory.Functor.PushoutObjObj.ofNatIso, CategoryTheory.Functor.PushoutObjObj.inl_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ sq.inr ≫ (sq.ofNatIso e).ι = sq.inr ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂

Tactic:
simp [← (sq.ofNatIso e).inr_ι]

Premises used: CategoryTheory.Functor.PushoutObjObj.inr_ι, CategoryTheory.Functor.PushoutObjObj.ofNatIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_3 : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
⊢ (F.map f₁).app X₂ ≫ (F.obj Y₁).map f₂ = (F.obj X₁).map f₂ ≫ (F.map f₁).app Y₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
inst_3 : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
hₗ :
  (ofHasPushout F f₁ f₂).inl ≫ (ofHasPushout F f₁ f₂).ι =
    (ofHasPushout F f₁ f₂).inl ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯
hᵣ :
  (ofHasPushout F f₁ f₂).inr ≫ (ofHasPushout F f₁ f₂).ι =
    (ofHasPushout F f₁ f₂).inr ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯
⊢ (ofHasPushout F f₁ f₂).ι = pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
inst_3 : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
⊢ (ofHasPushout F f₁ f₂).inl ≫ (ofHasPushout F f₁ f₂).ι =
    (ofHasPushout F f₁ f₂).inl ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯

Tactic:
simp [PushoutObjObj.ι, ofHasPushout_inl, ofHasPushout_inr]

Premises used: CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inl, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
inst_3 : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
⊢ (ofHasPushout F f₁ f₂).inr ≫ (ofHasPushout F f₁ f₂).ι =
    (ofHasPushout F f₁ f₂).inr ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯

Tactic:
simp [PushoutObjObj.ι, ofHasPushout_inl, ofHasPushout_inr]

Premises used: CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inl, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst_1 : Category.{v₁, u₁} C₁
inst_2 : Category.{v₂, u₂} C₂
inst_3 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst_5 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial.{v₁, u₁} X₁
hX₂ : IsInitial.{v₃, u₃} ((F.flip.obj X₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj X₂) X₁ h
hY₂ : IsInitial.{v₃, u₃} ((F.flip.obj Y₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h
inst : IsIso ((F.obj X₁).map f₂)
sq₁ :
  CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))

Tactic:
apply +allowSynthFailures IsPushout.of_vert_isIso

Premises used: CategoryTheory.IsPushout.of_vert_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial.{v₁, u₁} X₁
hX₂ : IsInitial.{v₃, u₃} ((F.flip.obj X₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj X₂) X₁ h
hY₂ : IsInitial.{v₃, u₃} ((F.flip.obj Y₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h
⊢ IsIso ((F.obj X₁).map f₂)

Tactic:
isIso_of_isInitial hX₂ hY₂ _

Premises used: CategoryTheory.Limits.isIso_of_isInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial.{v₁, u₁} X₁
hX₂ : IsInitial.{v₃, u₃} ((F.flip.obj X₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj X₂) X₁ h
hY₂ : IsInitial.{v₃, u₃} ((F.flip.obj Y₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h
⊢ IsIso ((F.obj X₁).map f₂)

Tactic:
exact isIso_of_isInitial hX₂ hY₂ _

Premises used: CategoryTheory.Limits.isIso_of_isInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial.{v₁, u₁} X₁
hX₂ : IsInitial.{v₃, u₃} ((F.flip.obj X₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj X₂) X₁ h
hY₂ : IsInitial.{v₃, u₃} ((F.flip.obj Y₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))

Tactic:
⟨hX₂.hom_ext _ _⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.CommSq.mk