awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
hφ' : QuasiIsoAt φ' i
rw :
  ∀
    (hφ :
      ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (hφ' :
      ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) L)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')),
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ φ'))
⊢ QuasiIsoAt (φ ≫ φ') i

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

Premises used: quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
hφ' :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) L)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')
rw :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
      CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ φ'))

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
hφ' :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) L)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
      CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')

Tactic:
ShortComplex.quasiIso_comp _ _

Premises used: CategoryTheory.ShortComplex.quasiIso_comp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
hφ' :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) L)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
      CategoryTheory.Functor.map (shortComplexFunctor C c i) φ')

Tactic:
exact ShortComplex.quasiIso_comp _ _

Premises used: CategoryTheory.ShortComplex.quasiIso_comp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
hφφ' : QuasiIsoAt (φ ≫ φ') i
rw :
  ∀ (hφ : IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i))
    (hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)),
    IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
⊢ QuasiIsoAt φ' i

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

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)
⊢ IsIso (X := K.homology i) (Y := M.homology i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))

Tactic:
rw [homologyMap_comp] at hφφ'

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
hφφ' :
  IsIso (X := K.homology i) (Y := M.homology i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))
⊢ IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)

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

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
hφφ' :
  IsIso (X := K.homology i) (Y := M.homology i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))
⊢ IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)

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

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
mp : QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i
mpr : QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
h : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i

Tactic:
quasiIsoAt_of_comp_left φ φ' i

Premises used: quasiIsoAt_of_comp_left
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
h : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i

Tactic:
exact quasiIsoAt_of_comp_left φ φ' i

Premises used: quasiIsoAt_of_comp_left
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ : QuasiIsoAt φ i
h : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ'

Tactic:
simp only [quasiIso_iff, quasiIsoAt_iff_comp_left φ φ']

Premises used: quasiIso_iff, quasiIsoAt_iff_comp_left
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' rw : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Tactic:
rw [← quasiIso_iff_comp_left φ φ']

Premises used: quasiIso_iff_comp_left
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
hφφ' : QuasiIsoAt (φ ≫ φ') i
rw :
  ∀ (hφ' : IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i))
    (hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)),
    IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)
⊢ QuasiIsoAt φ i

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

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
hφφ' : IsIso (X := K.homology i) (Y := M.homology i) (homologyMap (φ ≫ φ') i)
⊢ IsIso (X := K.homology i) (Y := M.homology i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))

Tactic:
rw [homologyMap_comp] at hφφ'

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
hφφ' :
  IsIso (X := K.homology i) (Y := M.homology i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))
⊢ IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)

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

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : IsIso (X := L.homology i) (Y := M.homology i) (homologyMap φ' i)
hφφ' :
  IsIso (X := K.homology i) (Y := M.homology i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap φ' i))
⊢ IsIso (X := K.homology i) (Y := L.homology i) (homologyMap φ i)

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

Premises used: CategoryTheory.IsIso.of_isIso_comp_right, HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
mp : QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ i
mpr : QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
h : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ i

Tactic:
quasiIsoAt_of_comp_right φ φ' i

Premises used: quasiIsoAt_of_comp_right
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
h : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ i

Tactic:
exact quasiIsoAt_of_comp_right φ φ' i

Premises used: quasiIsoAt_of_comp_right
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
hφ' : QuasiIsoAt φ' i
h : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), M.HasHomology i
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_iff_comp_right φ φ']

Premises used: quasiIsoAt_iff_comp_right, quasiIso_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' rw : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
rw [← quasiIso_iff_comp_right φ φ']

Premises used: quasiIso_iff_comp_right
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : K' ⟶ L'
e : Arrow.mk φ ≅ Arrow.mk φ'
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), K'.HasHomology i
inst_5 : ∀ (i : ι), L'.HasHomology i
⊢ QuasiIso φ ↔ QuasiIso φ'

Tactic:
simp [← quasiIso_iff_comp_left (show K' ⟶ K from e.inv.left) φ,
    ← quasiIso_iff_comp_right φ' (show L' ⟶ L from e.inv.right)]

Premises used: CategoryTheory.Arrow.Hom.right, quasiIso_iff_comp_left, CategoryTheory.Arrow.Hom.left, quasiIso_iff_comp_right, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L K' L' : HomologicalComplex.{v, u, u_1} C c
φ : K ⟶ L
φ' : K' ⟶ L'
e : Arrow.mk φ ≅ Arrow.mk φ'
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : ∀ (i : ι), K'.HasHomology i
inst_5 : ∀ (i : ι), L'.HasHomology i
hφ : QuasiIso φ
⊢ QuasiIso φ'

Tactic:
simpa only [← quasiIso_iff_of_arrow_mk_iso φ φ' e]

Premises used: quasiIso_iff_of_arrow_mk_iso
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K_1 L_1 M K' L' : HomologicalComplex.{v, u, u_1} C c
C₁ : Type u_2
C₂ : Type u_3
inst_2 : Category.{v_1, u_2} C₁
inst_3 : Category.{v_2, u_3} C₂
inst_4 : Preadditive.{v_1, u_2} C₁
inst_5 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_6 : F.Additive
inst_7 : F.PreservesHomology
i : ι
inst_8 : K.HasHomology i
inst_9 : L.HasHomology i
inst_10 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_11 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
hφ : QuasiIsoAt φ i
rw :
  ∀
    (hφ :
      ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
        (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)),
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
      (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i)
        (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ))
⊢ QuasiIsoAt (K := Functor.obj (F.mapHomologicalComplex c) K) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)
    i

