awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsColimit (F := parallelPair (X := pullback f.unop f.unop) (pullback.fst f.unop f.unop) (pullback.snd f.unop f.unop))
    (Cofork.ofπ f.unop ⋯)
refine_1 :
  Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f)
    (Quiver.Hom.op (pullback.fst f.unop f.unop) ≫ Iso.inv (pushoutIsoOpPullback f f))
refine_1₁ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f)
    (Quiver.Hom.op (pullback.fst f.unop f.unop) ≫ Quiver.Hom.op (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f f))))
refine_1₂ :
  Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f)
    (Quiver.Hom.op (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f f)) ≫ pullback.fst f.unop f.unop))
refine_1₃ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f)
    (Quiver.Hom.op (Quiver.Hom.unop (pushout.inl f f)))
refine_1₄ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f) (pushout.inl f f)
refine_1₅ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (𝟙 (Opposite.op (Opposite.unop Y)) ≫ pushout.inl f f) (pushout.inl f f)
refine_1₆ refine_1₇ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f)
    (pushout.inl f f)
⊢ Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f)
    (Quiver.Hom.op (pullback.fst f.unop f.unop) ≫ Iso.hom (Iso.symm (pushoutIsoOpPullback f f)))

Tactic:
rw [Iso.symm_hom, ← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv, ← op_comp,
        pushoutIsoOpPullback_inv_fst, Quiver.Hom.op_unop, Iso.refl_hom, Category.id_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.op_unop, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.pushoutIsoOpPullback_inv_fst, CategoryTheory.Limits.pushoutIsoOpPullback, CategoryTheory.Iso.inv, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsColimit (F := parallelPair (X := pullback f.unop f.unop) (pullback.fst f.unop f.unop) (pullback.snd f.unop f.unop))
    (Cofork.ofπ f.unop ⋯)
refine_2 :
  Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
    (Quiver.Hom.op (pullback.snd f.unop f.unop) ≫ Iso.inv (pushoutIsoOpPullback f f))
refine_2₁ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
    (Quiver.Hom.op (pullback.snd f.unop f.unop) ≫ Quiver.Hom.op (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f f))))
refine_2₂ :
  Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
    (Quiver.Hom.op (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f f)) ≫ pullback.snd f.unop f.unop))
refine_2₃ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
    (Quiver.Hom.op (Quiver.Hom.unop (pushout.inr f f)))
refine_2₄ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f) (pushout.inr f f)
refine_2₅ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (𝟙 (Opposite.op (Opposite.unop Y)) ≫ pushout.inr f f) (pushout.inr f f)
refine_2₆ refine_2₇ :
  Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inr f f)
    (pushout.inr f f)
⊢ Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
    (Quiver.Hom.op (pullback.snd f.unop f.unop) ≫ Iso.hom (Iso.symm (pushoutIsoOpPullback f f)))

