awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
rw :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (cyclesMap (opMap φ) ≫ Iso.hom S₁.cyclesOpIso)
        (Iso.inv S₁.cyclesOpIso) :
      S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso) (Quiver.Hom.op (opcyclesMap φ)))
        (Iso.inv S₁.cyclesOpIso) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₁ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Iso.hom S₁.cyclesOpIso) (Iso.inv S₁.cyclesOpIso) :
          S₁.op.cycles ⟶ S₁.op.cycles) :
      S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso) (Quiver.Hom.op (opcyclesMap φ)))
        (Iso.inv S₁.cyclesOpIso) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₂ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Iso.hom S₁.cyclesOpIso) (Iso.inv S₁.cyclesOpIso) :
          S₁.op.cycles ⟶ S₁.op.cycles) :
      S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso)) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₃ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles) (cyclesMap (opMap φ) ≫ 𝟙 S₁.op.cycles : S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso)) :
      S₂.op.cycles ⟶ S₁.op.cycles)
⊢ Eq (α := S₂.op.cycles ⟶ Opposite.op S₁.opcycles)
    (cyclesMap (opMap φ) ≫ Iso.hom S₁.cyclesOpIso : S₂.op.cycles ⟶ Opposite.op S₁.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso) (Quiver.Hom.op (opcyclesMap φ)) :
      S₂.op.cycles ⟶ Opposite.op S₁.opcycles)
have rw₄ : Eq (α := S₂.op.cycles ⟶ S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
  (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
      (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso)) :
    S₂.op.cycles ⟶ S₁.op.cycles)
Tactic: rw [← cancel_mono (S₁.cyclesOpIso).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    cyclesOpIso_inv_naturality, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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 φ))
    (Iso.inv S₂.rightHomologyOpIso ≫ rightHomologyMap (opMap φ) ≫ Iso.hom S₁.rightHomologyOpIso)
have 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)))
Tactic: dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap,
    leftHomologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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 φ))
    (Iso.inv S₂.leftHomologyOpIso ≫ leftHomologyMap (opMap φ) ≫ Iso.hom S₁.leftHomologyOpIso)
