awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.π ≫
      CategoryStruct.comp (Y := S₁.homology)
        (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData)
          (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left))
        (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫
          CategoryStruct.comp (Y := S₂.rightHomology)
              (S₂.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₂) S₂.homologyData.right S₂.rightHomologyData)
              (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData h₂) ≫
            h₂.ι) =
    h₁.i ≫ φ.τ₂ ≫ h₂.p

Tactic:
simp only [assoc, rightHomologyι_naturality', rightHomologyι_naturality'_assoc,
    leftHomologyπ_naturality'_assoc, HomologyData.comm_assoc, p_opcyclesMap'_assoc,
    id_τ₂, p_opcyclesMap', id_comp, cyclesMap'_i_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.rightHomologyι_naturality'_assoc, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.ShortComplex.p_opcyclesMap', CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc, CategoryTheory.ShortComplex.rightHomologyι_naturality', CategoryTheory.ShortComplex.id_τ₂, CategoryTheory.ShortComplex.cyclesMap'_i_assoc, CategoryTheory.ShortComplex.p_opcyclesMap'_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.cycles ⟶ S₂.opcycles)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι) :
      S₁.cycles ⟶ S₂.opcycles)
    (S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles : S₁.cycles ⟶ S₂.opcycles)

Tactic:
simp only [homologyι_naturality, homology_π_ι_assoc, p_opcyclesMap]

Premises used: CategoryTheory.ShortComplex.homologyι_naturality, CategoryTheory.ShortComplex.homology_π_ι_assoc, CategoryTheory.ShortComplex.p_opcyclesMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
dsimp : homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv
⊢ (homologyMap' φ h₁ h₂).op.unop = Quiver.Hom.unop (h₂.iso.inv.op ≫ homologyMap' (opMap φ) h₂.op h₁.op ≫ h₁.iso.hom.op)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
have :
  ∀ (γ : HomologyMapData φ h₁ h₂),
    homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv

Tactic:
have γ : HomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
γ : HomologyMapData φ h₁ h₂
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv

Tactic:
simp only [γ.homologyMap'_eq, γ.op.homologyMap'_eq, HomologyData.op_left,
      HomologyMapData.op_left, RightHomologyMapData.op_φH, Quiver.Hom.unop_op, assoc,
      ← γ.comm_assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.ShortComplex.HomologyMapData.op_left, CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyMapData.op_φH, Quiver.Hom.unop_op, CategoryTheory.ShortComplex.HomologyMapData.op, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.HomologyData.op_left, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
dsimp :
  Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology)
    (Quiver.Hom.op (homologyMap' φ S₁.homologyData S₂.homologyData))
    (CategoryStruct.comp (Y := S₂.op.homology)
      (Iso.inv (Iso.symm S₂.op.leftHomologyIso ≪≫ S₂.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₂.rightHomologyIso)))
      (CategoryStruct.comp (Y := S₁.op.homology) (homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData)
        (Iso.hom (Iso.symm S₁.op.leftHomologyIso ≪≫ S₁.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₁.rightHomologyIso)))))
⊢ Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology) (Quiver.Hom.op (homologyMap φ))
    (Iso.inv S₂.homologyOpIso ≫ homologyMap (opMap φ) ≫ Iso.hom S₁.homologyOpIso)

Tactic:
dsimp only [homologyMap, homologyOpIso]

Premises used: CategoryTheory.ShortComplex.homologyOpIso, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw :
  Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology)
    (S₂.homologyData.iso.inv.op ≫
      homologyMap' (opMap φ) S₂.homologyData.op S₁.homologyData.op ≫ S₁.homologyData.iso.hom.op)
    (CategoryStruct.comp (Y := S₂.op.homology)
      (Iso.inv (Iso.symm S₂.op.leftHomologyIso ≪≫ S₂.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₂.rightHomologyIso)))
      (CategoryStruct.comp (Y := S₁.op.homology) (homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData)
        (Iso.hom (Iso.symm S₁.op.leftHomologyIso ≪≫ S₁.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₁.rightHomologyIso)))))
⊢ Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology)
    (Quiver.Hom.op (homologyMap' φ S₁.homologyData S₂.homologyData))
    (CategoryStruct.comp (Y := S₂.op.homology)
      (Iso.inv (Iso.symm S₂.op.leftHomologyIso ≪≫ S₂.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₂.rightHomologyIso)))
      (CategoryStruct.comp (Y := S₁.op.homology) (homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData)
        (Iso.hom (Iso.symm S₁.op.leftHomologyIso ≪≫ S₁.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₁.rightHomologyIso)))))

