awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)
⊢ Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ)
    (opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData)

Tactic:
rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.opcyclesMap'_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.rightHomology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap φ) (Iso.hom h₂.rightHomologyIso))
    (Iso.hom h₁.rightHomologyIso ≫ γ.φH)

Tactic:
simp only [γ.rightHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_eq, CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.opcycles ⟶ h₂.Q) (CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ) (Iso.hom h₂.opcyclesIso))
    (Iso.hom h₁.opcyclesIso ≫ γ.φQ)

Tactic:
simp only [γ.opcyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (h₂.op.p ≫ ψ.φK.op).unop = ((opMap φ).τ₂ ≫ h₁.op.p).unop

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ Quiver.Hom.unop (ψ.φK.op ≫ h₁.op.g') = (h₂.op.g' ≫ (opMap φ).τ₃).unop

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ Quiver.Hom.unop (ψ.φH.op ≫ h₁.op.ι) = (h₂.op.ι ≫ ψ.φK.op).unop

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (h₂.unop.p ≫ ψ.φK.unop).op = ((unopMap φ).τ₂ ≫ h₁.unop.p).op

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φK.unop ≫ h₁.unop.g').op = (h₂.unop.g' ≫ (unopMap φ).τ₃).op

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φH.unop ≫ h₁.unop.ι).op = (h₂.unop.ι ≫ ψ.φK.unop).op

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ Quiver.Hom.unop (ψ.φQ.op ≫ h₁.op.i) = (h₂.op.i ≫ (opMap φ).τ₂).unop

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.op.f' ≫ ψ.φQ.op).unop = ((opMap φ).τ₁ ≫ h₁.op.f').unop

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.op.π ≫ ψ.φH.op).unop = Quiver.Hom.unop (ψ.φQ.op ≫ h₁.op.π)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.unop ≫ h₁.unop.i).op = (h₂.unop.i ≫ (unopMap φ).τ₂).op

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.unop.f' ≫ ψ.φQ.unop).op = ((unopMap φ).τ₁ ≫ h₁.unop.f').op

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.unop.π ≫ ψ.φH.unop).op = (ψ.φQ.unop ≫ h₁.unop.π).op

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
dsimp :
  Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁)
    (CategoryStruct.comp (Y := Opposite.op S.cycles) (Iso.hom S.opcyclesOpIso) (Quiver.Hom.op S.toCycles) :
      S.op.opcycles ⟶ Opposite.op S.X₁)
    (S.op.fromOpcycles : S.op.opcycles ⟶ S.op.X₃)

Tactic:
dsimp [opcyclesOpIso, toCycles]

Premises used: CategoryTheory.ShortComplex.opcyclesOpIso, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
rw₁ :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    S.op.g
rw₂ : S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g
rw₃ : S.leftHomologyData.i.op ≫ S.leftHomologyData.f'.op = S.op.g
rw₄ : (S.leftHomologyData.f' ≫ S.leftHomologyData.i).op = S.op.g
rw₅ : S.f.op = S.op.g
rw₆ rw₇ : S.f.op = S.f.op
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles

Tactic:
rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]

Premises used: CategoryTheory.op_comp, CategoryTheory.ShortComplex.op_g, CategoryTheory.ShortComplex.p_fromOpcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.ShortComplex.LeftHomologyData.op_p, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
dsimp :
  Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S.opcycles) (Quiver.Hom.op S.fromOpcycles) (Iso.inv S.cyclesOpIso) :
      Opposite.op S.X₃ ⟶ S.op.cycles)
    (S.op.toCycles : S.op.X₁ ⟶ S.op.cycles)

Tactic:
dsimp [cyclesOpIso, fromOpcycles]

Premises used: CategoryTheory.ShortComplex.cyclesOpIso, CategoryTheory.ShortComplex.fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₂ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    S.op.f
rw₃ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.i = S.op.f
rw₄ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.p.op = S.op.f
rw₅ : (S.rightHomologyData.p ≫ S.rightHomologyData.g').op = S.op.f
rw₆ : S.g.op = S.op.f
rw₇ rw₈ : S.g.op = S.g.op
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles

Tactic:
rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.toCycles_i, CategoryTheory.ShortComplex.op_f, CategoryTheory.ShortComplex.RightHomologyData.op_i, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
dsimp :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles (Iso.hom S.leftHomologyData.op.opcyclesIso) =
    Quiver.Hom.op S.iCycles
⊢ Eq (α := S.op.X₂ ⟶ Opposite.op S.cycles) (S.op.pOpcycles ≫ Iso.hom S.opcyclesOpIso) (Quiver.Hom.op S.iCycles)

Tactic:
dsimp [opcyclesOpIso]

Premises used: CategoryTheory.ShortComplex.opcyclesOpIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
rw : S.leftHomologyData.op.p = Quiver.Hom.op S.iCycles
⊢ CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles (Iso.hom S.leftHomologyData.op.opcyclesIso) =
    Quiver.Hom.op S.iCycles

Tactic:
rw [← S.leftHomologyData.op.p_comp_opcyclesIso_inv, assoc,
    Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv, CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyData.op
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
⊢ S.leftHomologyData.op.p = Quiver.Hom.op S.iCycles

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
dsimp :
  CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    Quiver.Hom.op S.pOpcycles
⊢ Eq (α := Opposite.op S.opcycles ⟶ S.op.X₂) (Iso.inv S.cyclesOpIso ≫ S.op.iCycles) (Quiver.Hom.op S.pOpcycles)

Tactic:
dsimp [cyclesOpIso]

Premises used: CategoryTheory.ShortComplex.cyclesOpIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw : S.rightHomologyData.op.i = Quiver.Hom.op S.pOpcycles
⊢ CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    Quiver.Hom.op S.pOpcycles

Tactic:
rw [← S.rightHomologyData.op.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i, CategoryTheory.ShortComplex.RightHomologyData.op
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
⊢ S.rightHomologyData.op.i = Quiver.Hom.op S.pOpcycles

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₁ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₂ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := S₁.op.opcycles) (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Iso.hom S₁.opcyclesOpIso) (Iso.inv S₁.opcyclesOpIso) :
          S₁.op.opcycles ⟶ S₁.op.opcycles) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₃ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles) (opcyclesMap (opMap φ) ≫ 𝟙 S₁.op.opcycles) (opcyclesMap (opMap φ))
