awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)) ⋯))
      (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯))
    (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
⊢ 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)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)) ⋯))
        (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯))
      (equalizer.ι f.op 0))
    (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ≫ equalizer.ι f.op 0)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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} (α :=
    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)) ⋯))
        (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯))
      (equalizer.ι f.op 0))
    (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ≫ equalizer.ι f.op 0)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
h :
  CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) ⋯ ≫
        Quiver.Hom.unop (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯)) =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
⊢ CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) ⋯ ≫
        Quiver.Hom.unop (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯)) =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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
⊢ 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

Tactic:
rw [← f.unop_op, ← unop_comp, f.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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} (α := 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:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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} (α := Opposite.op Y ⟶ Opposite.op (kernel f)) (f.op ≫ Quiver.Hom.op (kernel.ι f)) 0

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)) ⋯)
        (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)))
⊢ 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)))

Tactic:
rw [← unop_id, ← (kernel.lift f _ _).unop_op, ← unop_comp]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Limits.kernel.lift, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)) ⋯)
      (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))
⊢ 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)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)) ⋯)
        (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯))))
    (coequalizer.π f.op 0 ≫ 𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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} (α :=
    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)) ⋯)
        (Quiver.Hom.op (kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯))))
    (coequalizer.π f.op 0 ≫ 𝟙 (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
h :
  CategoryStruct.comp (Y := equalizer f 0)
      (Quiver.Hom.unop (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) ⋯) ≫
        kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯)
      (equalizer.ι f 0) =
    𝟙 (kernel f) ≫ equalizer.ι f 0
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
⊢ CategoryStruct.comp (Y := equalizer f 0)
      (Quiver.Hom.unop (cokernel.desc f.op (Quiver.Hom.op (kernel.ι f)) ⋯) ≫
        kernel.lift f (Quiver.Hom.unop (cokernel.π f.op)) ⋯)
      (equalizer.ι f 0) =
    𝟙 (kernel f) ≫ equalizer.ι f 0

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
⊢ Eq (α :=
    Opposite.unop (cokernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ⟶ Opposite.unop (Opposite.op X))
    (Quiver.Hom.unop (cokernel.π f.op)) (Iso.hom (cokernelOpUnop f) ≫ kernel.ι f ≫ eqToHom ⋯)

Tactic:
simp [cokernelOpUnop]

Premises used: CategoryTheory.cokernelOpUnop
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
⊢ Eq (α :=
    Opposite.unop (Opposite.op Y) ⟶ Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
    (Quiver.Hom.unop (kernel.ι f.op)) (eqToHom ⋯ ≫ cokernel.π f ≫ Iso.inv (kernelOpUnop f))

Tactic:
simp [kernelOpUnop]

Premises used: CategoryTheory.kernelOpUnop
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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 B) ⟶ Opposite.op (kernel g.unop)) (Quiver.Hom.op (kernel.ι g.unop))
    (eqToHom ⋯ ≫ cokernel.π g ≫ Iso.inv (kernelUnopOp g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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 (cokernel g.unop) ⟶ Opposite.op (Opposite.unop A)) (Quiver.Hom.op (cokernel.π g.unop))
    (Iso.hom (cokernelUnopOp g) ≫ kernel.ι g ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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)

Tactic:
simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom,
    cokernelCompIsIso_hom, Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Limits.cokernelCompIsIso_hom, CategoryTheory.Iso.op, CategoryTheory.Iso.trans, CategoryTheory.imageUnopOp, CategoryTheory.Abelian.coimageIsoImage'_hom, CategoryTheory.Iso.symm, CategoryTheory.Limits.cokernelEpiComp_hom, CategoryTheory.cokernelOpOp_inv
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
simp :
  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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.cokernel.π_desc_assoc, Quiver.Hom.op_unop, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc_assoc, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)
⊢ 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)

Tactic:
simp only [eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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)
rw₁ rw₂ :
  Eq.{v_1 + 1} (α := Opposite.op (Opposite.unop A) ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (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)

Tactic:
rw [IsIso.inv_id, Category.id_comp]

Premises used: CategoryTheory.IsIso.inv_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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 (image g.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) ⟶ B)
    (Quiver.Hom.op (factorThruImage g.unop) : Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B))

Tactic:
simp only [← cancel_epi (image.ι g.unop).op, ← Category.assoc, image_ι_op_comp_imageUnopOp_hom,
    ← op_comp, image.fac, Quiver.Hom.op_unop]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.op, CategoryTheory.image_ι_op_comp_imageUnopOp_hom, Quiver.Hom.op_unop, Quiver.Hom.unop, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image.fac, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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)
rw₁ rw₂ : Eq.{v_1 + 1} (α := A ⟶ image.{v_1, u_1} (X := A) (Y := B) g) (factorThruImage g) (factorThruImage 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))

Tactic:
rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.image_ι_op_comp_imageUnopOp_hom
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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))
rw₁ rw₂ :
  Eq (α := Opposite.op (image g.unop) ⟶ Opposite.op (Opposite.unop B)) (Quiver.Hom.op (factorThruImage g.unop))
    (Quiver.Hom.op (factorThruImage g.unop))
⊢ 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)

Tactic:
rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.imageUnopOp_hom_comp_image_ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Φ : Preradical.{v, u} C
X : C
rw : Φ.r.map (Φ.ι.app X) ≫ Φ.ι.app X = Φ.ι.app (Φ.r.obj X) ≫ Φ.ι.app X
⊢ Φ.r.map (Φ.ι.app X) = Φ.ι.app (Φ.r.obj X)

Tactic:
rw [← cancel_mono (Φ.ι.app X)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.Preradical.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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 X = Φ.ι.app (Φ.r.obj X) ≫ Φ.ι.app X

Tactic:
Φ.ι.naturality (Φ.ι.app X)

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.Preradical.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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 X = Φ.ι.app (Φ.r.obj X) ≫ Φ.ι.app X

Tactic:
exact Φ.ι.naturality (Φ.ι.app X)

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.Preradical.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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 (X := Φ.r.obj (Φ.r.obj X)) (Φ.ι.app (Φ.r.obj X))

Tactic:
inferInstanceAs (IsIso ((Functor.whiskerLeft Φ.r Φ.ι).app X))

Premises used: _private.0.CategoryTheory.Abelian.Preradical.instIsIsoAppιObjROfIsIdempotent._proof_1
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Φ : Preradical.{v, u} C
inst_2 : Φ.IsIdempotent
X : C
rw : IsIso (X := Φ.r.obj (Φ.r.obj X)) (Φ.ι.app (Φ.r.obj X))
⊢ IsIso (Φ.r.map (Φ.ι.app X))

Tactic:
rw [r_map_ι_app]

Premises used: CategoryTheory.Abelian.Preradical.r_map_ι_app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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 (X := Φ.r.obj (Φ.r.obj X)) (Φ.ι.app (Φ.r.obj X))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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
rw : ∀ (k : D), Mono ((F.whiskerLeft Φ.ι).app k)
⊢ Mono (F.whiskerLeft Φ.ι)

Tactic:
rw [NatTrans.mono_iff_mono_app]

Premises used: CategoryTheory.NatTrans.mono_iff_mono_app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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
dsimp : Mono (X := Φ.r.obj (F.obj k)) (Φ.ι.app (F.obj k))
⊢ Mono ((F.whiskerLeft Φ.ι).app k)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic
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 (X := Φ.r.obj (F.obj k)) (Φ.ι.app (F.obj k))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
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
⊢ Eq (α := Φ.r ⟶ Φ.quotient) (Φ.ι ≫ Φ.π) 0

Tactic:
cokernel.condition _

Premises used: CategoryTheory.Limits.cokernel.condition, CategoryTheory.Abelian.Preradical.π, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
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
dsimp : Mono Φ.ι
⊢ Mono (X := ShortComplex.X₁ Φ.shortComplex) (ShortComplex.f Φ.shortComplex)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
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 Φ.ι

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
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
⊢ Epi (Y := Φ.quotient) Φ.π

Tactic:
infer_instance