awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C) (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
      (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := Opposite.op (cokernel f))
        (Quiver.Hom.op (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) ⋯))
        (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯)))
    (Quiver.Hom.unop (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
have e_f : Eq.{v_1 + 1} (α :=
  Quiver.Hom.{v_1, u_1} (V := Cᵒᵖ)
    (Opposite.op (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
    (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
  (CategoryStruct.comp (Y := Opposite.op (cokernel f))
    (Quiver.Hom.op (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) sorry))
    (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) sorry))
  (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := Cᵒᵖ)
      (Opposite.op (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
      (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
    (CategoryStruct.comp (Y := Opposite.op (cokernel f))
      (Quiver.Hom.op (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) ⋯))
      (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯))
    (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
have e_f : Eq.{v_1 + 1} (α :=
  Opposite.op (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)) ⟶ Opposite.op Y)
  (CategoryStruct.comp (Y := equalizer.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op 0)
    (CategoryStruct.comp (Y := Opposite.op (cokernel f))
      (Quiver.Hom.op (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) sorry))
      (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) sorry))
    (equalizer.ι f.op 0))
  (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ≫ equalizer.ι f.op 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := cokernel f ⟶ cokernel f)
    (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) ⋯ ≫
        Quiver.Hom.unop (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯) :
      cokernel f ⟶ cokernel f)
    (𝟙 (cokernel f) : cokernel f ⟶ cokernel f)
have h : CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
    (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) sorry ≫
      Quiver.Hom.unop (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) sorry)) =
  coequalizer.π f 0 ≫ 𝟙 (cokernel f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ⟶ Y)
    (Quiver.Hom.unop (cokernel.π f.op) ≫ f) 0
have rw : Eq.{v_1 + 1} (α := Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ⟶ Y)
  (Quiver.Hom.unop (f.op ≫ cokernel.π f.op)) 0
Tactic: rw [← f.unop_op, ← unop_comp, f.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C) (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
      (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
    (CategoryStruct.comp (Y := kernel f) (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯)
      (Quiver.Hom.unop (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) ⋯)))
    (𝟙 (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
have rw : Eq.{v_1 + 1} (α :=
  Quiver.Hom.{v_1, u_1} (V := C) (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
    (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y := Opposite.op (kernel f)) (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) sorry)
      (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) sorry))))
  (Quiver.Hom.unop (𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
Tactic: rw [← unop_id, ← (kernel.lift f _ _).unop_op, ← unop_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C) (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
      (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := Opposite.op (kernel f)) (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) ⋯)
        (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯))))
    (Quiver.Hom.unop (𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
have e_f : Eq.{v_1 + 1} (α :=
  Quiver.Hom.{v_1, u_1} (V := Cᵒᵖ) (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
    (Opposite.op (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))))
  (CategoryStruct.comp (Y := Opposite.op (kernel f)) (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) sorry)
    (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) sorry)))
  (𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := Cᵒᵖ) (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
      (Opposite.op (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))))
    (CategoryStruct.comp (Y := Opposite.op (kernel f)) (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) ⋯)
      (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯)))
    (𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
have e_f : Eq.{v_1 + 1} (α :=
  Opposite.op X ⟶ Opposite.op (Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
  (CategoryStruct.comp (Y := coequalizer.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op 0)
    (coequalizer.π f.op 0)
    (CategoryStruct.comp (Y := Opposite.op (kernel f)) (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) sorry)
      (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) sorry))))
  (coequalizer.π f.op 0 ≫ 𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := kernel f ⟶ kernel f)
    (Quiver.Hom.unop (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) ⋯) ≫
        kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯ :
      kernel f ⟶ kernel f)
    (𝟙 (kernel f) : kernel f ⟶ kernel f)