Tactic:
rw [Iso.symm_hom, ← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv, ← op_comp,
        pushoutIsoOpPullback_inv_snd, Quiver.Hom.op_unop, Iso.refl_hom, Category.id_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.op_unop, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.pushoutIsoOpPullback, CategoryTheory.Limits.pushoutIsoOpPullback_inv_snd, CategoryTheory.Iso.inv, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
⊢ HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C

Tactic:
{ HasLimitsOfShape := fun _ _ _ => hasLimitsOfShape_of_hasColimitsOfShape_op }

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op, CategoryTheory.Limits.HasCofilteredLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
⊢ HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C

Tactic:
{ HasColimitsOfShape := fun _ _ _ => hasColimitsOfShape_of_hasLimitsOfShape_op }

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op, CategoryTheory.Limits.HasFilteredColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y Q : C
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
rw : (f ≫ p).op = 0
rw₁ : Eq.{v₁ + 1} (α := op Q ⟶ op X) (Quiver.Hom.op 0) 0
rw₂ rw₃ : Eq.{v₁ + 1} (α := op Q ⟶ op X) 0 0
⊢ Eq.{v₁ + 1} (α := op Q ⟶ op X) (p.op ≫ f.op) 0

Tactic:
rw [← op_comp, w, op_zero]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.op_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y Q : C
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
W' : Cᵒᵖ
x : W' ⟶ op Y
hx : x ≫ f.op = 0
b : W' ⟶ op Q
hb : b ≫ p.op = x
⊢ Cofork.π (CokernelCofork.ofπ p w) ≫ b.unop =
    Cofork.π (CokernelCofork.ofπ p w) ≫
      Quiver.Hom.unop
        ((fun {W' : Cᵒᵖ} (x : W' ⟶ op Y) (hx : x ≫ f.op = 0) ↦
            (Quiver.Hom.op (h.desc (CokernelCofork.ofπ x.unop ⋯)) :
              op (CokernelCofork.ofπ x.unop ⋯).pt ⟶ op (CokernelCofork.ofπ p w).pt))
          x hx)

Tactic:
simpa only [Quiver.Hom.unop_op, Cofork.IsColimit.π_desc] using Quiver.Hom.op_inj hb

Premises used: Quiver.Hom.unop_op, Quiver.Hom.op_inj, CategoryTheory.Limits.Cofork.IsColimit.π_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y Q : Cᵒᵖ
p : Y ⟶ Q
f : X ⟶ Y
w : Eq.{v₁ + 1} (α := X ⟶ Q) (f ≫ p) 0
h : IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F := parallelPair f 0) (CokernelCofork.ofπ p w)
rw : Eq.{v₁ + 1} (α := unop Q ⟶ unop X) (Quiver.Hom.unop (f ≫ p)) 0
rw₁ : Eq.{v₁ + 1} (α := unop Q ⟶ unop X) (Quiver.Hom.unop 0) 0
rw₂ rw₃ : Eq.{v₁ + 1} (α := unop Q ⟶ unop X) 0 0
⊢ p.unop ≫ f.unop = 0

Tactic:
rw [← unop_comp, w, unop_zero]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Limits.unop_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y Q : Cᵒᵖ
p : Y ⟶ Q
f : X ⟶ Y
w : Eq.{v₁ + 1} (α := X ⟶ Q) (f ≫ p) 0
h : IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F := parallelPair f 0) (CokernelCofork.ofπ p w)
W' : C
x : W' ⟶ unop Y
hx : x ≫ f.unop = 0
b : W' ⟶ unop Q
hb : b ≫ p.unop = x
⊢ Eq.{v₁ + 1} (α := Y ⟶ op W') (Cofork.π (CokernelCofork.ofπ p w) ≫ b.op)
    (CategoryStruct.comp (Y := Cocone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (CokernelCofork.ofπ p w))
      (Cofork.π (CokernelCofork.ofπ p w))
      (Quiver.Hom.op
        ((fun {W' : C} (x : W' ⟶ unop Y) (hx : x ≫ f.unop = 0) ↦
            (Quiver.Hom.unop (h.desc (CokernelCofork.ofπ x.op ⋯)) :
              Quiver.Hom.{v₁, u₁} (V := C)
                (unop (Cocone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (CokernelCofork.ofπ x.op ⋯)))
                (unop (Cocone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (CokernelCofork.ofπ p w)))))
          x hx)))

Tactic:
simpa only [Quiver.Hom.op_unop, Cofork.IsColimit.π_desc] using Quiver.Hom.unop_inj hb

Premises used: Quiver.Hom.op_unop, Quiver.Hom.unop_inj, CategoryTheory.Limits.Cofork.IsColimit.π_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
K X Y : C
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
rw : (i ≫ f).op = 0
rw₁ : Eq.{v₁ + 1} (α := op Y ⟶ op K) (Quiver.Hom.op 0) 0
rw₂ rw₃ : Eq.{v₁ + 1} (α := op Y ⟶ op K) 0 0
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op K) (f.op ≫ i.op) 0

