awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw :
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂) =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₁ :
  rightHomologyMap' φ h₁ h₂ =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₂ :
  leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ rightHomologyMap' φ h₁ h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₃ :
  leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have rw₄ : Eq (α := S₁.homology ⟶ h₂.H)
  (Iso.hom S₁.leftHomologyData.homologyIso ≫
    leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂)
  (Iso.hom S₁.leftHomologyData.homologyIso ≫
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
Tactic: rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw :
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂) =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₁ :
  rightHomologyMap' φ h₁ h₂ =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₂ :
  leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ rightHomologyMap' φ h₁ h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₃ :
  leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₄ :
  Eq (α := S₁.homology ⟶ h₂.H)
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂)
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
        CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
          (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have rw₅ : Eq (α := S₁.homology ⟶ h₂.H)
  (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ)
    (Iso.hom S₂.leftHomologyData.homologyIso ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂))
  (Iso.hom S₁.leftHomologyData.homologyIso ≫
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
Tactic: rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.homology) S.homologyπ (Iso.inv S.leftHomologyIso) : S.cycles ⟶ S.leftHomology)
    (S.leftHomologyπ : S.cycles ⟶ S.leftHomology)
have dsimp : Eq (α := S.cycles ⟶ S.leftHomology)
  (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) (Iso.inv S.leftHomologyIso) :
    S.cycles ⟶ S.leftHomology)
  (S.leftHomologyπ : S.cycles ⟶ S.leftHomology)
Tactic: dsimp only [homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.rightHomology ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.hom S.rightHomologyIso) S.homologyι : S.rightHomology ⟶ S.opcycles)
    (S.rightHomologyι : S.rightHomology ⟶ S.opcycles)
have dsimp : Eq (α := S.rightHomology ⟶ S.opcycles)
  (CategoryStruct.comp (Y := S.homology) (Iso.hom S.rightHomologyIso) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
    S.rightHomology ⟶ S.opcycles)
  (S.rightHomologyι : S.rightHomology ⟶ S.opcycles)
Tactic: dsimp only [homologyι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.homologyπ) 0
have dsimp : Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0
Tactic: dsimp only [homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ⟶ S.X₃) (S.homologyι ≫ S.fromOpcycles) 0
have dsimp : Eq (α := S.homology ⟶ S.X₃) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.fromOpcycles) 0
Tactic: dsimp only [homologyι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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₁.cycles ⟶ S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)
    (cyclesMap φ ≫ S₂.homologyπ : S₁.cycles ⟶ S₂.homology)
have simp : Eq (α := S₁.cycles ⟶ S₂.leftHomology)
  (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (Iso.inv S₁.leftHomologyIso ≫ leftHomologyMap φ) :
    S₁.cycles ⟶ S₂.leftHomology)
  (cyclesMap φ ≫ S₂.leftHomologyπ : S₁.cycles ⟶ S₂.leftHomology)
Tactic: simp only [← cancel_mono S₂.leftHomologyIso.inv, assoc, ← leftHomologyIso_inv_naturality φ,
    homologyπ_comp_leftHomologyIso_inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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₁.homology ⟶ S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)
    (S₁.homologyι ≫ opcyclesMap φ : S₁.homology ⟶ S₂.opcycles)
have simp : Eq (α := S₁.rightHomology ⟶ S₂.opcycles) (S₁.rightHomologyι ≫ opcyclesMap φ : S₁.rightHomology ⟶ S₂.opcycles)
  (CategoryStruct.comp (Y := S₁.homology) (Iso.hom S₁.rightHomologyIso) (S₁.homologyι ≫ opcyclesMap φ) :
    S₁.rightHomology ⟶ S₂.opcycles)
Tactic: simp only [← cancel_epi S₁.rightHomologyIso.hom, rightHomologyIso_hom_naturality_assoc φ,
    rightHomologyIso_hom_comp_homologyι, rightHomologyι_naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) S.homologyπ S.homologyι : S.cycles ⟶ S.opcycles)
    (S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles)