have h : CategoryStruct.comp (Y := equalizer f 0)
    (Quiver.Hom.unop (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) sorry) ≫
      kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) sorry)
    (equalizer.ι f 0) =
  𝟙 (kernel f) ≫ equalizer.ι f 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
    (CategoryStruct.comp (Y := Opposite.op (image g.unop))
        (Quiver.Hom.op (image.ι g.unop) : Opposite.op (Opposite.unop A) ⟶ Opposite.op (image g.unop))
        (Iso.hom (imageUnopOp g) : Opposite.op (image g.unop) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) :
      Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
    (factorThruImage g : A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom,
    cokernelCompIsIso_hom, Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
  (inv (eqToHom sorry) ≫ factorThruImage g) (factorThruImage g)
Tactic: simp only [Category.assoc, Abelian.imageIsoImage_hom_comp_image_ι, kernel.lift_ι,
    Quiver.Hom.op_unop, cokernelIsoOfEq_hom_comp_desc_assoc, cokernel.π_desc_assoc,
    cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
    (inv (eqToHom ⋯) ≫ factorThruImage g) (factorThruImage g)
have simp : Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (inv (𝟙 A) ≫ factorThruImage g)
  (factorThruImage g)
Tactic: simp only [eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
    (inv (𝟙 A) ≫ factorThruImage g) (factorThruImage g)
have rw : Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (𝟙 A ≫ factorThruImage g)
  (factorThruImage g)
Tactic: rw [IsIso.inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
rw :
  Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (𝟙 A ≫ factorThruImage g)
    (factorThruImage g)
⊢ Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
    (inv (𝟙 A) ≫ factorThruImage g) (factorThruImage g)
have rw₁ : Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (factorThruImage g)
  (factorThruImage g)
Tactic: rw [IsIso.inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := A ⟶ Opposite.op (image g.unop))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := A) (Y := B) g)
        (factorThruImage g : A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
        (Iso.inv (imageUnopOp g) : image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (image g.unop)) :
      A ⟶ Opposite.op (image g.unop))
    (Quiver.Hom.op (image.ι g.unop) : Opposite.op (Opposite.unop A) ⟶ Opposite.op (image g.unop))
have rw : Eq (α := A ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (factorThruImage g : A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
  (CategoryStruct.comp (Y := Opposite.op (image g.unop))
      (Quiver.Hom.op (image.ι g.unop) : Opposite.op (Opposite.unop A) ⟶ Opposite.op (image g.unop))
      (Iso.hom (imageUnopOp g) : Opposite.op (image g.unop) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) :
    A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
Tactic: rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
rw :
  Eq (α := A ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (factorThruImage g : A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
    (CategoryStruct.comp (Y := Opposite.op (image g.unop))
        (Quiver.Hom.op (image.ι g.unop) : Opposite.op (Opposite.unop A) ⟶ Opposite.op (image g.unop))
        (Iso.hom (imageUnopOp g) : Opposite.op (image g.unop) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) :
      A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
⊢ Eq (α := A ⟶ Opposite.op (image g.unop))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := A) (Y := B) g)
        (factorThruImage g : A ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
        (Iso.inv (imageUnopOp g) : image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (image g.unop)) :
      A ⟶ Opposite.op (image g.unop))
    (Quiver.Hom.op (image.ι g.unop) : Opposite.op (Opposite.unop A) ⟶ Opposite.op (image g.unop))
have rw₁ : Eq.{v_1 + 1} (α := A ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (factorThruImage g) (factorThruImage g)
Tactic: rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (Opposite.unop B))
    (CategoryStruct.comp (Y := Opposite.op (image g.unop))
        (Iso.inv (imageUnopOp g) : image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (image g.unop))
        (Quiver.Hom.op (factorThruImage g.unop) : Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B)) :
      image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (Opposite.unop B))
    (image.ι g : image.{v_1, u_1} (X := A) (Y := B) g ⟶ B)
have rw : Eq (α := Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))
  (Quiver.Hom.op (factorThruImage g.unop) : Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))
  (CategoryStruct.comp (Y := image.{v_1, u_1} (X := A) (Y := B) g)
      (Iso.hom (imageUnopOp g) : Opposite.op (image g.unop) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
      (image.ι g : image.{v_1, u_1} (X := A) (Y := B) g ⟶ B) :
    Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))
Tactic: rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B : Cᵒᵖ
g : A ⟶ B
rw :
  Eq (α := Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))
    (Quiver.Hom.op (factorThruImage g.unop) : Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := A) (Y := B) g)
        (Iso.hom (imageUnopOp g) : Opposite.op (image g.unop) ⟶ image.{v_1, u_1} (X := A) (Y := B) g)
        (image.ι g : image.{v_1, u_1} (X := A) (Y := B) g ⟶ B) :
      Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))
⊢ Eq (α := image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (Opposite.unop B))
    (CategoryStruct.comp (Y := Opposite.op (image g.unop))
        (Iso.inv (imageUnopOp g) : image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (image g.unop))
        (Quiver.Hom.op (factorThruImage g.unop) : Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B)) :
      image.{v_1, u_1} (X := A) (Y := B) g ⟶ Opposite.op (Opposite.unop B))
    (image.ι g : image.{v_1, u_1} (X := A) (Y := B) g ⟶ B)
have rw₁ : Eq (α := Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B)) (Quiver.Hom.op (factorThruImage g.unop))
  (Quiver.Hom.op (factorThruImage g.unop))
Tactic: rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Φ : Preradical.{v, u} C
X : C
⊢ Φ.r.map (Φ.ι.app X) = Φ.ι.app (Φ.r.obj X)
have rw : Φ.r.map (Φ.ι.app X) ≫ Φ.ι.app X = Φ.ι.app (Φ.r.obj X) ≫ Φ.ι.app X
Tactic: rw [← cancel_mono (Φ.ι.app X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Φ : Preradical.{v, u} C
inst_2 : Φ.IsIdempotent
X : C
⊢ IsIso (Φ.r.map (Φ.ι.app X))
have rw : IsIso (X := Φ.r.obj (Φ.r.obj X)) (Φ.ι.app (Φ.r.obj X))
Tactic: rw [r_map_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Φ : Preradical.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : Functor.{v_1, v, u_1, u} D C
⊢ Mono (F.whiskerLeft Φ.ι)
have rw : ∀ (k : D), Mono ((F.whiskerLeft Φ.ι).app k)
Tactic: rw [NatTrans.mono_iff_mono_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Φ : Preradical.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : Functor.{v_1, v, u_1, u} D C
k : D
⊢ Mono ((F.whiskerLeft Φ.ι).app k)
have dsimp : Mono (X := Φ.r.obj (F.obj k)) (Φ.ι.app (F.obj k))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
⊢ Mono (X := ShortComplex.X₁ Φ.shortComplex) (ShortComplex.f Φ.shortComplex)
have dsimp : Mono Φ.ι
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ Mono (X := ShortComplex.X₁ (Φ.shortComplexObj X)) (ShortComplex.f (Φ.shortComplexObj X))
have dsimp : Mono (Φ.ι.app X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ Epi (X := ShortComplex.X₂ (Φ.shortComplexObj X)) (ShortComplex.g (Φ.shortComplexObj X))
have dsimp : Epi (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X
have rw : (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ)) ≫ (Φ.colon Ψ).ι).app X = Φ.ι.app X
Tactic: rw [← NatTrans.comp_app, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
rw : (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ)) ≫ (Φ.colon Ψ).ι).app X = Φ.ι.app X
⊢ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X
have rw₁ : Φ.obj (P := Over.isMono (𝟭 C)).hom.app X = Φ.ι.app X
Tactic: rw [← NatTrans.comp_app, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X) ↔
    IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
have mp : IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X) →
  IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
mp :
  IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X) →
    IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X) ↔
    IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
have mpr : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X)) →
  IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
⊢ Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) ((Φ.colon Ψ).ι.app X ≫ NatTrans.app Φ.π X) 0
have rw : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (NatTrans.app (Φ.colonπ Ψ) X ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
Tactic: rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
rw : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (NatTrans.app (Φ.colonπ Ψ) X ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
⊢ Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) ((Φ.colon Ψ).ι.app X ≫ NatTrans.app Φ.π X) 0
have rw₁ : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (0 ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
Tactic: rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
rw : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (NatTrans.app (Φ.colonπ Ψ) X ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
rw₁ : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (0 ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
⊢ Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) ((Φ.colon Ψ).ι.app X ≫ NatTrans.app Φ.π X) 0
have rw₂ : Eq.{u_2 + 1} (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) 0 0
Tactic: rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
have mpr : ∀
  (inv :
    (Φ.colon Ψ).r.obj X ⟶
      Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) sorry))
  (hinv : inv ≫ Fork.ι (KernelFork.ofι (Φ.ι.app X) sorry) = (Φ.colon Ψ).ι.app X),
  IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
Tactic: obtain ⟨inv, hinv⟩ :=
      KernelFork.IsLimit.lift' (Φ.isLimitKernelForkObj X) ((colon Φ Ψ).ι.app X) (by
        rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp])