awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'
have rw : ∀ (hφ : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ))
  (hφφ' : IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))),
  IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')
Tactic: rw [quasiIso_iff] at hφ hφφ' ⊢
Cleared hypotheses: hφ, hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
hφφ' : IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))
⊢ IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')
have hφφ'₁ : IsIso (X := S₁.homology) (Y := S₃.homology) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
Tactic: rw [homologyMap_comp] at hφφ'
Cleared hypotheses: hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ'
have mp : QuasiIso (φ ≫ φ') → QuasiIso φ'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
mp : QuasiIso (φ ≫ φ') → QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ'
have mpr : QuasiIso φ' → QuasiIso (φ ≫ φ')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ
have rw : ∀ (hφ' : IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ'))
  (hφφ' : IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))),
  IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
Tactic: rw [quasiIso_iff] at hφ' hφφ' ⊢
Cleared hypotheses: hφ', hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')
hφφ' : IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have hφφ'₁ : IsIso (X := S₁.homology) (Y := S₃.homology) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
Tactic: rw [homologyMap_comp] at hφφ'
Cleared hypotheses: hφφ'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ
have mp : QuasiIso (φ ≫ φ') → QuasiIso φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
mp : QuasiIso (φ ≫ φ') → QuasiIso φ
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ
have mpr : QuasiIso φ → QuasiIso (φ ≫ φ')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := Arrow.Hom.left e.inv
β : S₂ ⟶ S₄ := Arrow.Hom.right e.hom
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso φ'
have rw : QuasiIso (α ≫ φ ≫ β)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := Arrow.Hom.left e.inv
β : S₂ ⟶ S₄ := Arrow.Hom.right e.hom
⊢ QuasiIso φ'
have suffices : φ' = α ≫ φ ≫ β
Tactic: suffices φ' = α ≫ φ ≫ β by
    rw [this]
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso γ.φH
have rw : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
Tactic: rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
have mp : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) → IsIso γ.φH
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
mp : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) → IsIso γ.φH
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
have mpr : IsIso γ.φH → IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
h : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso γ.φH
have this : IsIso (Y := S₂.homology) (γ.φH ≫ Iso.inv h₂.homologyIso)
Tactic: haveI : IsIso (γ.φH ≫ (LeftHomologyData.homologyIso h₂).inv) :=
      IsIso.of_isIso_comp_left (LeftHomologyData.homologyIso h₁).hom _
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso γ.φH
have rw : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
Tactic: rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
have mp : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) → IsIso γ.φH
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
mp : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) → IsIso γ.φH
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
have mpr : IsIso γ.φH → IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
h : IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso γ.φH
have this : IsIso (Y := S₂.homology) (γ.φH ≫ Iso.inv h₂.homologyIso)
Tactic: haveI : IsIso (γ.φH ≫ (RightHomologyData.homologyIso h₂).inv) :=
      IsIso.of_isIso_comp_left (RightHomologyData.homologyIso h₁).hom _
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)
have rw : IsIso γ.φH ↔ IsIso (leftHomologyMap' φ h₁ h₂)
Tactic: rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
rw : IsIso γ.φH ↔ IsIso (leftHomologyMap' φ h₁ h₂)
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)
have rw₁ : IsIso γ.φH ↔ IsIso γ.φH
Tactic: rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂), QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
have rw : IsIso γ.φH ↔ IsIso (rightHomologyMap' φ h₁ h₂)
Tactic: rw [γ.quasiIso_iff, γ.rightHomologyMap'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
rw : IsIso γ.φH ↔ IsIso (rightHomologyMap' φ h₁ h₂)
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
have rw₁ : IsIso γ.φH ↔ IsIso γ.φH
Tactic: rw [γ.quasiIso_iff, γ.rightHomologyMap'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
⊢ QuasiIso φ
have rw : IsIso (X := S₁.leftHomologyData.H) (Y := (LeftHomologyData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData).H)
  (LeftHomologyMapData.φH (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData))
Tactic: rw [((LeftHomologyMapData.ofEpiOfIsIsoOfMono φ) S₁.leftHomologyData).quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
⊢ IsIso (X := S₁.leftHomologyData.H) (Y := (LeftHomologyData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData).H)
    (LeftHomologyMapData.φH (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData))
have dsimp : IsIso.{v_1, u_1} (𝟙 S₁.leftHomology)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ
have have : ∀ (γ : HomologyMapData φ S₁.homologyData S₂.homologyData), QuasiIso (opMap φ) ↔ QuasiIso φ
Tactic: have γ : HomologyMapData φ S₁.homologyData S₂.homologyData := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ
have rw : IsIso γ.op.right.φH ↔ IsIso γ.left.φH
Tactic: rw [γ.left.quasiIso_iff, γ.op.right.quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
      γ.left.φH.op ↔
    IsIso γ.left.φH
have mp : IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
    γ.left.φH.op →
  IsIso γ.left.φH
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
mp :
  IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
      γ.left.φH.op →
    IsIso γ.left.φH
⊢ IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
      γ.left.φH.op ↔
    IsIso γ.left.φH
have mpr : IsIso γ.left.φH →
  IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
    γ.left.φH.op
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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ᵒᵖ
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₁.unop.HasHomology
inst_5 : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst_6 : QuasiIso φ
⊢ QuasiIso (unopMap φ)
have rw : QuasiIso (opMap (unopMap φ))
Tactic: rw [← quasiIso_opMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw : S₁.g ≫ φ.τ₃ = 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw : S₁.g ≫ φ.τ₃ = 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.f ≫ φ.τ₂ = 0
have rw : φ.τ₁ ≫ S₂.f = 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
⊢ S₁.f ≫ φ.τ₂ = 0
have rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
⊢ S₁.f ≫ φ.τ₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.f ≫ φ.τ₂ = 0
have rw : φ.τ₁ ≫ S₂.f = 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
⊢ S₁.f ≫ φ.τ₂ = 0
have rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.QuasiIso (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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
⊢ S₁.f ≫ φ.τ₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
Tactic: rw [← φ.comm₁₂, hf₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Retract (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : QuasiIso f₂
⊢ QuasiIso f₁
have rw : ∀ (hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)),
  IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)
Tactic: rw [quasiIso_iff] at hf₂ ⊢
Cleared hypotheses: hf₂