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 : 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:
exact isIso_of_isTerminal hX₃ hY₃ _

Premises used: CategoryTheory.Limits.isIso_of_isTerminal
-- 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)
⊢ 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₃)

Tactic:
⟨hY₃.hom_ext _ _⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.Limits.IsTerminal.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₁ : 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)
⊢ 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₃)

Tactic:
exact ⟨hY₃.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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
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₁
⊢ (ofIsInitial G f₁ f₃ h).π = (G.obj (op Y₁)).map f₃

Tactic:
simpa using (ofIsInitial G f₁ f₃ h).π_snd

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

Tactic:
apply +allowSynthFailures IsPullback.of_horiz_isIso

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

Tactic:
isIso_of_isTerminal hY₁ hX₁ _

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

Tactic:
exact isIso_of_isTerminal hY₁ hX₁ _

Premises used: CategoryTheory.Limits.isIso_of_isTerminal
-- 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.obj (op X₁))
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal.{v₃, u₃} Y₃
hX₁ : IsTerminal.{v₂, u₂} ((G.obj (op X₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op X₁)) Y₃ h
hY₁ : IsTerminal.{v₂, u₂} ((G.obj (op Y₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h
⊢ CommSq (𝟙 ((G.obj (op X₁)).obj X₃)) ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃))
    ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)

Tactic:
⟨hX₁.hom_ext _ _⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.Limits.IsTerminal.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₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal.{v₃, u₃} Y₃
hX₁ : IsTerminal.{v₂, u₂} ((G.obj (op X₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op X₁)) Y₃ h
hY₁ : IsTerminal.{v₂, u₂} ((G.obj (op Y₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h
⊢ CommSq (𝟙 ((G.obj (op X₁)).obj X₃)) ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃))
    ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app 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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal.{v₃, u₃} Y₃
⊢ (ofIsTerminal G f₁ f₃ h).π = (G.map f₁.op).app X₃

Tactic:
simpa using (ofIsTerminal G f₁ f₃ h).π_fst

Premises used: CategoryTheory.Functor.PullbackObjObj.π_fst, CategoryTheory.Functor.PullbackObjObj.ofIsTerminal
-- 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 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
simp :
  sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left ≫ (G.obj (op f₁'.left)).map f₃.hom =
    sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right ≫ (G.map f₁'.hom.op).app f₃.right
⊢ (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left) ≫ (G.obj (op f₁'.left)).map f₃.hom =
    (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ≫ (G.map f₁'.hom.op).app f₃.right

Tactic:
simp [Arrow.mk_right]

Premises used: CategoryTheory.Arrow.mk_right
-- 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 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left ≫ (G.obj (op f₁'.left)).map f₃.hom =
    sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right ≫ (G.map f₁'.hom.op).app f₃.right

Tactic:
grind [sq.w, sq₁₃.isPullback.w]

Premises used: CategoryTheory.Arrow.Hom.w, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, 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₁_1 : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃_1 : X₃ ⟶ Y₃
sq_1 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
h₁ :
  (map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.fst
h₂ :
  (map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.snd
⊢ map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)

Tactic:
apply PullbackObjObj.hom_ext

Premises used: CategoryTheory.Functor.PullbackObjObj.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 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ (map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.fst

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

Premises used: CategoryTheory.op_comp, 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 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
simp :
  sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    sq₁₃.snd ≫ (G.map f₁.hom.op).app f₃.right ≫ (G.obj (op f₁.left)).map (Arrow.Hom.right sq)
⊢ (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq)) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ≫ (G.map f₁.hom.op).app f₃'.right

Tactic:
simp [Arrow.mk_right]

Premises used: CategoryTheory.Arrow.mk_right
-- 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 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    sq₁₃.snd ≫ (G.map f₁.hom.op).app f₃.right ≫ (G.obj (op f₁.left)).map (Arrow.Hom.right sq)

Tactic:
grind [sq.w, sq₁₃.isPullback.w]

Premises used: CategoryTheory.Arrow.Hom.w, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, 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₁_1 : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃_1 : X₃ ⟶ Y₃
sq_1 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
h₁ :
  (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.fst
h₂ :
  (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.snd
⊢ map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
          (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)

Tactic:
apply PullbackObjObj.hom_ext

Premises used: CategoryTheory.Functor.PullbackObjObj.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 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.fst

Tactic:
simp [← Functor.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₁_1 : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃_1 : X₃ ⟶ Y₃
sq_1 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.snd

Tactic:
simp [← Functor.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₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
w :
  ∀ (x_1 : Arrow.{v₂, u₂} C₂),
    Arrow.Hom.left
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) =
      Arrow.Hom.left
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1)
w₁ :
  ∀ (x_1 : Arrow.{v₂, u₂} C₂),
    Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) =
      Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1)
⊢ Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
      whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁)) =
    Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
      (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)

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₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
x_1 : Arrow.{v₂, u₂} C₂
⊢ Arrow.Hom.left
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) =
    Arrow.Hom.left
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1)

Tactic:
simp [← homEquiv_naturality_one, ← homEquiv_naturality_three]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one