Tactic:
rw [← op_comp, w, op_zero]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.op_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
K X Y : C
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
Z' : Cᵒᵖ
x : op X ⟶ Z'
hx : Eq (α := op Y ⟶ Z') (f.op ≫ x) 0
b : op K ⟶ Z'
hb : i.op ≫ b = x
⊢ b.unop ≫ Fork.ι (KernelFork.ofι i w) =
    Quiver.Hom.unop
        ((fun {Z' : Cᵒᵖ} (x : op X ⟶ Z') (hx : Eq (α := op Y ⟶ Z') (f.op ≫ x) 0) ↦
            (Quiver.Hom.op (h.lift (KernelFork.ofι x.unop ⋯)) :
              op (KernelFork.ofι i w).pt ⟶ op (KernelFork.ofι x.unop ⋯).pt))
          x hx) ≫
      Fork.ι (KernelFork.ofι i w)

Tactic:
simpa only [Quiver.Hom.unop_op, Fork.IsLimit.lift_ι] using Quiver.Hom.op_inj hb

Premises used: Quiver.Hom.unop_op, Quiver.Hom.op_inj, CategoryTheory.Limits.Fork.IsLimit.lift_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
K X Y : Cᵒᵖ
i : K ⟶ X
f : X ⟶ Y
w : Eq.{v₁ + 1} (α := K ⟶ Y) (i ≫ f) 0
h : IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F := parallelPair f 0) (KernelFork.ofι i w)
rw : Eq.{v₁ + 1} (α := unop Y ⟶ unop K) (Quiver.Hom.unop (i ≫ f)) 0
rw₁ : Eq.{v₁ + 1} (α := unop Y ⟶ unop K) (Quiver.Hom.unop 0) 0
rw₂ rw₃ : Eq.{v₁ + 1} (α := unop Y ⟶ unop K) 0 0
⊢ f.unop ≫ i.unop = 0

Tactic:
rw [← unop_comp, w, unop_zero]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Limits.unop_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasZeroMorphisms.{v₁, u₁} C
K X Y : Cᵒᵖ
i : K ⟶ X
f : X ⟶ Y
w : Eq.{v₁ + 1} (α := K ⟶ Y) (i ≫ f) 0
h : IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F := parallelPair f 0) (KernelFork.ofι i w)
Z' : C
x : unop X ⟶ Z'
hx : f.unop ≫ x = 0
b : unop K ⟶ Z'
hb : i.unop ≫ b = x
⊢ Eq.{v₁ + 1} (α := op Z' ⟶ X) (b.op ≫ Fork.ι (KernelFork.ofι i w))
    (CategoryStruct.comp (Y := Cone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (KernelFork.ofι i w))
      (Quiver.Hom.op
          ((fun {Z' : C} (x : unop X ⟶ Z') (hx : f.unop ≫ x = 0) ↦
              (Quiver.Hom.unop (h.lift (KernelFork.ofι x.op ⋯)) :
                Quiver.Hom.{v₁, u₁} (V := C)
                  (unop (Cone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (KernelFork.ofι i w)))
                  (unop (Cone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (KernelFork.ofι x.op ⋯)))))
            x hx) :
        op Z' ⟶ op (unop K))
      (Fork.ι (KernelFork.ofι i w) : Cone.pt.{0, v₁, 0, u₁} (F := parallelPair f 0) (KernelFork.ofι i w) ⟶ X))

Tactic:
simpa only [Quiver.Hom.op_unop, Fork.IsLimit.lift_ι] using Quiver.Hom.unop_inj hb

Premises used: Quiver.Hom.op_unop, CategoryTheory.Limits.Fork.IsLimit.lift_ι, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
inst_2 : HasProductsOfShape.{v₂, u₁, v₁} X C
⊢ HasLimitsOfShape.{v₂, v₂, v₁, u₁} (Discrete X)ᵒᵖ C

Tactic:
haveI : HasLimitsOfShape (Discrete X)ᵒᵖ C :=
    hasLimitsOfShape_of_equivalence (Discrete.opposite X).symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
inst_2 : HasProductsOfShape.{v₂, u₁, v₁} X C
this : HasLimitsOfShape.{v₂, v₂, v₁, u₁} (Discrete X)ᵒᵖ C
⊢ HasCoproductsOfShape.{v₂, u₁, v₁} X Cᵒᵖ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type v₂
inst_1 : HasProductsOfShape.{v₂, u₁, v₁} X Cᵒᵖ
⊢ HasCoproductsOfShape.{v₂, u₁, v₁} X C

Tactic:
haveI : HasLimitsOfShape (Discrete X)ᵒᵖ Cᵒᵖ :=
    hasLimitsOfShape_of_equivalence (Discrete.opposite X).symm
  hasColimitsOfShape_of_hasLimitsOfShape_op

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
inst_2 : HasCoproductsOfShape.{v₂, u₁, v₁} X C
⊢ HasProductsOfShape.{v₂, u₁, v₁} X Cᵒᵖ

Tactic:
haveI : HasColimitsOfShape (Discrete X)ᵒᵖ C :=
    hasColimitsOfShape_of_equivalence (Discrete.opposite X).symm
  hasLimitsOfShape_op_of_hasColimitsOfShape

Premises used: CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type v₂
inst_1 : HasCoproductsOfShape.{v₂, u₁, v₁} X Cᵒᵖ
⊢ HasProductsOfShape.{v₂, u₁, v₁} X C

Tactic:
haveI : HasColimitsOfShape (Discrete X)ᵒᵖ Cᵒᵖ :=
    hasColimitsOfShape_of_equivalence (Discrete.opposite X).symm
  hasLimitsOfShape_of_hasColimitsOfShape_op

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
inst_2 : HasCoproducts.{v₂, v₁, u₁} C
⊢ HasProducts.{v₂, v₁, u₁} Cᵒᵖ

Tactic:
fun _ =>
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCoproducts.{v₂, v₁, u₁} Cᵒᵖ
⊢ HasProducts.{v₂, v₁, u₁} C

Tactic:
fun X =>
  hasProductsOfShape_of_opposite X

Premises used: CategoryTheory.Limits.hasProductsOfShape_of_opposite
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
inst_2 : HasProducts.{v₂, v₁, u₁} C
⊢ HasCoproducts.{v₂, v₁, u₁} Cᵒᵖ

Tactic:
fun _ =>
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasProducts.{v₂, v₁, u₁} Cᵒᵖ
⊢ HasCoproducts.{v₂, v₁, u₁} C

Tactic:
fun X =>
  hasCoproductsOfShape_of_opposite X

Premises used: CategoryTheory.Limits.hasCoproductsOfShape_of_opposite
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasFiniteProducts.{v₁, u₁} Cᵒᵖ
⊢ HasFiniteCoproducts.{v₁, u₁} C

Tactic:
{ out := fun _ => hasCoproductsOfShape_of_opposite _ }

Premises used: CategoryTheory.Limits.hasCoproductsOfShape_of_opposite, CategoryTheory.Limits.HasFiniteCoproducts.mk, Fin
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasFiniteCoproducts.{v₁, u₁} Cᵒᵖ
⊢ HasFiniteProducts.{v₁, u₁} C

Tactic:
{ out := fun _ => hasProductsOfShape_of_opposite _ }

Premises used: CategoryTheory.Limits.HasFiniteProducts.mk, CategoryTheory.Limits.hasProductsOfShape_of_opposite, Fin
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasCoproduct.{u_1, v₁, u₁} Z
⊢ HasLimit.{u_1, u_1, v₁, u₁} (Functor.op (Discrete.functor Z))

Tactic:
hasLimit_op_of_hasColimit (Discrete.functor Z)

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.hasLimit_op_of_hasColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasCoproduct.{u_1, v₁, u₁} Z
⊢ HasLimit.{u_1, u_1, v₁, u₁} ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z))

Tactic:
hasLimit_equivalence_comp (Discrete.opposite α).symm

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Discrete.opposite, CategoryTheory.Limits.hasLimit_equivalence_comp, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasCoproduct.{u_1, v₁, u₁} Z
x : Discrete α
⊢ obj.{u_1, v₁, u_1, u₁}
      (Discrete.functor
        (obj.{u_1, v₁, u_1, u₁} ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) ∘ Discrete.mk))
      x ≅
    obj.{u_1, v₁, u_1, u₁}
      (Discrete.functor
        (obj.{u_1, v₁, u_1, u₁} ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) ∘ Discrete.mk))
      x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasCoproduct.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} Z