have dsimp : Eq (α := S.cycles ⟶ S.opcycles)
  (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
      (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
    S.cycles ⟶ S.opcycles)
  (S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles)
Tactic: dsimp only [homologyπ, homologyι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ Eq (α := S.cycles ⟶ h.H) (CategoryStruct.comp (Y := S.homology) S.homologyπ (Iso.hom h.homologyIso) : S.cycles ⟶ h.H)
    (Iso.hom h.cyclesIso ≫ h.π : S.cycles ⟶ h.H)
have dsimp : Eq (α := S.cycles ⟶ h.H)
  (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
      (Iso.hom (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso)) :
    S.cycles ⟶ h.H)
  (Iso.hom h.cyclesIso ≫ h.π : S.cycles ⟶ h.H)
Tactic: dsimp only [homologyπ, homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ Eq (α := h.K ⟶ S.homology) (h.π ≫ Iso.inv h.homologyIso) (Iso.inv h.cyclesIso ≫ S.homologyπ)
have dsimp : Eq (α := h.K ⟶ S.homology) (h.π ≫ Iso.inv (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso))
  (Iso.inv h.cyclesIso ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
Tactic: dsimp only [homologyπ, homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ Eq (α := h.H ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.inv h.homologyIso) S.homologyι : h.H ⟶ S.opcycles)
    (h.ι ≫ Iso.inv h.opcyclesIso : h.H ⟶ S.opcycles)
have dsimp : Eq (α := h.H ⟶ S.opcycles)
  (CategoryStruct.comp (Y := S.homology) (Iso.inv (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso))
      (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
    h.H ⟶ S.opcycles)
  (h.ι ≫ Iso.inv h.opcyclesIso : h.H ⟶ S.opcycles)
Tactic: dsimp only [homologyι, homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ Eq (α := S.homology ⟶ h.Q) (Iso.hom h.homologyIso ≫ h.ι) (S.homologyι ≫ Iso.hom h.opcyclesIso)
have dsimp : Eq (α := S.homology ⟶ h.Q) (Iso.hom (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso) ≫ h.ι)
  ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ Iso.hom h.opcyclesIso)
Tactic: dsimp only [homologyι, homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ Eq (α := S.homology ⟶ S.leftHomology) (Iso.hom h.homologyIso ≫ Iso.inv h.leftHomologyIso) (Iso.inv S.leftHomologyIso)
have dsimp : Eq (α := S.homology ⟶ S.leftHomology)
  (Iso.hom (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso) ≫ Iso.inv h.leftHomologyIso) (Iso.inv S.leftHomologyIso)
Tactic: dsimp only [homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ Eq (α := S.leftHomology ⟶ S.homology) (Iso.hom h.leftHomologyIso ≫ Iso.inv h.homologyIso) (Iso.hom S.leftHomologyIso)
have dsimp : Eq (α := S.leftHomology ⟶ S.homology)
  (Iso.hom h.leftHomologyIso ≫ Iso.inv (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso)) (Iso.hom S.leftHomologyIso)
Tactic: dsimp only [homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ Eq (α := S.homology ⟶ S.rightHomology) (Iso.hom h.homologyIso ≫ Iso.inv h.rightHomologyIso)
    (Iso.inv S.rightHomologyIso)
have dsimp : Eq (α := S.homology ⟶ S.rightHomology)
  (Iso.hom (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso) ≫ Iso.inv h.rightHomologyIso)
  (Iso.inv S.rightHomologyIso)
Tactic: dsimp only [homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ Eq (α := S.rightHomology ⟶ S.homology) (Iso.hom h.rightHomologyIso ≫ Iso.inv h.homologyIso)
    (Iso.hom S.rightHomologyIso)
have dsimp : Eq (α := S.rightHomology ⟶ S.homology)
  (Iso.hom h.rightHomologyIso ≫ Iso.inv (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso))
  (Iso.hom S.rightHomologyIso)
Tactic: dsimp only [homologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso ≫ h₂.ι)) =
    h₁.i ≫ φ.τ₂ ≫ h₂.p
have dsimp : 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: dsimp only [LeftHomologyData.homologyIso, RightHomologyData.homologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyIso, rightHomologyIso,
    leftHomologyMapIso', rightHomologyMapIso',
    LeftHomologyData.cyclesIso, RightHomologyData.opcyclesIso,
    LeftHomologyData.leftHomologyIso, RightHomologyData.rightHomologyIso,
    homologyMap, homologyMap']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ (homologyMap' φ h₁ h₂).op.unop = Quiver.Hom.unop (h₂.iso.inv.op ≫ homologyMap' (opMap φ) h₂.op h₁.op ≫ h₁.iso.hom.op)
have dsimp : homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv
have have : ∀ (γ : HomologyMapData φ h₁ h₂),
  homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ Quiver.Hom.unop (homologyMap' (opMap φ) h₂.op h₁.op)) ≫ h₂.iso.inv
Tactic: have γ : HomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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) (Quiver.Hom.op (homologyMap φ))
    (Iso.inv S₂.homologyOpIso ≫ homologyMap (opMap φ) ≫ Iso.hom S₁.homologyOpIso)
have 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)))))
Tactic: dsimp only [homologyMap, homologyOpIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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)
    (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)))))
have 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)))))
Tactic: rw [homologyMap'_op]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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 ≫
      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)))))
have 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))))))
Tactic: dsimp only [Iso.symm, Iso.trans, Iso.op, Iso.refl, rightHomologyIso, leftHomologyIso,
    leftHomologyOpIso, leftHomologyMapIso', rightHomologyMapIso',
    LeftHomologyData.leftHomologyIso, homologyMap']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ k ≫ S.g = 0
have rw : (x ≫ S.f) ≫ S.g = 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ k ≫ S.g = 0
have rw₁ : x ≫ S.f ≫ S.g = 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ k ≫ S.g = 0
have rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ k ≫ S.g = 0
have rw₃ : Eq.{v + 1} (α := A ⟶ S.X₃) 0 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
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
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles k ⋯ ≫ S.homologyπ) 0
have dsimp : Eq (α := A ⟶ S.homology) (S.liftCycles k sorry ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0
Tactic: dsimp only [homologyπ]