awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨hX₂.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₂
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₁
⊢ (ofIsInitialLeft F f₁ f₂ h).ι = (F.obj Y₁).map f₂

Tactic:
simpa using (ofIsInitialLeft F f₁ f₂ h).inl_ι

Premises used: CategoryTheory.Functor.PushoutObjObj.inl_ι, CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft
-- 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.obj X₁)
inst_5 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
inst : IsIso ((F.map f₁).app X₂)
sq₁ :
  CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
apply +allowSynthFailures IsPushout.of_horiz_isIso

Premises used: CategoryTheory.IsPushout.of_horiz_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.obj X₁)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
⊢ IsIso ((F.map f₁).app X₂)

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.obj X₁)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
⊢ IsIso ((F.map f₁).app X₂)

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.obj X₁)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
⟨hX₁.hom_ext _ _⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.CommSq.mk
-- 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.obj X₁)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
exact ⟨hX₁.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₂
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
⊢ (ofIsInitialRight F f₁ f₂ h).ι = (F.map f₁).app Y₂

Tactic:
simpa using (ofIsInitialRight F f₁ f₂ h).inr_ι

Premises used: CategoryTheory.Functor.PushoutObjObj.inr_ι, CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight
-- 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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
simp :
  (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr

Tactic:
simp only [Arrow.mk_left]

Premises used: CategoryTheory.Arrow.mk_left
-- 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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr

Tactic:
grind [sq.w, sq₁₂'.isPushout.w]

Premises used: CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.Arrow.Hom.w, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- 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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
hₗ :
  sq₁₂.inl ≫
      map (𝟭 C₃)
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
hᵣ :
  sq₁₂.inr ≫
      map (𝟭 C₃)
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
⊢ map (𝟭 C₃)
        (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
apply PushoutObjObj.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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ sq₁₂.inl ≫
      map (𝟭 C₃)
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
simp [← NatTrans.comp_app, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ sq₁₂.inr ≫
      map (𝟭 C₃)
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
simp [← NatTrans.comp_app, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
simp :
  (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr

Tactic:
simp only [Arrow.mk_left]

Premises used: CategoryTheory.Arrow.mk_left
-- 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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr

Tactic:
grind [sq.w, sq₁₂'.isPushout.w]

Premises used: CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.Arrow.Hom.w, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- 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₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
hₗ :
  sq₁₂.inl ≫
      map (𝟭 C₃)
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
hᵣ :
  sq₁₂.inr ≫
      map (𝟭 C₃)
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
⊢ map (𝟭 C₃)
        (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))

Tactic:
apply PushoutObjObj.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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ sq₁₂.inl ≫
      map (𝟭 C₃)
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : G.PullbackObjObj f₁ f₃
⊢ (G.map f₁.op).app X₃ ≫ (G.obj (op X₁)).map f₃ = (G.obj (op Y₁)).map f₃ ≫ (G.map f₁.op).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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
⊢ sq.π ≫ sq.fst = (G.map f₁.op).app X₃

Tactic:
simp [π]

Premises used: CategoryTheory.Functor.PullbackObjObj.π
-- 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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
⊢ sq.π ≫ sq.snd = (G.obj (op Y₁)).map f₃

Tactic:
simp [π]

Premises used: CategoryTheory.Functor.PullbackObjObj.π
-- 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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
X₂ : C₂
f g : X₂ ⟶ sq.pt
h₁ : f ≫ sq.fst = g ≫ sq.fst
h₂ : f ≫ sq.snd = g ≫ sq.snd
⊢ f = g

Tactic:
sq.isPullback.hom_ext h₁ h₂

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.Functor.PullbackObjObj.isPullback
-- 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 : G.PullbackObjObj f₁ f₃
inst_3 : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (G.map f₁.op).app X₃ ≫ (G.obj (op X₁)).map f₃ = (G.obj (op Y₁)).map f₃ ≫ (G.map f₁.op).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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst_3 : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
h₁ :
  (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).fst =
    pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯ ≫ (ofHasPullback G f₁ f₃).fst
h₂ :
  (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).snd =
    pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯ ≫ (ofHasPullback G f₁ f₃).snd
⊢ (ofHasPullback G f₁ f₃).π = pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯

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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst_3 : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).fst =
    pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯ ≫ (ofHasPullback G f₁ f₃).fst

Tactic:
simp [PullbackObjObj.π, ofHasPullback_fst, ofHasPullback_snd]

Premises used: CategoryTheory.Functor.PullbackObjObj.π, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_snd, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_fst
-- 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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst_3 : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).snd =
    pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯ ≫ (ofHasPullback G f₁ f₃).snd

Tactic:
simp [PullbackObjObj.π, ofHasPullback_fst, ofHasPullback_snd]

Premises used: CategoryTheory.Functor.PullbackObjObj.π, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_snd, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_fst
-- 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 : G.PullbackObjObj f₁ f₃
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst_5 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial.{v₁, u₁} X₁
hX₃ : IsTerminal.{v₂, u₂} ((G.flip.obj X₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)
hY₃ : IsTerminal.{v₂, u₂} ((G.flip.obj Y₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj Y₃) (op X₁) (IsInitial.op C₁ h)
inst : IsIso ((G.obj (op X₁)).map f₃)
sq₁ :
  CommSq ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ IsPullback ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)

Tactic:
apply +allowSynthFailures IsPullback.of_vert_isIso

Premises used: CategoryTheory.IsPullback.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 : G.PullbackObjObj f₁ f₃
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial.{v₁, u₁} X₁
hX₃ : IsTerminal.{v₂, u₂} ((G.flip.obj X₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)
hY₃ : IsTerminal.{v₂, u₂} ((G.flip.obj Y₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj Y₃) (op X₁) (IsInitial.op C₁ h)
⊢ IsIso ((G.obj (op X₁)).map f₃)

Tactic:
isIso_of_isTerminal hX₃ hY₃ _

Premises used: CategoryTheory.Limits.isIso_of_isTerminal