awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ Eq (α :=
    (cospan f_1.unop g.unop).obj none ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (some WalkingPair.left))
    ((cospan f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          none) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ Eq (α :=
    (cospan f_1.unop g.unop).obj none ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (some WalkingPair.right))
    ((cospan f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.right)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          none) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ Eq (α :=
    (cospan f_1.unop g.unop).obj (some WalkingPair.left) ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (some WalkingPair.right))
    ((cospan f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.right)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.left)) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ Eq (α :=
    (cospan f_1.unop g.unop).obj (some WalkingPair.right) ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) (some WalkingPair.left))
    ((cospan f_1.unop g.unop).map f ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f_1.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x)
                x with
              | none => Iso.refl ((cospan f_1.unop g.unop).obj none)
              | some WalkingPair.left => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f_1.unop g.unop).obj WalkingCospan.right) :
              (cospan f_1.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) x))
          (some WalkingPair.right)) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f_1 g)) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.fst = c.inl.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.snd = c.inr.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.fst = c.inl.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.snd = c.inr.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.inl = c.fst.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.inr = c.snd.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.inl = c.fst.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.inr = c.snd.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.unop.fst = Iso.hom (Iso.refl c.op.unop.pt) ≫ c.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.unop.snd = Iso.hom (Iso.refl c.op.unop.pt) ≫ c.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.op.fst = Iso.hom (Iso.refl c.unop.op.pt) ≫ c.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.op.snd = Iso.hom (Iso.refl c.unop.op.pt) ≫ c.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.unop.inl ≫ Iso.hom (Iso.refl c.op.unop.pt) = c.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.unop.inr ≫ Iso.hom (Iso.refl c.op.unop.pt) = c.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.op.inl ≫ Iso.hom (Iso.refl c.unop.op.pt) = c.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ c.unop.op.inr ≫ Iso.hom (Iso.refl c.unop.op.pt) = c.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
f₁ : IsColimit c → IsLimit c.op
g₁ : IsLimit c.op → IsColimit c
⊢ IsColimit c ≃ IsLimit c.op

Tactic:
apply equivOfSubsingletonOfSubsingleton

Premises used: equivOfSubsingletonOfSubsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsColimit c
⊢ IsLimit c.op

Tactic:
exact (IsLimit.postcomposeHomEquiv _ _).invFun
      ((IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).toFun h.op)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Limits.walkingSpanOpEquiv, Equiv.toFun, CategoryTheory.Limits.IsColimit.op, CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv, CategoryTheory.Equivalence.symm, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsLimit c.op
⊢ IsColimit c

Tactic:
exact (IsColimit.equivIsoColimit c.opUnopIso).toFun
      (((IsLimit.postcomposeHomEquiv _ _).invFun
        ((IsLimit.whiskerEquivalenceEquiv _).toFun h)).unop)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Limits.IsColimit.equivIsoColimit, CategoryTheory.Limits.IsLimit.unop, Equiv.toFun, CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv, CategoryTheory.Limits.PushoutCocone.opUnopIso, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
f₁ : IsColimit c → IsLimit c.unop
g₁ : IsLimit c.unop → IsColimit c
⊢ IsColimit c ≃ IsLimit c.unop

Tactic:
apply equivOfSubsingletonOfSubsingleton

Premises used: equivOfSubsingletonOfSubsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
h : IsColimit c
⊢ IsLimit c.unop

Tactic:
exact ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv _).toFun h)).unop

Premises used: Equiv.toFun, CategoryTheory.Limits.IsColimit.unop, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, Equiv.invFun, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
h : IsLimit c.unop
⊢ IsColimit c

Tactic:
exact (IsColimit.equivIsoColimit c.unopOpIso).toFun
      ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingCospanOpEquiv.symm).toFun h.op))

Premises used: CategoryTheory.Limits.IsLimit.op, CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.toFun, CategoryTheory.Limits.walkingCospanOpEquiv, CategoryTheory.Limits.PushoutCocone.unopOpIso, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, Equiv.invFun, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (span f.op g.op) ↔ HasPullback f g
rw₁ : HasColimit (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op) ↔ HasPullback f g
rw₂ : HasColimit (cospan f g).op ↔ HasPullback f g
rw₃ rw₄ : HasLimit (cospan f g) ↔ HasPullback f g
⊢ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := op Z) (Y := op X) (Z := op Y) f.op g.op ↔ HasPullback f g

Tactic:
rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]

Premises used: CategoryTheory.Limits.hasColimit_iff_of_iso, CategoryTheory.Limits.spanOp, CategoryTheory.Limits.hasColimit_inverse_equivalence_comp_iff, CategoryTheory.Limits.hasColimit_op_iff_hasLimit, CategoryTheory.Limits.HasPushout
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
rw : HasColimit (span f.unop g.unop) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₁ :
  HasColimit.{0, 0, v₁, u₁} (C := C) (walkingCospanOpEquiv.inverse ⋙ Functor.leftOp (cospan f g)) ↔
    HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₂ :
  HasColimit.{0, 0, v₁, u₁} (C := C) (Functor.leftOp (cospan f g)) ↔
    HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
rw₃ rw₄ :
  HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f g) ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPushout f.unop g.unop ↔ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g

Tactic:
rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]

Premises used: CategoryTheory.Limits.hasColimit_iff_of_iso, CategoryTheory.Limits.hasColimit_inverse_equivalence_comp_iff, CategoryTheory.Limits.spanUnop, CategoryTheory.Limits.hasColimit_leftOp_iff_hasLimit, CategoryTheory.Limits.HasPushout
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 rwa rwa₁ rwa₂ rwa₃ : HasPullback f g
⊢ HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := op Z) (Y := op X) (Z := op Y) f.op g.op