hc : IsColimit c
e : Iso (C := Functor.{u_1, v₁, u_1, u₁} (Discrete α) Cᵒᵖ) (Discrete.functor fun (x : α) ↦ Opposite.op (Z x))
  ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) :=
  Discrete.natIso fun (x : Discrete α) ↦
    Iso.refl (obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) x)
refine :
  ∀ (x : Discrete α) (a : α),
    Eq (α :=
      obj.{u_1, v₁, u_1, u₁}
          (obj (const (Discrete α))
            ((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).pt)
          { as := a : Discrete α } ⟶
        obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) { as := a : Discrete α })
      (((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).π.app { as := a })
      (Iso.hom
          (Iso.refl ((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).pt) ≫
        c.op.π.app { as := a })
⊢ IsLimit c.op

Tactic:
refine IsLimit.ofIsoLimit ((IsLimit.postcomposeInvEquiv e _).2
    (IsLimit.whiskerEquivalence hc.op (Discrete.opposite α).symm))
    (Cone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.IsLimit.whiskerEquivalence, CategoryTheory.Limits.Cone.pt, CategoryTheory.Limits.IsColimit.op, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cone.whisker, CategoryTheory.Limits.Cofan.IsColimit.op.match_1, CategoryTheory.Discrete.opposite, CategoryTheory.Iso.hom, Eq, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Iso.inv, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, Equiv.invFun, CategoryTheory.Limits.Cocone.op, CategoryTheory.Limits.Cone.ext, CategoryTheory.Limits.Cone.postcompose
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasCoproduct.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} Z
hc : IsColimit c
e : Iso (C := Functor.{u_1, v₁, u_1, u₁} (Discrete α) Cᵒᵖ) (Discrete.functor fun (x : α) ↦ Opposite.op (Z x))
  ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) :=
  Discrete.natIso fun (x : Discrete α) ↦
    Iso.refl (obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) x)
