awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
        Iso.hom (α_ K₁.X K₂.X K₃.X)
have rw : Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
  𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
    Iso.hom (α_ K₁.X K₂.X K₃.X)
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      Iso.hom (α_ K₁.X K₂.X K₃.X)
have erw : Eq (α :=
  (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂)
        K₃).X ⟶
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₂ K₃)).X)
  (Hom.f (Iso.hom (α_ K₁ K₂ K₃))) (Iso.hom (α_ K₁.X K₂.X K₃.X))
Tactic: erw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
                  ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))
                (Functor.obj (forget C c) K))) ≪≫
          (Iso.symm (tensorUnitIso C c) ⊗ᵢ Iso.refl (Functor.obj (forget C c) K))) ≪≫
        λ_ (Functor.obj (forget C c) K)).hom
have dsimp : CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)) =
  (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
            ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))
          (Functor.obj (forget C c) K)) ≫
      (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K))) ≫
    Iso.hom (λ_ (Functor.obj (forget C c) K))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
              ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))
            (Functor.obj (forget C c) K)) ≫
        (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K))) ≫
      Iso.hom (λ_ (Functor.obj (forget C c) K))
have erw : Eq (α :=
  Functor.obj (forget C c)
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
        ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)) K) ⟶
    Functor.obj (forget C c) K)
  (CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)))
  (CategoryStruct.comp (Y :=
    MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
      ((𝟙_ (GradedObject I C)) (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I))
      (Functor.obj (forget C c) K))
    (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K)) (Iso.hom (λ_ (Functor.obj (forget C c) K))))
Tactic: erw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                (Functor.obj (forget C c) K)
                (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
                  ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))))) ≪≫
          (Iso.refl (Functor.obj (forget C c) K) ⊗ᵢ Iso.symm (tensorUnitIso C c))) ≪≫
        ρ_ (Functor.obj (forget C c) K)).hom
have dsimp : CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)) =
  (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (Functor.obj (forget C c) K)
          (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
            ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
      (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c))) ≫
    Iso.hom (ρ_ (Functor.obj (forget C c) K))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (forget C c) K)
            (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
              ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
        (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c))) ≫
      Iso.hom (ρ_ (Functor.obj (forget C c) K))
have rw : Eq (α :=
  Functor.obj (forget C c)
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
        ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
    Functor.obj (forget C c) K)
  (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
  (𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
        (Functor.obj (forget C c) K)
        (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
    (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
    (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (Functor.obj (forget C c) K)
          (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
            ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
      (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))
have erw : Eq (α :=
  Functor.obj (forget C c)
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
        ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
    Functor.obj (forget C c) K)
  (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
  ((𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))
Tactic: erw [id_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 : f ≫ g = 0
⊢ Eq.{v_1 + 1} (α := op Z ⟶ op X) (g.op ≫ f.op) 0
have rw : (f ≫ g).op = 0
Tactic: rw [← op_comp, w, op_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 : f ≫ g = 0
rw : (f ≫ g).op = 0
⊢ Eq.{v_1 + 1} (α := op Z ⟶ op X) (g.op ≫ f.op) 0
have rw₁ : Eq.{v_1 + 1} (α := op Z ⟶ op X) (Quiver.Hom.op 0) 0
Tactic: rw [← op_comp, w, op_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 : f ≫ g = 0
rw : (f ≫ g).op = 0
rw₁ : Eq.{v_1 + 1} (α := op Z ⟶ op X) (Quiver.Hom.op 0) 0
⊢ Eq.{v_1 + 1} (α := op Z ⟶ op X) (g.op ≫ f.op) 0
have rw₂ : Eq.{v_1 + 1} (α := op Z ⟶ op X) 0 0
Tactic: rw [← op_comp, w, op_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 : f ≫ g = 0
⊢ Eq (α := X ⟶ image g) (f ≫ factorThruImage g) 0
have rw : CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) =
  CategoryStruct.comp (Y := image 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 : f ≫ g = 0
rw :
  CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
⊢ Eq (α := X ⟶ image g) (f ≫ factorThruImage g) 0
have rw₁ : f ≫ CategoryStruct.comp (Y := image g) (factorThruImage g) (image.ι g) =
  CategoryStruct.comp (Y := image 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 : f ≫ g = 0
rw :
  CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₁ :
  f ≫ CategoryStruct.comp (Y := image g) (factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
⊢ Eq (α := X ⟶ image g) (f ≫ factorThruImage g) 0
have rw₂ : f ≫ g = CategoryStruct.comp (Y := image 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 : f ≫ g = 0
rw :
  CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₁ :
  f ≫ CategoryStruct.comp (Y := image g) (factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₂ : f ≫ g = CategoryStruct.comp (Y := image g) 0 (image.ι g)
⊢ Eq (α := X ⟶ image g) (f ≫ factorThruImage g) 0
have rw₃ : Eq (α := X ⟶ Z) 0 (CategoryStruct.comp (Y := image 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 : f ≫ g = 0
rw :
  CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₁ :
  f ≫ CategoryStruct.comp (Y := image g) (factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₂ : f ≫ g = CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₃ : Eq (α := X ⟶ Z) 0 (CategoryStruct.comp (Y := image g) 0 (image.ι g))
⊢ Eq (α := X ⟶ image 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 : f ≫ g = 0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := Vᵒᵖ)
      (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op))
      (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
    (imageToKernel g.op f.op ⋯ :
      Quiver.Hom.{v_1, u_1} (V := Vᵒᵖ)
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op))
        (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)) :
      Quiver.Hom.{v_1, u_1} (V := Vᵒᵖ)
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op))
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
have h : 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 sorry) (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) sorry) ≫ 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)
Tactic: ext