awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers (goal)
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)
⊢ 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)))
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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)
⊢ Eq.{v₁ + 1} (α := op Q ⟶ op X) (p.op ≫ f.op) 0
have rw : (f ≫ p).op = 0
Tactic: rw [← op_comp, w, op_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ Eq.{v₁ + 1} (α := op Q ⟶ op X) (p.op ≫ f.op) 0
have rw₁ : Eq.{v₁ + 1} (α := op Q ⟶ op X) (Quiver.Hom.op 0) 0
Tactic: rw [← op_comp, w, op_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ Eq.{v₁ + 1} (α := op Q ⟶ op X) (p.op ≫ f.op) 0
have rw₂ : Eq.{v₁ + 1} (α := op Q ⟶ op X) 0 0
Tactic: rw [← op_comp, w, op_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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)
⊢ p.unop ≫ f.unop = 0
have rw : Eq.{v₁ + 1} (α := unop Q ⟶ unop X) (Quiver.Hom.unop (f ≫ p)) 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ p.unop ≫ f.unop = 0
have rw₁ : Eq.{v₁ + 1} (α := unop Q ⟶ unop X) (Quiver.Hom.unop 0) 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ p.unop ≫ f.unop = 0
have rw₂ : Eq.{v₁ + 1} (α := unop Q ⟶ unop X) 0 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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)
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op K) (f.op ≫ i.op) 0
have rw : (i ≫ f).op = 0
Tactic: rw [← op_comp, w, op_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op K) (f.op ≫ i.op) 0
have rw₁ : Eq.{v₁ + 1} (α := op Y ⟶ op K) (Quiver.Hom.op 0) 0
Tactic: rw [← op_comp, w, op_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op K) (f.op ≫ i.op) 0
have rw₂ : Eq.{v₁ + 1} (α := op Y ⟶ op K) 0 0
Tactic: rw [← op_comp, w, op_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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)
⊢ f.unop ≫ i.unop = 0
have rw : Eq.{v₁ + 1} (α := unop Y ⟶ unop K) (Quiver.Hom.unop (i ≫ f)) 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ f.unop ≫ i.unop = 0
have rw₁ : Eq.{v₁ + 1} (α := unop Y ⟶ unop K) (Quiver.Hom.unop 0) 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels (goal)
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
⊢ f.unop ≫ i.unop = 0
have rw₂ : Eq.{v₁ + 1} (α := unop Y ⟶ unop K) 0 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (hypothesis)
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
⊢ HasCoproductsOfShape.{v₂, u₁, v₁} X Cᵒᵖ
have this : HasLimitsOfShape.{v₂, v₂, v₁, u₁} (Discrete X)ᵒᵖ C
Tactic: haveI : HasLimitsOfShape (Discrete X)ᵒᵖ C :=
    hasLimitsOfShape_of_equivalence (Discrete.opposite X).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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)
