awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Eq (α :=
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
      (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right)
    (Under.Hom.right (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Under.homMk m ⋯))
    (Under.Hom.right
      ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.left }))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Eq (α :=
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).right ⟶
      (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right)
    (Under.Hom.right (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Under.homMk m ⋯))
    (Under.Hom.right
      ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.right }))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Eq (α := c.pt ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt) (Under.homMk m ⋯)
    (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s))

Tactic:
have := hc.uniq (pushoutCoconeEquivBinaryCofan.functor.obj s) (Under.homMk m <| by
        simp [← hm₁, dsimp% c.inl.w_assoc])
        (by rintro (_ | _) <;> ext <;> simpa)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
this :
  Eq (α := c.pt ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt) (Under.homMk m ⋯)
    (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s))
⊢ m =
    (fun
          (s :
            PushoutCocone
              (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Under.Hom.right (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s)) :
          c.pt.right ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right))
      s

Tactic:
congr(($this).right)

Premises used: congrArg, id, CategoryTheory.Under.Hom.right
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
this :
  Eq (α := c.pt ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt) (Under.homMk m ⋯)
    (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s))
⊢ m =
    (fun
          (s :
            PushoutCocone
              (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Under.Hom.right (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s)) :
          c.pt.right ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right))
      s

Tactic:
exact congr(($this).right)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y Z : Over.{v, u} X
c : BinaryFan Y Z
hc : IsLimit c
⊢ CommSq (Hom.left c.fst) (Hom.left c.snd) Y.hom Z.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y Z : Over.{v, u} X
inst_1 : HasPullback Y.hom Z.hom
inst_2 : HasBinaryProduct Y Z
⊢ Eq (α := (Y ⨯ Z).left ⟶ Y.left)
    (CategoryStruct.comp (Y := pullback Y.hom Z.hom) (Iso.hom (Y.prodLeftIsoPullback Z)) (pullback.fst Y.hom Z.hom))
    (Hom.left prod.fst)

Tactic:
IsPullback.isoPullback_hom_fst _

Premises used: CategoryTheory.IsPullback.isoPullback_hom_fst
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y Z : Over.{v, u} X
inst_1 : HasPullback Y.hom Z.hom
inst_2 : HasBinaryProduct Y Z
⊢ Eq (α := (Y ⨯ Z).left ⟶ Z.left)
    (CategoryStruct.comp (Y := pullback Y.hom Z.hom) (Iso.hom (Y.prodLeftIsoPullback Z)) (pullback.snd Y.hom Z.hom))
    (Hom.left prod.snd)

Tactic:
IsPullback.isoPullback_hom_snd _

Premises used: CategoryTheory.IsPullback.isoPullback_hom_snd
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y Z : Over.{v, u} X
inst_1 : HasPullback Y.hom Z.hom
inst_2 : HasBinaryProduct Y Z
⊢ Eq (α := pullback Y.hom Z.hom ⟶ Y.left)
    (CategoryStruct.comp (Y := (Y ⨯ Z).left) (Iso.inv (Y.prodLeftIsoPullback Z)) (Hom.left prod.fst))
    (pullback.fst Y.hom Z.hom)

Tactic:
IsPullback.isoPullback_inv_fst _

Premises used: CategoryTheory.IsPullback.isoPullback_inv_fst
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y Z : Over.{v, u} X
inst_1 : HasPullback Y.hom Z.hom
inst_2 : HasBinaryProduct Y Z
⊢ Eq (α := pullback Y.hom Z.hom ⟶ Z.left)
    (CategoryStruct.comp (Y := (Y ⨯ Z).left) (Iso.inv (Y.prodLeftIsoPullback Z)) (Hom.left prod.snd))
    (pullback.snd Y.hom Z.hom)

Tactic:
IsPullback.isoPullback_inv_snd _

Premises used: CategoryTheory.IsPullback.isoPullback_inv_snd
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : WidePullbackShape J
none :
  Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj Option.none)
    (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app Option.none)
    ((conesEquivInverseObj B F X_1).π.app Option.none)
some :
  ∀ (j : J),
    Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj (Option.some j))
      (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app (Option.some j))
      ((conesEquivInverseObj B F X_1).π.app (Option.some j))
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app j = (conesEquivInverseObj B F X_1).π.app j

Tactic:
obtain - | j := j
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
⊢ Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj none)
    (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app none) ((conesEquivInverseObj B F X_1).π.app none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : J
some :
  Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
    (Hom.left (X_1.π.app { as := j }))
⊢ Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj (Option.some j))
    (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app (Option.some j))
    ((conesEquivInverseObj B F X_1).π.app (Option.some j))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : J
some :
  Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
    (Hom.left (f.hom ≫ Y_1.π.app { as := j }))
⊢ Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
    (Hom.left (X_1.π.app { as := j }))

Tactic:
rw [← f.w ⟨j⟩]

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : J
⊢ Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
    (Hom.left (f.hom ≫ Y_1.π.app { as := j }))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
F : Discrete J ⥤ Over.{v, u} B
inst_1 : HasLimit (widePullbackDiagramOfDiagramOver B F)
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := _
      isLimit := IsLimit.ofRightAdjoint (conesEquiv B F).symm.toAdjunction
        (limit.isLimit (widePullbackDiagramOfDiagramOver B F)) }

Premises used: CategoryTheory.Limits.IsLimit.ofRightAdjoint, CategoryTheory.Limits.limit.cone, CategoryTheory.Over.ConstructProducts.conesEquiv, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfShape.{w, w, v, u} (WidePullbackShape J) C
B : C
⊢ HasLimitsOfShape (Discrete J) (Over.{v, u} B)

Tactic:
{ has_limit := fun F => has_over_limit_discrete_of_widePullback_limit F }

Premises used: CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit, CategoryTheory.Limits.HasLimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
B : C
⊢ HasBinaryProducts (Over.{v, u} B)

Tactic:
over_product_of_widePullback

Premises used: CategoryTheory.Over.ConstructProducts.over_product_of_widePullback
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWidePullbacks.{w, v, u} C
B : C
⊢ HasProducts (Over.{v, u} B)

Tactic:
fun _ => over_product_of_widePullback

Premises used: CategoryTheory.Over.ConstructProducts.over_product_of_widePullback
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteWidePullbacks.{v, u} C
B : C
⊢ HasFiniteProducts (Over.{v, u} B)

Tactic:
⟨fun _ => over_product_of_widePullback⟩

Premises used: CategoryTheory.Limits.HasFiniteProducts.mk, CategoryTheory.Over.ConstructProducts.over_product_of_widePullback
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over.{v, u} B
s : Cone F
m :
  s.pt ⟶
    Cone.pt (J := Discrete PEmpty.{1}) (F := F)
      { pt := mk (𝟙 B), π := { app := fun (p : Discrete PEmpty.{1}) ↦ p.as.elim, naturality := ⋯ } }
h_1 :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫
        NatTrans.app
          (Cone.π { pt := mk (𝟙 B), π := { app := fun (p : Discrete PEmpty.{1}) ↦ p.as.elim, naturality := ⋯ } }) j =
      s.π.app j
h : Hom.left m = Hom.left (homMk s.pt.hom ⋯)
⊢ m = homMk s.pt.hom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
C : Type u
inst : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over.{v, u} B
s : Cone F
m :
  s.pt ⟶
    Cone.pt (J := Discrete PEmpty.{1}) (F := F)
      { pt := mk (𝟙 B), π := { app := fun (p : Discrete PEmpty.{1}) ↦ p.as.elim, naturality := ⋯ } }
h :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫
        NatTrans.app
          (Cone.π { pt := mk (𝟙 B), π := { app := fun (p : Discrete PEmpty.{1}) ↦ p.as.elim, naturality := ⋯ } }) j =
      s.π.app j
⊢ Hom.left m = Hom.left (homMk s.pt.hom ⋯)

Tactic:
simpa using m.w

Premises used: CategoryTheory.Over.Hom.w
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
rw : equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g
⊢ (e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g

Tactic:
rw [Category.assoc, equalizer.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g

Tactic:
simp [e]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
rw :
  Eq (α := s.pt ⟶ Z)
    ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.left } ≫ f :
      s.pt ⟶ Z)
    ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.right } ≫ g :
      s.pt ⟶ Z)
⊢ prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ π₁ ≫ f =
    prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ π₂ ≫ g

Tactic:
rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ Eq (α := s.pt ⟶ Z)
    ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.left } ≫ f :
      s.pt ⟶ Z)
    ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.right } ≫ g :
      s.pt ⟶ Z)

Tactic:
PullbackCone.condition _

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ Eq (α := s.pt ⟶ Z)
    ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.left } ≫ f :
      s.pt ⟶ Z)
    ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.right } ≫ g :
      s.pt ⟶ Z)

Tactic:
exact PullbackCone.condition _

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s ≫
        e ≫ π₁ =
      s.fst

Tactic:
simp [π₁, e]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s ≫
        e ≫ π₂ =
      s.snd

Tactic:
simp [π₂, e]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
h :
  (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        ((fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s)
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst
h₃ :
  (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        ((fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s)
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.snd
⊢ m =
    (fun (s : PullbackCone f g) ↦
        (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
          s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
      s

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
h :
  (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
          s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g))
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g) : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y) ≫
      prod.fst
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        ((fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s)
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
          s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g))
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g) : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y) ≫
      prod.fst

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        ((fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s)
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.snd

Tactic:
simpa using h₂
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasEqualizers.{v, u} C
⊢ 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