x : Discrete α
a : α
⊢ Eq (α :=
    obj.{u_1, v₁, u_1, u₁}
        (obj (const (Discrete α))
          ((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).pt)
        { as := a : Discrete α } ⟶
      obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) { as := a : Discrete α })
    (((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).π.app { as := a })
    (Iso.hom
        (Iso.refl ((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).pt) ≫
      c.op.π.app { as := a })

Tactic:
simp [e, Cofan.inj]

Premises used: CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
i : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj i = (c.inj i).op

Tactic:
simp [opCoproductIsoProduct', Fan.proj]

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.opCoproductIsoProduct'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
i : α
⊢ Eq.{v₁ + 1} (α := op (sigmaObj.{u_1, v₁, u₁} Z) ⟶ op (Z i))
    (Iso.hom (opCoproductIsoProduct Z) ≫ Pi.π (fun (x : α) ↦ op (Z x)) i) (Quiver.Hom.op (Sigma.ι Z i))

Tactic:
Limits.opCoproductIsoProduct'_hom_comp_proj ..

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
b : α
⊢ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj b).op = f.proj b

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp (Cofan.IsColimit.op hc) hf ⟨b⟩

Premises used: CategoryTheory.Limits.Fan.proj, Quiver.Hom.op, CategoryTheory.Limits.Cofan.IsColimit.op, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp