awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W_1 : C
w : W_1 ⟶ X
hw : Eq (α := W_1 ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
W : C
h : coequalizer u v ⟶ W
⊢ w ≫ coequalizer.π u v ≫ h = 0 ≫ h
have rw : (w ≫ coequalizer.π u v) ≫ h = 0 ≫ h
Tactic: rw [← Category.assoc, eq_whisker hw]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W_1 : C
w : W_1 ⟶ X
hw : Eq (α := W_1 ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
W : C
h : coequalizer u v ⟶ W
rw : (w ≫ coequalizer.π u v) ≫ h = 0 ≫ h
⊢ w ≫ coequalizer.π u v ≫ h = 0 ≫ h
have rw₁ : Eq (α := W_1 ⟶ W) (0 ≫ h) (0 ≫ h)
Tactic: rw [← Category.assoc, eq_whisker hw]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
⊢ u = v
have reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
Tactic: have reassoced {W : C} (h : coequalizer u v ⟶ W) : w ≫ coequalizer.π u v ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hw]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
⊢ w ≫ f = 0
have rw : w ≫ coequalizer.π u v ≫ m = 0
Tactic: rw [← hm, reassoced, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
rw : w ≫ coequalizer.π u v ≫ m = 0
⊢ w ≫ f = 0
have rw₁ : Eq (α := W ⟶ Y) (0 ≫ m) 0
Tactic: rw [← hm, reassoced, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
rw : w ≫ coequalizer.π u v ≫ m = 0
rw₁ : Eq (α := W ⟶ Y) (0 ≫ m) 0
⊢ w ≫ f = 0
have rw₂ : Eq.{v_1 + 1} (α := W ⟶ Y) 0 0
Tactic: rw [← hm, reassoced, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
⊢ u = v
have hwf : w ≫ f = 0
Tactic: have hwf : w ≫ f = 0 := by rw [← hm, reassoced, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
⊢ u = v
have obtain : ∀ (n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 sorry))
  (hn : n ≫ Fork.ι (KernelFork.ofι (Z := Z) 0 sorry) = w), u = v
Tactic: obtain ⟨n, hn⟩ := KernelFork.IsLimit.lift' l _ hwf
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : n ≫ Fork.ι (KernelFork.ofι (Z := Z) 0 ⋯) = w
⊢ u = v
have hn₁ : 0 = w
Tactic: rw [Fork.ι_ofι, HasZeroMorphisms.comp_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
⊢ u = v
have this : IsIso (Y := coequalizer u v) (coequalizer.π u v)
Tactic: have : IsIso (coequalizer.π u v) := by
      apply isIso_colimit_cocone_parallelPair_of_eq hn.symm hl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
this : IsIso (Y := coequalizer u v) (coequalizer.π u v)
⊢ u = v
have apply : Eq (α := Z_1 ⟶ coequalizer u v) (u ≫ coequalizer.π u v) (v ≫ coequalizer.π u v)
Tactic: apply (cancel_mono (coequalizer.π u v)).1
-- 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 g : X ⟶ Y
c : Cofork f g
⊢ IsColimit c ≃ IsLimit c.op
have f₁ : IsColimit c → IsLimit c.op
Tactic: apply equivOfSubsingletonOfSubsingleton
-- 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 g : X ⟶ Y
c : Cofork f g
f₁ : IsColimit c → IsLimit c.op
⊢ IsColimit c ≃ IsLimit c.op
have g₁ : IsLimit c.op → IsColimit c
Tactic: apply equivOfSubsingletonOfSubsingleton
-- 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 g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ IsColimit c ≃ IsLimit c.unop
have f₁ : IsColimit c → IsLimit c.unop
Tactic: apply equivOfSubsingletonOfSubsingleton
-- 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 g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
f₁ : IsColimit c → IsLimit c.unop
⊢ IsColimit c ≃ IsLimit c.unop
have g₁ : IsLimit c.unop → IsColimit c
Tactic: apply equivOfSubsingletonOfSubsingleton
-- 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 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
⊢ Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (pushout.inl f.op f.op) ≫ f.op.unop) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
have rw : Eq (α :=
  Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
    Opposite.unop (Opposite.op Y))
  (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
Tactic: rw [← unop_comp, ← unop_comp, pushout.condition]
-- 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 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
rw :
  Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
⊢ Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (pushout.inl f.op f.op) ≫ f.op.unop) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
have rw₁ : Eq.{v₁ + 1} (α :=
  Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
    Opposite.unop (Opposite.op Y))
  (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op))
Tactic: rw [← unop_comp, ← unop_comp, pushout.condition]
-- 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 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
rw :
  Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
rw₁ :
  Eq.{v₁ + 1} (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op))
⊢ Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (pushout.inl f.op f.op) ≫ f.op.unop) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
have rw₂ : Eq.{v₁ + 1} (α :=
  Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
    Opposite.unop (Opposite.op Y))
  (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op)) (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op))
Tactic: rw [← unop_comp, ← unop_comp, pushout.condition]
-- 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 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := X) (Z := Y) f f
h :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
⊢ Eq.{v₁ + 1} (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (pushout.inl f.unop f.unop) ≫ f.unop.op) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
have rw : Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
  (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
Tactic: rw [← op_comp, ← op_comp, pushout.condition]
-- 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 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := X) (Z := Y) f f
h :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
rw :
  Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
⊢ Eq.{v₁ + 1} (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (pushout.inl f.unop f.unop) ≫ f.unop.op) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
have rw₁ : Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
  (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop))
Tactic: rw [← op_comp, ← op_comp, pushout.condition]
-- 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 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := X) (Z := Y) f f
h :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
rw :
  Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
rw₁ :
  Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop))
⊢ Eq.{v₁ + 1} (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (pushout.inl f.unop f.unop) ≫ f.unop.op) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
have rw₂ : Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
  (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop)) (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop))
Tactic: rw [← op_comp, ← op_comp, pushout.condition]
-- 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 ⋯)
⊢ IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι 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 (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
Tactic: refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitUnop f.op f.op
      pullback.condition (by simp only [← unop_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoUnopPullback 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 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.hom (Iso.symm (pushoutIsoUnopPullback f f)))
⊢ IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι 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.hom (Iso.symm (pushoutIsoUnopPullback f f)))
Tactic: refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitUnop f.op f.op
      pullback.condition (by simp only [← unop_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoUnopPullback 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 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.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 (pullback.fst 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_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))
⊢ 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 (pullback.fst 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_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]