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

Tactic:
(colimit.isColimit (span f g)).comp_coconePointUniqueUpToIso_hom
    (PushoutCocone.flipIsColimit (pushoutIsPushout g f)) _

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitAux, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.PushoutCocone.IsColimit.mk, CategoryTheory.Limits.colimit, CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.Cocone.forget, CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.Limits.PushoutCocone.flip, CategoryTheory.Limits.span, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ Eq (α := Z ⟶ pushout f g) (pushout.inl g f ≫ Iso.inv (pushoutSymmetry f g)) (pushout.inr f g)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ Eq (α := Y ⟶ pushout f g) (pushout.inr g f ≫ Iso.inv (pushoutSymmetry f g)) (pushout.inl f g)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, HasLimit (cospan f g)
⊢ HasPullbacks.{v, u} C

Tactic:
{ has_limit := fun F => hasLimit_of_iso (diagramIsoCospan F).symm }

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, HasColimit (span f g)
⊢ HasPushouts.{v, u} C

Tactic:
{ has_colimit := fun F => hasColimit_of_iso (diagramIsoSpan F) }

Premises used: CategoryTheory.Limits.diagramIsoSpan, CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.hasColimit_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
D : Type u
inst_1 : Category.{v, u} D
inst_2 : HasWidePullbacks.{w, v, u} D
⊢ HasPullbacks.{v, u} D

Tactic:
hasWidePullbacks_shrink WalkingPair

Premises used: CategoryTheory.Limits.hasWidePullbacks_shrink, CategoryTheory.Limits.WalkingPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
D : Type u
inst_1 : Category.{v, u} D
inst_2 : HasWidePushouts.{w, v, u} D
⊢ HasPushouts.{v, u} D

Tactic:
hasWidePushouts_shrink WalkingPair

Premises used: CategoryTheory.Limits.hasWidePushouts_shrink, CategoryTheory.Limits.WalkingPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
S X Y : C
f : X ⟶ S
inst_1 : HasPullbacksAlong f
g : Y ⟶ S
⊢ HasPullback f g

Tactic:
hasPullback_symmetry g f

Premises used: CategoryTheory.Limits.hasPullback_symmetry
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
S X Y : C
f : S ⟶ X
inst_1 : HasPushoutsAlong f
g : S ⟶ Y
⊢ HasPushout f g

Tactic:
hasPushout_symmetry g f

Premises used: CategoryTheory.Limits.hasPushout_symmetry
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
h₀ :
  CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.fst f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.fst f prod.fst
h₁ :
  CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.snd f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst
⊢ CategoryStruct.comp (Y := prod.{v, u} X Z) (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
      (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.fst f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.fst f prod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} Y Z)
      (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
        (CategoryStruct.comp (Y := prod.{v, u} X Z)
          (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
          (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
        (pullback.snd f prod.fst))
      prod.fst =
    (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst
h₂ :
  CategoryStruct.comp (Y := prod.{v, u} Y Z)
      (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
        (CategoryStruct.comp (Y := prod.{v, u} X Z)
          (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
          (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
        (pullback.snd f prod.fst))
      prod.snd =
    (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd
⊢ CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.snd f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst

Tactic:
apply prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ CategoryStruct.comp (Y := prod.{v, u} Y Z)
      (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
        (CategoryStruct.comp (Y := prod.{v, u} X Z)
          (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
          (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
        (pullback.snd f prod.fst))
      prod.fst =
    (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ CategoryStruct.comp (Y := prod.{v, u} Y Z)
      (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
        (CategoryStruct.comp (Y := prod.{v, u} X Z)
          (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
          (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
        (pullback.snd f prod.fst))
      prod.snd =
    (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ Eq (α := pullback (Y := prod.{v, u} Y Z) f prod.fst ⟶ X)
    (CategoryStruct.comp (Y := prod.{v, u} X Z) (Iso.hom (pullbackProdFstIsoProd f Z)) prod.fst)
    (pullback.fst f prod.fst)

Tactic:
simp [pullbackProdFstIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdFstIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ Eq (α := pullback (Y := prod.{v, u} Y Z) f prod.fst ⟶ Z)
    (CategoryStruct.comp (Y := prod.{v, u} X Z) (Iso.hom (pullbackProdFstIsoProd f Z)) prod.snd)
    (pullback.snd f prod.fst ≫ prod.snd)

Tactic:
simp [pullbackProdFstIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdFstIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ Eq (α := prod.{v, u} X Z ⟶ X)
    (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst) (Iso.inv (pullbackProdFstIsoProd f Z))
      (pullback.fst f prod.fst))
    prod.fst

Tactic:
simp [pullbackProdFstIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdFstIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ Eq (α := prod.{v, u} X Z ⟶ Y)
    (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst) (Iso.inv (pullbackProdFstIsoProd f Z))
      (pullback.snd f prod.fst ≫ prod.fst))
    (prod.fst ≫ f)

Tactic:
simp [pullbackProdFstIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdFstIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ Eq (α := prod.{v, u} X Z ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst) (Iso.inv (pullbackProdFstIsoProd f Z))
      (pullback.snd f prod.fst ≫ prod.snd))
    prod.snd

Tactic:
simp [pullbackProdFstIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdFstIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
h₀ :
  CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.fst prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f
h₁ :
  CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.snd prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.snd prod.snd f
⊢ CategoryStruct.comp (Y := prod.{v, u} Z X) (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
      (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
h₀ :
  CategoryStruct.comp (Y := prod.{v, u} Z Y)
      (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
        (CategoryStruct.comp (Y := prod.{v, u} Z X)
          (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
          (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
        (pullback.fst prod.snd f))
      prod.fst =
    (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} Z Y)
      (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
        (CategoryStruct.comp (Y := prod.{v, u} Z X)
          (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
          (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
        (pullback.fst prod.snd f))
      prod.snd =
    (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd
⊢ CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.fst prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f

Tactic:
apply prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ CategoryStruct.comp (Y := prod.{v, u} Z Y)
      (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
        (CategoryStruct.comp (Y := prod.{v, u} Z X)
          (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
          (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
        (pullback.fst prod.snd f))
      prod.fst =
    (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ CategoryStruct.comp (Y := prod.{v, u} Z Y)
      (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
        (CategoryStruct.comp (Y := prod.{v, u} Z X)
          (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
          (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
        (pullback.fst prod.snd f))
      prod.snd =
    (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.snd prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.snd prod.snd f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ Eq (α := pullback (X := prod.{v, u} Z Y) prod.snd f ⟶ Z)
    (CategoryStruct.comp (Y := prod.{v, u} Z X) (Iso.hom (pullbackProdSndIsoProd f Z)) prod.fst)
    (pullback.fst prod.snd f ≫ prod.fst)

Tactic:
simp [pullbackProdSndIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdSndIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ Eq (α := pullback (X := prod.{v, u} Z Y) prod.snd f ⟶ X)
    (CategoryStruct.comp (Y := prod.{v, u} Z X) (Iso.hom (pullbackProdSndIsoProd f Z)) prod.snd)
    (pullback.snd prod.snd f)

Tactic:
simp [pullbackProdSndIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdSndIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ Eq (α := prod.{v, u} Z X ⟶ Z)
    (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f) (Iso.inv (pullbackProdSndIsoProd f Z))
      (pullback.fst prod.snd f ≫ prod.fst))
    prod.fst

Tactic:
simp [pullbackProdSndIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdSndIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ Eq (α := prod.{v, u} Z X ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f) (Iso.inv (pullbackProdSndIsoProd f Z))
      (pullback.fst prod.snd f ≫ prod.snd))
    (prod.snd ≫ f)

Tactic:
simp [pullbackProdSndIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdSndIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ Eq (α := prod.{v, u} Z X ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f) (Iso.inv (pullbackProdSndIsoProd f Z))
      (pullback.snd prod.snd f))
    prod.snd

Tactic:
simp [pullbackProdSndIsoProd]

Premises used: CategoryTheory.Limits.pullbackProdSndIsoProd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan.{v₁, u₁} X Y
h : IsLimit c
t : IsTerminal.{v₁, u₁} Z
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (c.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl c.pt) ≫
      NatTrans.app
        (Cone.π (BinaryFan.mk (P := c.1) (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })))
        { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan.{v₁, u₁} X Y
h : IsLimit c
t : IsTerminal.{v₁, u₁} Z
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (c.π.app { as := WalkingPair.right })
    (Iso.hom (Iso.refl c.pt) ≫
      NatTrans.app
        (Cone.π (BinaryFan.mk (P := c.1) (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })))
        { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
h : IsLimit (BinaryFan.mk fst snd)
t : IsTerminal.{v₁, u₁} Z
⊢ IsPullback fst snd (t.from X) (t.from Y)

Tactic:
of_is_product h t

Premises used: CategoryTheory.IsPullback.of_is_product
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasBinaryProduct.{v₁, u₁} X Y
inst_2 : HasTerminal.{v₁, u₁} C
⊢ IsPullback.{v₁, u₁} (P := Limits.prod.{v₁, u₁} X Y) (Z := terminal.{v₁, u₁} C) prod.fst prod.snd (terminal.from X)
    (terminal.from Y)

Tactic:
of_is_product (limit.isLimit _) terminalIsTerminal

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.terminalIsTerminal, CategoryTheory.IsPullback.of_is_product
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : CommSq fst snd f g
inst_1 : HasPullback f g
i : P ≅ pullback f g
w₁ : i.hom ≫ pullback.fst f g = fst
w₂ : i.hom ≫ pullback.snd f g = snd
⊢ IsPullback fst snd f g

Tactic:
of_isLimit' h
    (Limits.IsLimit.ofIsoLimit (limit.isLimit _)
      (@PullbackCone.ext _ _ _ _ _ _ _ (PullbackCone.mk _ _ _) _ i w₁.symm w₂.symm).symm)

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.PullbackCone.ext, CategoryTheory.Iso.symm, CategoryTheory.IsPullback.of_isLimit', Eq.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso fst
inst_2 : Mono g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g), (fun (s : PullbackCone f g) ↦ s.fst ≫ inv fst) s ≫ fst = s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso fst
inst_2 : Mono g
sq : CommSq fst snd f g
_ : ∀ (s : PullbackCone f g), (fun (s : PullbackCone f g) ↦ s.fst ≫ inv fst) s ≫ snd = s.snd
⊢ IsLimit sq.cone

Tactic:
refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by cat_disch)

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.IsLimit.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv