awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op))
        (imageToKernel g.op f.op ⋯) (Subobject.arrow (kernelSubobject f.op)) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op))
        (CategoryStruct.comp (Y := op (image g))
          (Iso.hom (imageSubobjectIso g.op ≪≫ Iso.symm (imageOpOp g)) :
            Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op (image g))
          (Quiver.Hom.op (cokernel.desc f (factorThruImage g) ⋯) ≫ Iso.inv (kernelSubobjectIso f.op ≪≫ kernelOpOp f) :
            op (image g) ⟶ Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
        (Subobject.arrow (kernelSubobject f.op)) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
have h : Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
  (Iso.hom (imageSubobjectIso g.op) ≫
      CategoryStruct.comp (Y := op (image g.op.unop))
        (Iso.inv (imageUnopOp g.op) : image.{v_1, u_1} (X := op Z) (Y := op Y) g.op ⟶ op (image g.op.unop))
        (Quiver.Hom.op (factorThruImage g.op.unop) : op (image g.op.unop) ⟶ op Y) :
    Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
  (Iso.hom (imageSubobjectIso g.op) ≫
      CategoryStruct.comp (Y := op (image g))
        (Iso.inv (imageOpOp g) : image.{v_1, u_1} (X := op Z) (Y := op Y) g.op ⟶ op (image g))
        (Quiver.Hom.op (factorThruImage g) : op (image g) ⟶ op Y) :
    Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
Tactic: simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc,
    imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc,
    ← imageSubobject_arrow, ← imageUnopOp_inv_comp_op_factorThruImage g.op]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
⊢ g.unop ≫ f.unop = 0
have rw : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop (f ≫ g)) 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop (f ≫ g)) 0
⊢ g.unop ≫ f.unop = 0
have rw₁ : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop 0) 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop (f ≫ g)) 0
rw₁ : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop 0) 0
⊢ g.unop ≫ f.unop = 0
have rw₂ : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) 0 0
Tactic: rw [← unop_comp, w, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
⊢ Eq.{v_1 + 1} (α := X ⟶ image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) 0
have rw : Eq.{v_1 + 1} (α := X ⟶ Z)
  (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) (image.ι g))
  (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
Tactic: rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
⊢ Eq.{v_1 + 1} (α := X ⟶ image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) 0
have rw₁ : Eq.{v_1 + 1} (α := X ⟶ Z)
  (f ≫ CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (factorThruImage g) (image.ι g))
  (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
Tactic: rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₁ :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (f ≫ CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
⊢ Eq.{v_1 + 1} (α := X ⟶ image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) 0
have rw₂ : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
Tactic: rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₁ :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (f ≫ CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₂ : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
⊢ Eq.{v_1 + 1} (α := X ⟶ image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) 0
have rw₃ : Eq.{v_1 + 1} (α := X ⟶ Z) 0 (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
Tactic: rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₁ :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (f ≫ CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₂ : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₃ : Eq.{v_1 + 1} (α := X ⟶ Z) 0 (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
⊢ Eq.{v_1 + 1} (α := X ⟶ image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) 0
have rw₄ : Eq.{v_1 + 1} (α := X ⟶ Z) 0 0
Tactic: rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶
      Functor.obj Subobject.underlying (kernelSubobject f.unop))
    (imageToKernel g.unop f.unop ⋯ :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶
        Functor.obj Subobject.underlying (kernelSubobject f.unop))
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (imageUnopUnop g)) :
          Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
            Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
          unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶
        Functor.obj Subobject.underlying (kernelSubobject f.unop))
have h : Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
  (imageToKernel g.unop f.unop sorry ≫ (kernelSubobject f.unop).arrow :
    Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
  (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (imageUnopUnop g)) :
          Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) sorry) ≫
            Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
          unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
      (kernelSubobject f.unop).arrow :
    Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
⊢ Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (imageUnopUnop g)) :
            Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
              Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
            unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
        (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
have h : Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
  (imageToKernel g.unop f.unop sorry ≫ (kernelSubobject f.unop).arrow :
    Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
  (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (Iso.unop (imageUnopOp g))) :
          Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) sorry) ≫
            Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
          unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
      (kernelSubobject f.unop).arrow :
    Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
Tactic: dsimp only [imageUnopUnop]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).op = 0
have rw : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) (Quiver.Hom.op 0) 0
Tactic: rw [X.shape j i hij, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
i j : ι
hij : ¬c.symm.Rel i j
rw : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) (Quiver.Hom.op 0) 0
⊢ (X.d j i).op = 0
have rw₁ : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) 0 0
Tactic: rw [X.shape j i hij, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0
have rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
Tactic: rw [← op_comp, X.d_comp_d, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0
have rw₁ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) (Quiver.Hom.op 0) 0
Tactic: rw [← op_comp, X.d_comp_d, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
rw₁ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) (Quiver.Hom.op 0) 0
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0
have rw₂ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) 0 0
Tactic: rw [← op_comp, X.d_comp_d, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).op = 0
have rw : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) (Quiver.Hom.op 0) 0
Tactic: rw [X.shape j i hij, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
i j : ι
hij : ¬c.Rel i j
rw : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) (Quiver.Hom.op 0) 0
⊢ (X.d j i).op = 0
have rw₁ : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) 0 0
Tactic: rw [X.shape j i hij, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0
have rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
Tactic: rw [← op_comp, X.d_comp_d, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0
have rw₁ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) (Quiver.Hom.op 0) 0
Tactic: rw [← op_comp, X.d_comp_d, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
rw₁ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) (Quiver.Hom.op 0) 0
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0
have rw₂ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) 0 0
Tactic: rw [← op_comp, X.d_comp_d, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).unop = 0
have rw : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) (Quiver.Hom.unop 0) 0
Tactic: rw [X.shape j i hij, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
i j : ι
hij : ¬c.symm.Rel i j
rw : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) (Quiver.Hom.unop 0) 0
⊢ (X.d j i).unop = 0
have rw₁ : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) 0 0
Tactic: rw [X.shape j i hij, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0
have rw : (X.d x_2 x_1 ≫ X.d x_1 x).unop = 0
Tactic: rw [← unop_comp, X.d_comp_d, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).unop = 0
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0
have rw₁ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) (Quiver.Hom.unop 0) 0
Tactic: rw [← unop_comp, X.d_comp_d, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).unop = 0
rw₁ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) (Quiver.Hom.unop 0) 0
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0
have rw₂ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) 0 0
Tactic: rw [← unop_comp, X.d_comp_d, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).unop = 0
have rw : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) (Quiver.Hom.unop 0) 0
Tactic: rw [X.shape j i hij, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm
i j : ι
hij : ¬c.Rel i j
rw : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) (Quiver.Hom.unop 0) 0
⊢ (X.d j i).unop = 0
have rw₁ : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) 0 0
Tactic: rw [X.shape j i hij, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0
have rw : (X.d x_2 x_1 ≫ X.d x_1 x).unop = 0
Tactic: rw [← unop_comp, X.d_comp_d, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).unop = 0
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0
have rw₁ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) (Quiver.Hom.unop 0) 0
Tactic: rw [← unop_comp, X.d_comp_d, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).unop = 0
rw₁ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) (Quiver.Hom.unop 0) 0
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0
have rw₂ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) 0 0
Tactic: rw [← unop_comp, X.d_comp_d, unop_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X Y : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α := Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X ⟶ Functor.obj (opFunctor V c ⋙ opInverse V c) Y)
    (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          Y))
    (Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          X) ≫
      CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f)
have refine : Eq (α :=
  unop (Functor.obj (opFunctor V c ⋙ opInverse V c) Y) ⟶
    unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X))
  (Quiver.Hom.unop
    (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) sorry) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          Y)))
  (Quiver.Hom.unop
    (Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) sorry) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          X) ≫
      CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f))
Tactic: refine Quiver.Hom.unop_inj ?_