Tactic:
rw [homologyMap'_op]

Premises used: CategoryTheory.ShortComplex.homologyMap'_op
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
dsimp :
  Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology)
    (S₂.homologyData.iso.inv.op ≫
      leftHomologyMap' (opMap φ) S₂.homologyData.op.left S₁.homologyData.op.left ≫ S₁.homologyData.iso.hom.op)
    (CategoryStruct.comp (Y := S₂.op.homology)
      (CategoryStruct.comp (Y := S₂.op.leftHomology)
        (CategoryStruct.comp (Y := Opposite.op S₂.rightHomology)
          (Quiver.Hom.op
            (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv))
          (leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData))
        (leftHomologyMap' (𝟙 S₂.op) S₂.op.leftHomologyData S₂.op.homologyData.left))
      (CategoryStruct.comp (Y := S₁.op.homology)
        (leftHomologyMap' (opMap φ) S₂.op.homologyData.left S₁.op.homologyData.left)
        (CategoryStruct.comp (Y := S₁.op.leftHomology)
          (leftHomologyMap' (𝟙 S₁.op) S₁.op.homologyData.left S₁.op.leftHomologyData)
          (CategoryStruct.comp (Y := Opposite.op S₁.rightHomology)
            (leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op :
              S₁.op.leftHomologyData.H ⟶ S₁.rightHomologyData.op.H)
            (Quiver.Hom.op
              (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData))))))
⊢ Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology)
    (S₂.homologyData.iso.inv.op ≫
      homologyMap' (opMap φ) S₂.homologyData.op S₁.homologyData.op ≫ S₁.homologyData.iso.hom.op)
    (CategoryStruct.comp (Y := S₂.op.homology)
      (Iso.inv (Iso.symm S₂.op.leftHomologyIso ≪≫ S₂.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₂.rightHomologyIso)))
      (CategoryStruct.comp (Y := S₁.op.homology) (homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData)
        (Iso.hom (Iso.symm S₁.op.leftHomologyIso ≪≫ S₁.leftHomologyOpIso ≪≫ Iso.op (Iso.symm S₁.rightHomologyIso)))))

Tactic:
dsimp only [Iso.symm, Iso.trans, Iso.op, Iso.refl, rightHomologyIso, leftHomologyIso,
    leftHomologyOpIso, leftHomologyMapIso', rightHomologyMapIso',
    LeftHomologyData.leftHomologyIso, homologyMap']

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.Iso.op, CategoryTheory.ShortComplex.leftHomologyMapIso', CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.leftHomologyOpIso, CategoryTheory.ShortComplex.leftHomologyIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := Opposite.op S₂.homology ⟶ Opposite.op S₁.homology)
    (S₂.homologyData.iso.inv.op ≫
      leftHomologyMap' (opMap φ) S₂.homologyData.op.left S₁.homologyData.op.left ≫ S₁.homologyData.iso.hom.op)
    (CategoryStruct.comp (Y := S₂.op.homology)
      (CategoryStruct.comp (Y := S₂.op.leftHomology)
        (CategoryStruct.comp (Y := Opposite.op S₂.rightHomology)
          (Quiver.Hom.op
            (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv))
          (leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData))
        (leftHomologyMap' (𝟙 S₂.op) S₂.op.leftHomologyData S₂.op.homologyData.left))
      (CategoryStruct.comp (Y := S₁.op.homology)
        (leftHomologyMap' (opMap φ) S₂.op.homologyData.left S₁.op.homologyData.left)
        (CategoryStruct.comp (Y := S₁.op.leftHomology)
          (leftHomologyMap' (𝟙 S₁.op) S₁.op.homologyData.left S₁.op.leftHomologyData)
          (CategoryStruct.comp (Y := Opposite.op S₁.rightHomology)
            (leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op :
              S₁.op.leftHomologyData.H ⟶ S₁.rightHomologyData.op.H)
            (Quiver.Hom.op
              (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData))))))

Tactic:
simp only [assoc, rightHomologyMap'_op, op_comp, ← leftHomologyMap'_comp_assoc, id_comp,
    opMap_id, comp_id, HomologyData.op_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.ShortComplex.opMap_id, CategoryTheory.ShortComplex.leftHomologyMap'_comp_assoc, CategoryTheory.ShortComplex.rightHomologyMap'_op, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.HomologyData.op_left, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₂.op.homology ⟶ Opposite.op S₁.homology)
    (homologyMap (opMap φ) ≫ Iso.hom S₁.homologyOpIso : S₂.op.homology ⟶ Opposite.op S₁.homology)
    (CategoryStruct.comp (Y := Opposite.op S₂.homology) (Iso.hom S₂.homologyOpIso) (Quiver.Hom.op (homologyMap φ)) :
      S₂.op.homology ⟶ Opposite.op S₁.homology)

Tactic:
simp [homologyMap_op]

Premises used: CategoryTheory.ShortComplex.homologyMap_op
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := Opposite.op S₂.homology ⟶ S₁.op.homology)
    (CategoryStruct.comp (Y := Opposite.op S₁.homology) (Quiver.Hom.op (homologyMap φ)) (Iso.inv S₁.homologyOpIso) :
      Opposite.op S₂.homology ⟶ S₁.op.homology)
    (Iso.inv S₂.homologyOpIso ≫ homologyMap (opMap φ) : Opposite.op S₂.homology ⟶ S₁.op.homology)

Tactic:
simp [homologyMap_op]

Premises used: CategoryTheory.ShortComplex.homologyMap_op
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
rw₁ : x ≫ S.f ≫ S.g = 0
rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
rw₃ rw₄ : Eq.{v + 1} (α := A ⟶ S.X₃) 0 0
⊢ k ≫ S.g = 0

Tactic:
rw [hx, assoc, S.zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
dsimp : Eq (α := A ⟶ S.homology) (S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles k ⋯ ≫ S.homologyπ) 0

Tactic:
dsimp only [homologyπ]

Premises used: CategoryTheory.ShortComplex.homologyπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : Eq (α := A ⟶ S.homology) (0 ≫ Iso.hom S.leftHomologyIso) 0
rw₁ rw₂ : Eq.{v + 1} (α := A ⟶ S.homology) 0 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0

Tactic:
rw [S.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc k x hx, zero_comp]

Premises used: CategoryTheory.ShortComplex.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
rw₂ rw₃ : Eq.{v + 1} (α := S.X₁ ⟶ A) 0 0
⊢ S.f ≫ k = 0

Tactic:
rw [hx, S.zero_assoc, zero_comp]

Premises used: CategoryTheory.ShortComplex.zero_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
dsimp : Eq (α := S.homology ⟶ A) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯) 0
⊢ Eq (α := S.homology ⟶ A) (S.homologyι ≫ S.descOpcycles k ⋯) 0

Tactic:
dsimp only [homologyι]

Premises used: CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι ≫ S.descOpcycles k ⋯) 0
rw₁ : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := S.homology ⟶ A) 0 0
⊢ Eq (α := S.homology ⟶ A) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯) 0

Tactic:
rw [assoc, S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
⊢ Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0

Tactic:
simp only [← cancel_epi φ.τ₁, ← toCycles_naturality_assoc,
      IsIso.hom_inv_id_assoc, toCycles_comp_homologyπ, comp_zero]

Premises used: CategoryTheory.ShortComplex.toCycles_comp_homologyπ, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.Limits.comp_zero, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.ShortComplex.toCycles_naturality_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
⊢ Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0

Tactic:
have h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0 := by
    simp only [← cancel_epi φ.τ₁, ← toCycles_naturality_assoc,
      IsIso.hom_inv_id_assoc, toCycles_comp_homologyπ, comp_zero]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
have :
  ∀
    (z :
      Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
          (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
        S₁.homology)
    (hz :
      Eq (α := S₂.cycles ⟶ S₁.homology)
        (Cofork.π (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯) ≫ z : S₂.cycles ⟶ S₁.homology)
        (inv (cyclesMap φ) ≫ S₁.homologyπ : S₂.cycles ⟶ S₁.homology)),
    IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
have ⟨z, hz⟩ := CokernelCofork.IsColimit.desc' S₂.homologyIsCokernel _ h
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
⟨⟨z, ?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : homologyMap φ ≫ z = 𝟙 S₁.homology
refine_2 : z ≫ homologyMap φ = 𝟙 S₂.homology
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
refine ⟨⟨z, ?_, ?_⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ ≫ z) = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₁ : cyclesMap φ ≫ S₂.homologyπ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₂ :
  CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) (inv (cyclesMap φ) ≫ S₁.homologyπ) = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₃ : S₁.homologyπ = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₄ refine_1₅ : Eq (α := S₁.cycles ⟶ S₁.homology) S₁.homologyπ S₁.homologyπ
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology

Tactic:
rw [← cancel_epi S₁.homologyπ, homologyπ_naturality_assoc, hz,
      IsIso.hom_inv_id_assoc, comp_id]

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ_naturality_assoc, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_2 : S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₁ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ) : S₂.cycles ⟶ S₁.cycles)
      (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology) =
    S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₂ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ)) (cyclesMap φ ≫ S₂.homologyπ) = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₃ : S₂.homologyπ = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₄ refine_2₅ : Eq (α := S₂.cycles ⟶ S₂.homology) S₂.homologyπ S₂.homologyπ
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology

Tactic:
rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ_naturality, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.cancel_epi