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 ⋯)
⊢ 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)))
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.inv (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]
-- 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.inv (pushoutIsoOpPullback 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)))
have 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))))
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]
-- 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.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))))
⊢ 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)))
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 (Quiver.Hom.unop (Iso.inv (pushoutIsoOpPullback f f)) ≫ pullback.fst f.unop f.unop))
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]
-- 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.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))
⊢ 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)))
have 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)))
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]
-- 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.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)))
⊢ 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)))
have 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)
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]
-- 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.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)
⊢ 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)))
have 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)
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]
-- 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.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)
⊢ 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)))
have 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)
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]
-- 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 ⋯)
⊢ 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 (α := 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))
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.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))
⊢ 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)
  (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))))
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.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))))
⊢ 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 (α := 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))
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.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))
⊢ 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)
  (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
  (Quiver.Hom.op (Quiver.Hom.unop (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.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)))
⊢ 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)
  (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ 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.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)
⊢ 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)
  (𝟙 (Opposite.op (Opposite.unop Y)) ≫ 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]