have 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)))
Tactic: dsimp [leftHomologyOpIso, LeftHomologyData.leftHomologyIso, leftHomologyMap,
    rightHomologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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 φ.τ₃
⊢ S₂.RightHomologyData
have this : Epi (opMap φ).τ₁
Tactic: haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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 φ.τ₃
this : Epi (opMap φ).τ₁
⊢ S₂.RightHomologyData
have this₁ : IsIso (opMap φ).τ₂
Tactic: haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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 φ.τ₃
this_1 : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ S₂.RightHomologyData
have this₁ : Mono (opMap φ).τ₃
Tactic: haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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 φ.τ₃
⊢ S₁.RightHomologyData
have this : Epi (opMap φ).τ₁
Tactic: haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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 φ.τ₃
this : Epi (opMap φ).τ₁
⊢ S₁.RightHomologyData
have this₁ : IsIso (opMap φ).τ₂
Tactic: haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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 φ.τ₃
this_1 : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ S₁.RightHomologyData
have this₁ : Mono (opMap φ).τ₃
Tactic: haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
have rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
Tactic: rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
have rw₁ : S₁.g ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
Tactic: rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₁ : S₁.g ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
have rw₂ : S₁.g ≫ φ.τ₃ = (φ.τ₂ ≫ h.p) ≫ h.g'
Tactic: rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₁ : S₁.g ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₂ : S₁.g ≫ φ.τ₃ = (φ.τ₂ ≫ h.p) ≫ h.g'
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
have rw₃ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ h.p ≫ h.g'
Tactic: rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₁ : S₁.g ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₂ : S₁.g ≫ φ.τ₃ = (φ.τ₂ ≫ h.p) ≫ h.g'
rw₃ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ h.p ≫ h.g'
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
have rw₄ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ S₂.g
Tactic: rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₁ : S₁.g ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₂ : S₁.g ≫ φ.τ₃ = (φ.τ₂ ≫ h.p) ≫ h.g'
rw₃ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ h.p ≫ h.g'
rw₄ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ S₂.g
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
have rw₅ : S₁.g ≫ φ.τ₃ = S₁.g ≫ φ.τ₃
Tactic: rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (rightHomologyMap' φ h₁ h₂')
have rw : IsIso (Y := h₂'.H) (RightHomologyMapData.φH (RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁))
Tactic: rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (Y := h₂'.H) (RightHomologyMapData.φH (RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁))
have dsimp : IsIso.{v_1, u_1} (𝟙 h₁.H)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
have this : IsIso (rightHomologyMap' φ h₁ h₂')
Tactic: haveI : IsIso (rightHomologyMap' φ h₁ h₂') := by
    rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
    dsimp
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
have eq : rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
Tactic: have eq := rightHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
have eq₁ : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
Tactic: rw [comp_id] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
have rw : IsIso (rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ S.f ≫ k ≫ α = 0
have rw : Eq (α := S.X₁ ⟶ A') (0 ≫ α) 0
Tactic: rw [reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
A' : C
α : A ⟶ A'
rw : Eq (α := S.X₁ ⟶ A') (0 ≫ α) 0
⊢ S.f ≫ k ≫ α = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁ ⟶ A') 0 0
Tactic: rw [reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0
have rw : S.f ≫ S.g ≫ x = 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
⊢ S.f ≫ k = 0
have rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
⊢ S.f ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ A) 0 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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.g = S.g ≫ 𝟙 S.X₃
have rw : S.g = S.g
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
φ : S₁ ⟶ S
inst_3 : S₁.HasRightHomology
⊢ S₁.f ≫ φ.τ₂ ≫ k = 0
have rw : φ.τ₁ ≫ S.f ≫ k = 0
Tactic: rw [← φ.comm₁₂_assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
φ : S₁ ⟶ S
inst_3 : S₁.HasRightHomology
rw : φ.τ₁ ≫ S.f ≫ k = 0
⊢ S₁.f ≫ φ.τ₂ ≫ k = 0
have rw₁ : Eq (α := S₁.X₁ ⟶ A) (φ.τ₁ ≫ 0) 0
Tactic: rw [← φ.comm₁₂_assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
φ : S₁ ⟶ S
inst_3 : S₁.HasRightHomology
rw : φ.τ₁ ≫ S.f ≫ k = 0
rw₁ : Eq (α := S₁.X₁ ⟶ A) (φ.τ₁ ≫ 0) 0
⊢ S₁.f ≫ φ.τ₂ ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ A) 0 0
Tactic: rw [← φ.comm₁₂_assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
⊢ Eq (α := S.opcycles ⟶ A) (Iso.hom h.opcyclesIso ≫ h.descQ k hk) (S.descOpcycles k hk)
have rw : Eq (α := S.opcycles ⟶ A)
  (Iso.hom h.opcyclesIso ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.inv h.opcyclesIso) (S.descOpcycles k hk))
  (S.descOpcycles k hk)
Tactic: rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
rw :
  Eq (α := S.opcycles ⟶ A)
    (Iso.hom h.opcyclesIso ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.inv h.opcyclesIso) (S.descOpcycles k hk))
    (S.descOpcycles k hk)
⊢ Eq (α := S.opcycles ⟶ A) (Iso.hom h.opcyclesIso ≫ h.descQ k hk) (S.descOpcycles k hk)
have rw₁ : Eq (α := S.opcycles ⟶ A) (S.descOpcycles k hk) (S.descOpcycles k hk)
Tactic: rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
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
inst_3 : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
⊢ HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
have this : HasLimit (parallelPair h.g' 0)
Tactic: haveI : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ IsIso (opcyclesMap' φ h₁ h₂)
have refine_1 : S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0
Tactic: refine ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
refine_1 : S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0
⊢ IsIso (opcyclesMap' φ h₁ h₂)
have refine_2 : opcyclesMap' φ h₁ h₂ ≫ h₂.descQ (inv φ.τ₂ ≫ h₁.p) sorry = 𝟙 h₁.Q
Tactic: refine ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
refine_1 : S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0
refine_2 : opcyclesMap' φ h₁ h₂ ≫ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ = 𝟙 h₁.Q
⊢ IsIso (opcyclesMap' φ h₁ h₂)
have refine_3 : h₂.descQ (inv φ.τ₂ ≫ h₁.p) sorry ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q
Tactic: refine ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Mono S₂.f
have suffices : Mono (S₂.f ≫ e.inv.τ₂)
Tactic: suffices Mono (S₂.f ≫ e.inv.τ₂) by
      exact mono_of_mono _ e.inv.τ₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Mono (S₂.f ≫ e.inv.τ₂)
have this : Mono S₁.f
Tactic: have := h.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Mono S₁.f
⊢ Mono (S₂.f ≫ e.inv.τ₂)
have rw : Mono (e.inv.τ₁ ≫ S₁.f)
Tactic: rw [← e.inv.comm₁₂]