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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_1₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_1₂ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
  (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.fst f.op f.op))
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_1₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_1₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.fst f.op f.op))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_1₃ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
  (Quiver.Hom.unop (Quiver.Hom.op (pushout.inl f f)))
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_1₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_1₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.fst f.op f.op))
refine_1₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inl f f)))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_1₄ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f) (pushout.inl f f)
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_1₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_1₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.fst f.op f.op))
refine_1₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inl f f)))
refine_1₄ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f) (pushout.inl f f)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_1₅ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (𝟙 (Opposite.unop (Opposite.op Y)) ≫ pushout.inl f f)
  (pushout.inl f f)
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_1₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_1₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.fst f.op f.op))
refine_1₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inl f f)))
refine_1₄ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f) (pushout.inl f f)
refine_1₅ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (𝟙 (Opposite.unop (Opposite.op Y)) ≫ pushout.inl f f)
    (pushout.inl f f)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_1₆ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (pushout.inl f f) (pushout.inl f f)
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2 : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
  (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2₁ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
  (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_2₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2₂ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
  (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.snd f.op f.op))
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_2₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_2₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.snd f.op f.op))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2₃ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
  (Quiver.Hom.unop (Quiver.Hom.op (pushout.inr f f)))
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_2₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_2₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.snd f.op f.op))
refine_2₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inr f f)))
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2₄ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
  (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f) (pushout.inr f f)
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_2₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_2₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.snd f.op f.op))
refine_2₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inr f f)))
refine_2₄ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f) (pushout.inr f f)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2₅ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (𝟙 (Opposite.unop (Opposite.op Y)) ≫ pushout.inr f f)
  (pushout.inr f f)
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_2₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_2₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.snd f.op f.op))
refine_2₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inr f f)))
refine_2₄ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f) (pushout.inr f f)
refine_2₅ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (𝟙 (Opposite.unop (Opposite.op Y)) ≫ pushout.inr f f)
    (pushout.inr f f)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
have refine_2₆ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (pushout.inr f f) (pushout.inr f f)
Tactic: rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
-- 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 ⋯)
⊢ IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)
have 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.hom (Iso.symm (pushoutIsoOpPullback f f)))
Tactic: refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitOp f.unop f.unop pullback.condition
      (by simp only [← op_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoOpPullback f f).symm) (.refl _) ?_ ?_ (by simp)
-- 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_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.hom (Iso.symm (pushoutIsoOpPullback f f)))
⊢ IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)
have 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.hom (Iso.symm (pushoutIsoOpPullback f f)))
Tactic: refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitOp f.unop f.unop pullback.condition
      (by simp only [← op_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoOpPullback f f).symm) (.refl _) ?_ ?_ (by simp)