Tactic:
rw [quasiIsoAt_iff] at hφ ⊢

Premises used: quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K_1 L_1 M K' L' : HomologicalComplex.{v, u, u_1} C c
C₁ : Type u_2
C₂ : Type u_3
inst_2 : Category.{v_1, u_2} C₁
inst_3 : Category.{v_2, u_3} C₂
inst_4 : Preadditive.{v_1, u_2} C₁
inst_5 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_6 : F.Additive
inst_7 : F.PreservesHomology
i : ι
inst_8 : K.HasHomology i
inst_9 : L.HasHomology i
inst_10 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_11 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
hφ :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
    (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ))

Tactic:
ShortComplex.quasiIso_map_of_preservesLeftHomology F
    ((shortComplexFunctor C₁ c i).map φ)

Premises used: CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.map
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K_1 L_1 M K' L' : HomologicalComplex.{v, u, u_1} C c
C₁ : Type u_2
C₂ : Type u_3
inst_2 : Category.{v_1, u_2} C₁
inst_3 : Category.{v_2, u_3} C₂
inst_4 : Preadditive.{v_1, u_2} C₁
inst_5 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_6 : F.Additive
inst_7 : F.PreservesHomology
i : ι
inst_8 : K.HasHomology i
inst_9 : L.HasHomology i
inst_10 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_11 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
hφ :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
    (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ))

Tactic:
exact ShortComplex.quasiIso_map_of_preservesLeftHomology F
    ((shortComplexFunctor C₁ c i).map φ)

Premises used: CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst : Category.{v_1, u_2} C₁
inst_1 : Category.{v_2, u_3} C₂
inst_2 : Preadditive.{v_1, u_2} C₁
inst_3 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_4 : F.Additive
inst_5 : F.PreservesHomology
i : ι
inst_6 : K.HasHomology i
inst_7 : L.HasHomology i
inst_8 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_9 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
inst_10 : F.ReflectsIsomorphisms
simp :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
      (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i)
        (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)
⊢ QuasiIsoAt (K := Functor.obj (F.mapHomologicalComplex c) K) (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)
      i ↔
    QuasiIsoAt φ i

Tactic:
simp only [quasiIsoAt_iff]

Premises used: quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst : Category.{v_1, u_2} C₁
inst_1 : Category.{v_2, u_3} C₂
inst_2 : Preadditive.{v_1, u_2} C₁
inst_3 : Preadditive.{v_2, u_3} C₂
K L : HomologicalComplex.{v_1, u_2, u_1} C₁ c
φ : K ⟶ L
F : CategoryTheory.Functor.{v_1, v_2, u_2, u_3} C₁ C₂
inst_4 : F.Additive
inst_5 : F.PreservesHomology
i : ι
inst_6 : K.HasHomology i
inst_7 : L.HasHomology i
inst_8 : HasHomology (Functor.obj (F.mapHomologicalComplex c) K) i
inst_9 : HasHomology (Functor.obj (F.mapHomologicalComplex c) L) i
inst_10 : F.ReflectsIsomorphisms
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₂ c i) (Functor.obj (F.mapHomologicalComplex c) K))
      (CategoryTheory.Functor.map (shortComplexFunctor C₂ c i)
        (CategoryTheory.Functor.map (F.mapHomologicalComplex c) φ)) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C₁ c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C₁ c i) φ)

Tactic:
ShortComplex.quasiIso_map_iff_of_preservesLeftHomology F
    ((shortComplexFunctor C₁ c i).map φ)

Premises used: HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology, CategoryTheory.ShortComplex.map