awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
⊢ QuasiIso φ

Tactic:
⟨h⟩

Premises used: CategoryTheory.ShortComplex.QuasiIso.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
⊢ QuasiIso φ

Tactic:
exact ⟨h⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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₂
inst_6 : IsIso φ
⊢ QuasiIso φ

Tactic:
⟨(homologyMapIso (asIso φ)).isIso_hom⟩

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.ShortComplex.QuasiIso.mk, CategoryTheory.asIso, CategoryTheory.ShortComplex.homologyMapIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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₃
hφ : QuasiIso φ
hφ' : QuasiIso φ'
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 (φ ≫ φ'))
⊢ QuasiIso (φ ≫ φ')

Tactic:
rw [quasiIso_iff] at hφ hφ' ⊢

Premises used: CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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₃
hφ : IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
hφ' : IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')
rw :
  IsIso (X := S₁.homology) (Y := S₃.homology) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
⊢ IsIso (X := S₁.homology) (Y := S₃.homology) (homologyMap (φ ≫ φ'))

Tactic:
rw [homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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₃
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (φ ≫ φ')
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 φ')
⊢ QuasiIso φ'

Tactic:
rw [quasiIso_iff] at hφ hφφ' ⊢

Premises used: CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))

Tactic:
rw [homologyMap_comp] at hφφ'

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
⊢ IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')

Tactic:
IsIso.of_isIso_comp_left (homologyMap φ) (homologyMap φ')

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
⊢ IsIso (X := S₂.homology) (Y := S₃.homology) (homologyMap φ')

Tactic:
exact IsIso.of_isIso_comp_left (homologyMap φ) (homologyMap φ')

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ'
mpr : QuasiIso φ' → QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ'

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ'

Tactic:
quasiIso_of_comp_left φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_of_comp_left
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ'

Tactic:
exact quasiIso_of_comp_left φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_of_comp_left
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (φ ≫ φ')

Tactic:
quasiIso_comp φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (φ ≫ φ')

Tactic:
exact quasiIso_comp φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (φ ≫ φ')
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 φ)
⊢ QuasiIso φ

Tactic:
rw [quasiIso_iff] at hφ' hφφ' ⊢

Premises used: CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))

Tactic:
rw [homologyMap_comp] at hφφ'

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
IsIso.of_isIso_comp_right (homologyMap φ) (homologyMap φ')

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (homologyMap φ'))
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
exact IsIso.of_isIso_comp_right (homologyMap φ) (homologyMap φ')

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ
mpr : QuasiIso φ → QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ

Tactic:
quasiIso_of_comp_right φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_of_comp_right
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ

Tactic:
exact quasiIso_of_comp_right φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_of_comp_right
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (φ ≫ φ')

Tactic:
quasiIso_comp φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (φ ≫ φ')

Tactic:
exact quasiIso_comp φ φ'

Premises used: CategoryTheory.ShortComplex.quasiIso_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 : φ' = α ≫ φ ≫ β
rw : QuasiIso (α ≫ φ ≫ β)
⊢ QuasiIso φ'

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (α ≫ φ ≫ β)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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
suffices : φ' = α ≫ φ ≫ β
⊢ QuasiIso φ'

Tactic:
suffices φ' = α ≫ φ ≫ β by
    rw [this]
    infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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
⊢ φ' = α ≫ φ ≫ β

Tactic:
simp only [α, β, Arrow.w_mk_right_assoc, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom,
    ← Arrow.comp_right, e.inv_hom_id, Arrow.id_right, comp_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Arrow.w_mk_right_assoc, CategoryTheory.Arrow.mk_right, CategoryTheory.Category.comp_id, CategoryTheory.Arrow.mk_hom, CategoryTheory.Arrow.id_right, CategoryTheory.Arrow.mk_left, CategoryTheory.Arrow.comp_right
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 φ'
⊢ QuasiIso φ ↔ QuasiIso φ'

Tactic:
⟨fun _ => quasiIso_of_arrow_mk_iso φ φ' e, fun _ => quasiIso_of_arrow_mk_iso φ' φ e.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.quasiIso_of_arrow_mk_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
⊢ QuasiIso φ ↔ IsIso γ.φH

Tactic:
rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq, CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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
mpr : IsIso γ.φH → IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (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 _
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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)
this : IsIso (Y := S₂.homology) (γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso γ.φH

Tactic:
IsIso.of_isIso_comp_right _ (LeftHomologyData.homologyIso h₂).inv

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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)
this : IsIso (Y := S₂.homology) (γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso γ.φH

Tactic:
exact IsIso.of_isIso_comp_right _ (LeftHomologyData.homologyIso h₂).inv

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 γ.φH
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH
⊢ QuasiIso φ ↔ IsIso γ.φH

Tactic:
rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq, CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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
mpr : IsIso γ.φH → IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso) ↔ IsIso γ.φH

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 (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 _
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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)
this : IsIso (Y := S₂.homology) (γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso γ.φH

Tactic:
IsIso.of_isIso_comp_right _ (RightHomologyData.homologyIso h₂).inv

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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)
this : IsIso (Y := S₂.homology) (γ.φH ≫ Iso.inv h₂.homologyIso)
⊢ IsIso γ.φH

Tactic:
exact IsIso.of_isIso_comp_right _ (RightHomologyData.homologyIso h₂).inv

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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 γ.φH
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
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
have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default