rw₄ rw₅ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles) (opcyclesMap (opMap φ)) (opcyclesMap (opMap φ))
⊢ Eq (α := Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso) :
      Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ) : Opposite.op S₂.cycles ⟶ S₁.op.opcycles)

Tactic:
rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.opcyclesOpIso, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
simp only [γ.leftHomologyMap'_eq, γ.op.rightHomologyMap'_eq,
    LeftHomologyMapData.op_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.op_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.op, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
dsimp :
  Eq (α := Opposite.op S₂.leftHomology ⟶ Opposite.op S₁.leftHomology)
    (Quiver.Hom.op (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData))
    (CategoryStruct.comp (Y := S₂.op.rightHomology)
      (rightHomologyMap' (𝟙 S₂.op) S₂.leftHomologyData.op S₂.op.rightHomologyData)
      (CategoryStruct.comp (Y := S₁.op.rightHomology)
        (rightHomologyMap' (opMap φ) S₂.op.rightHomologyData S₁.op.rightHomologyData)
        (rightHomologyMap' (𝟙 S₁.op) S₁.op.rightHomologyData S₁.leftHomologyData.op)))
⊢ Eq (α := Opposite.op S₂.leftHomology ⟶ Opposite.op S₁.leftHomology) (Quiver.Hom.op (leftHomologyMap φ))
    (Iso.inv S₂.rightHomologyOpIso ≫ rightHomologyMap (opMap φ) ≫ Iso.hom S₁.rightHomologyOpIso)

Tactic:
dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap,
    leftHomologyMap]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyOpIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := Opposite.op S₂.leftHomology ⟶ Opposite.op S₁.leftHomology)
    (Quiver.Hom.op (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData))
    (CategoryStruct.comp (Y := S₂.op.rightHomology)
      (rightHomologyMap' (𝟙 S₂.op) S₂.leftHomologyData.op S₂.op.rightHomologyData)
      (CategoryStruct.comp (Y := S₁.op.rightHomology)
        (rightHomologyMap' (opMap φ) S₂.op.rightHomologyData S₁.op.rightHomologyData)
        (rightHomologyMap' (𝟙 S₁.op) S₁.op.rightHomologyData S₁.leftHomologyData.op)))

Tactic:
simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.Category.id_comp, CategoryTheory.ShortComplex.leftHomologyMap'_op
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
simp only [γ.rightHomologyMap'_eq, γ.op.leftHomologyMap'_eq,
    RightHomologyMapData.op_φH]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.op_φH, CategoryTheory.ShortComplex.RightHomologyMapData.op, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
dsimp :
  Eq (α := Opposite.op S₂.rightHomology ⟶ Opposite.op S₁.rightHomology)
    (Quiver.Hom.op (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData))
    (CategoryStruct.comp (Y := S₂.op.leftHomology)
      (leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData)
      (CategoryStruct.comp (Y := S₁.op.leftHomology)
        (leftHomologyMap' (opMap φ) S₂.op.leftHomologyData S₁.op.leftHomologyData)
        (leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op)))
⊢ Eq (α := Opposite.op S₂.rightHomology ⟶ Opposite.op S₁.rightHomology) (Quiver.Hom.op (rightHomologyMap φ))
    (Iso.inv S₂.leftHomologyOpIso ≫ leftHomologyMap (opMap φ) ≫ Iso.hom S₁.leftHomologyOpIso)

Tactic:
dsimp [leftHomologyOpIso, LeftHomologyData.leftHomologyIso, leftHomologyMap,
    rightHomologyMap]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.leftHomologyOpIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := Opposite.op S₂.rightHomology ⟶ Opposite.op S₁.rightHomology)
    (Quiver.Hom.op (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData))
    (CategoryStruct.comp (Y := S₂.op.leftHomology)
      (leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData)
      (CategoryStruct.comp (Y := S₁.op.leftHomology)
        (leftHomologyMap' (opMap φ) S₂.op.leftHomologyData S₁.op.leftHomologyData)
        (leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op)))

Tactic:
simp only [← leftHomologyMap'_comp, comp_id, id_comp, rightHomologyMap'_op]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.ShortComplex.rightHomologyMap'_op, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ Epi.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₃) (Y := Opposite.op S₁.X₃) φ.τ₃.op

Tactic:
infer_instance