⊢ IsLimit c.op
have 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 })
Tactic: refine IsLimit.ofIsoLimit ((IsLimit.postcomposeInvEquiv e _).2
    (IsLimit.whiskerEquivalence hc.op (Discrete.opposite α).symm))
    (Cone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
have a : ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
  (hc.coconePointUniqueUpToIso hc').op.inv.unop
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    (hc.coconePointUniqueUpToIso hc').op.inv.unop
have a : ∀ (j : Discrete α),
  c'.ι.app j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app j ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
Tactic: apply hc'.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ Eq (α := obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α } ⟶ unop (op c.pt))
    (c'.ι.app { as := j } ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop)
    (c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop)
have a : c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
  c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
Tactic: change c'.inj _ ≫ _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
have a : c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }
Tactic: simp only [unop_op, unop_comp, Discrete.functor_obj, const_obj_obj, Iso.op_inv,
    Quiver.Hom.unop_op, IsColimit.comp_coconePointUniqueUpToIso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }
have a : (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
  Quiver.Hom.op (c.ι.app { as := j })
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
    Quiver.Hom.op (c.ι.app { as := j })
have a : (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = Quiver.Hom.op (c.ι.app { as := j })
Tactic: simp only [op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc,
    opCoproductIsoProduct'_inv_comp_inj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = Quiver.Hom.op (c.ι.app { as := j })
have a : (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op =
  Quiver.Hom.op (c.ι.app { as := j })
Tactic: rw [← opCoproductIsoProduct'_inv_comp_inj hc hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op =
    Quiver.Hom.op (c.ι.app { as := j })
have a : (c.inj j).op = Quiver.Hom.op (c.ι.app { as := j })
Tactic: simp only [Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
c' : Cofan.{u_1, v₁, u₁} Z
⊢ Eq (α := op c'.pt ⟶ f.pt) ((hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom : op c'.pt ⟶ f.pt)
    (hf.lift c'.op : c'.op.pt ⟶ f.pt)
have refine : ∀ (x : Discrete α) (j : α),
  Eq (α := op (unop (op c'.pt)) ⟶ op (obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α }))
    (Quiver.Hom.op (c.ι.app { as := j } ≫ (hc.desc c').op.unop))
    (Quiver.Hom.op
      (c.ι.app { as := j : Discrete α } ≫ Quiver.Hom.unop (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv)))
Tactic: refine (Iso.eq_comp_inv _).mp (Quiver.Hom.unop_inj (hc.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
c' : Cofan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
⊢ Eq (α := op (unop (op c'.pt)) ⟶ op (obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α }))
    (Quiver.Hom.op (c.ι.app { as := j } ≫ (hc.desc c').op.unop))
    (Quiver.Hom.op
      (c.ι.app { as := j : Discrete α } ≫ Quiver.Hom.unop (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv)))
have simp : Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
  (hf.lift (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op) ≫
    (opCoproductIsoProduct' hc hf).inv ≫ Quiver.Hom.op (c.ι.app { as := j : Discrete α }))
Tactic: simp only [unop_op, Discrete.functor_obj, const_obj_obj, Quiver.Hom.unop_op, IsColimit.fac,
    Cofan.op, unop_comp, op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
c' : Cofan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
⊢ Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
    (hf.lift (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op) ≫
      (opCoproductIsoProduct' hc hf).inv ≫ Quiver.Hom.op (c.ι.app { as := j : Discrete α }))
have erw : Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
  (NatTrans.app (Cone.π (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op)) { as := j })
Tactic: erw [opCoproductIsoProduct'_inv_comp_inj, IsLimit.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → Z a ⟶ X
⊢ Eq.{v₁ + 1} (α := op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (CategoryStruct.comp (Y := op (sigmaObj.{u_1, v₁, u₁} Z)) (Quiver.Hom.op (Sigma.desc π))
        (Iso.hom (opCoproductIsoProduct Z)) :
      op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (Pi.lift fun (a : α) ↦ (π a).op : op X ⟶ piObj.{u_1, v₁, u₁} fun (a : α) ↦ op (Z a))
have h : (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
    (op (Cofan.mk X π).pt ⟶
      Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x)))) →
  op X = op (Cofan.mk X π).pt →
    op (sigmaObj.{u_1, v₁, u₁} Z) = op (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt →
      sigmaObj.{u_1, v₁, u₁} Z = (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt →
        X = (Cofan.mk X π).pt →
          Eq (α := sigmaObj.{u_1, v₁, u₁} Z ⟶ X) (Sigma.desc π) (IsColimit.desc (coproductIsCoproduct Z) (Cofan.mk X π))
Tactic: convert!
    desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))
      (Cofan.mk _ π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → Z a ⟶ X
h :
  (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
      (op (Cofan.mk X π).pt ⟶
        Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
          (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x)))) →
    op X = op (Cofan.mk X π).pt →
      op (sigmaObj.{u_1, v₁, u₁} Z) = op (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt →
        sigmaObj.{u_1, v₁, u₁} Z = (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt →
          X = (Cofan.mk X π).pt →
            Eq (α := sigmaObj.{u_1, v₁, u₁} Z ⟶ X) (Sigma.desc π)
              (IsColimit.desc (coproductIsCoproduct Z) (Cofan.mk X π))
⊢ Eq.{v₁ + 1} (α := op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (CategoryStruct.comp (Y := op (sigmaObj.{u_1, v₁, u₁} Z)) (Quiver.Hom.op (Sigma.desc π))
        (Iso.hom (opCoproductIsoProduct Z)) :
      op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (Pi.lift fun (a : α) ↦ (π a).op : op X ⟶ piObj.{u_1, v₁, u₁} fun (a : α) ↦ op (Z a))
have h₁ : (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
    (op (Cofan.mk X π).pt ⟶
      Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x)))) →
  Eq (α := op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.lift fun (a : α) ↦ (π a).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (Z x)) (Cofan.mk X π).op)
Tactic: convert!
    desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))
      (Cofan.mk _ π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : HasProduct.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} Z
hf : IsLimit f
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)
⊢ IsColimit f.op
have refine : ∀ (x : Discrete α) (a : α),
  Eq (α := obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) { as := a : Discrete α } ⟶ f.op.pt)
    (((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).ι.app
        { as := a : Discrete α } ≫
      Iso.hom
        (Iso.refl ((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).pt))
    (f.op.ι.app { as := a })
Tactic: refine IsColimit.ofIsoColimit ((IsColimit.precomposeHomEquiv e _).2
    (IsColimit.whiskerEquivalence hf.op (Discrete.opposite α).symm))
    (Cocone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
⊢ (opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
have a : ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop =
  (hf.conePointUniqueUpToIso hf').op.inv.unop
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
⊢ ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop =
    (hf.conePointUniqueUpToIso hf').op.inv.unop
have a : ∀ (j : Discrete α),
  ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.π.app j =
    (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app j
Tactic: apply hf.hom_ext