Tactic:
rwa [hasPushout_op_iff_hasPullback]

Premises used: CategoryTheory.Limits.hasPushout_op_iff_hasPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst_2 rwa rwa₁ rwa₂ rwa₃ : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ HasPushout f.unop g.unop

Tactic:
rwa [hasPushout_unop_iff_hasPullback]

Premises used: CategoryTheory.Limits.hasPushout_unop_iff_hasPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq.{v₁ + 1} (α :=
    Cone.pt.{0, v₁, 0, u₁} (F := cospan f g) (PushoutCocone.unop (colimit.cocone (span f.op g.op))) ⟶
      (cospan f g).obj WalkingCospan.left)
    (NatTrans.app (Cone.π (PushoutCocone.unop (colimit.cocone (span f.op g.op)))) WalkingCospan.left :
      obj.{0, v₁, 0, u₁}
          (obj (const WalkingCospan)
            (Cone.pt.{0, v₁, 0, u₁} (F := cospan f g) (PushoutCocone.unop (colimit.cocone (span f.op g.op)))))
          WalkingCospan.left ⟶
        (cospan f g).obj WalkingCospan.left)
    (Quiver.Hom.unop (pushout.inl f.op g.op))

Tactic:
simp [unop_id (X := { unop := X })]

Premises used: CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq.{v₁ + 1} (α :=
    Cone.pt.{0, v₁, 0, u₁} (F := cospan f g) (PushoutCocone.unop (colimit.cocone (span f.op g.op))) ⟶
      (cospan f g).obj WalkingCospan.right)
    (NatTrans.app (Cone.π (PushoutCocone.unop (colimit.cocone (span f.op g.op)))) WalkingCospan.right :
      obj.{0, v₁, 0, u₁}
          (obj (const WalkingCospan)
            (Cone.pt.{0, v₁, 0, u₁} (F := cospan f g) (PushoutCocone.unop (colimit.cocone (span f.op g.op)))))
          WalkingCospan.right ⟶
        (cospan f g).obj WalkingCospan.right)
    (Quiver.Hom.unop (pushout.inr f.op g.op))

Tactic:
simp [unop_id (X := { unop := Y })]

Premises used: CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := unop (op (pullback f g)) ⟶ unop (op X))
    (Quiver.Hom.unop (pushout.inl f.op g.op ≫ Quiver.Hom.op (Iso.hom (pullbackIsoUnopPushout f g))))
    (Quiver.Hom.unop (Quiver.Hom.op (pullback.fst f g)))

Tactic:
simp [← pullbackIsoUnopPushout_inv_fst]

Premises used: CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := unop (op (pullback f g)) ⟶ unop (op Y))
    (Quiver.Hom.unop (pushout.inr f.op g.op ≫ Quiver.Hom.op (Iso.hom (pullbackIsoUnopPushout f g))))
    (Quiver.Hom.unop (Quiver.Hom.op (pullback.snd f g)))

Tactic:
simp [← pullbackIsoUnopPushout_inv_snd]

Premises used: CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ (PushoutCocone.op (colimit.cocone (span f.unop g.unop))).π.app WalkingCospan.left =
    Quiver.Hom.op (pushout.inl f.unop g.unop)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ (PushoutCocone.op (colimit.cocone (span f.unop g.unop))).π.app WalkingCospan.right =
    Quiver.Hom.op (pushout.inr f.unop g.unop)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ Eq (α := op (unop (pullback.{v₁, u₁} (X := X) (Y := Y) (Z := Z) f g)) ⟶ op (unop X))
    (Quiver.Hom.op (pushout.inl f.unop g.unop ≫ Quiver.Hom.unop (Iso.hom (pullbackIsoOpPushout f g))))
    (Quiver.Hom.op (Quiver.Hom.unop (pullback.fst f g)))

Tactic:
simp [← pullbackIsoOpPushout_inv_fst]

Premises used: CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) f g
⊢ Eq (α := op (unop (pullback.{v₁, u₁} (X := X) (Y := Y) (Z := Z) f g)) ⟶ op (unop Y))
    (Quiver.Hom.op (pushout.inr f.unop g.unop ≫ Quiver.Hom.unop (Iso.hom (pullbackIsoOpPushout f g))))
    (Quiver.Hom.op (Quiver.Hom.unop (pullback.snd f g)))

Tactic:
simp [← pullbackIsoOpPushout_inv_snd]

Premises used: CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
rw : HasLimit.{0, 0, v₁, u₁} (C := Cᵒᵖ) (cospan f.op g.op) ↔ HasPushout f g
rw₁ : HasLimit (walkingSpanOpEquiv.inverse ⋙ (span f g).op) ↔ HasPushout f g
rw₂ : HasLimit (span f g).op ↔ HasPushout f g
rw₃ rw₄ : HasColimit (span f g) ↔ HasPushout f g
⊢ HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op Z) (Z := op X) f.op g.op ↔ HasPushout f g

Tactic:
rw [HasPullback, hasLimit_iff_of_iso (cospanOp f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_op_iff_hasColimit]

Premises used: CategoryTheory.Limits.hasLimit_iff_of_iso, CategoryTheory.Limits.cospanOp, CategoryTheory.Limits.HasPullback, CategoryTheory.Limits.hasLimit_op_iff_hasColimit, CategoryTheory.Limits.hasLimit_inverse_equivalence_comp_iff