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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
mp :
  QuasiIsoAt f i →
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
mpr :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f) →
    QuasiIsoAt f i
⊢ QuasiIsoAt f i ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)

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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
h : QuasiIsoAt f i
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)

Tactic:
h.quasiIso

Premises used: QuasiIsoAt.quasiIso
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
h : QuasiIsoAt f i
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)

Tactic:
exact h.quasiIso

Premises used: QuasiIsoAt.quasiIso
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
h :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
⊢ QuasiIsoAt f i

Tactic:
⟨h⟩

Premises used: QuasiIsoAt.mk
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
h :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
⊢ QuasiIsoAt f i

Tactic:
exact ⟨h⟩
-- 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
f : K ⟶ L
inst_2 : IsIso f
i : ι
inst_3 : K.HasHomology i
inst_4 : L.HasHomology i
rw :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff]

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
f : K ⟶ L
inst_2 : IsIso f
i : ι
inst_3 : K.HasHomology i
inst_4 : L.HasHomology i
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)

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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : L.HasHomology j
inst_4 : (K.sc' i j k).HasHomology
inst_5 : (L.sc' i j k).HasHomology
rw :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c j) f) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C c i j k) K)
      (CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) f)
⊢ QuasiIsoAt f j ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C c i j k) K)
      (CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) f)

Tactic:
rw [quasiIsoAt_iff]

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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : L.HasHomology j
inst_4 : (K.sc' i j k).HasHomology
inst_5 : (L.sc' i j k).HasHomology
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c j) f) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C c i j k) K)
      (CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) f)

Tactic:
ShortComplex.quasiIso_iff_of_arrow_mk_iso _ _
    (Arrow.isoOfNatIso (natIsoSc' C c i j k hi hk) (Arrow.mk f))

Premises used: HomologicalComplex.natIsoSc', CategoryTheory.Arrow.isoOfNatIso, CategoryTheory.Arrow.mk, CategoryTheory.ShortComplex.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 L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : L.HasHomology j
inst_4 : (K.sc' i j k).HasHomology
inst_5 : (L.sc' i j k).HasHomology
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c j) f) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C c i j k) K)
      (CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) f)

Tactic:
exact ShortComplex.quasiIso_iff_of_arrow_mk_iso _ _
    (Arrow.isoOfNatIso (natIsoSc' C c i j k hi hk) (Arrow.mk f))
-- 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
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : K'.HasHomology i
inst_5 : L'.HasHomology i
hf' : QuasiIsoAt f' i
rw :
  ∀
    (hf' :
      ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K')
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) f')),
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff] at hf' ⊢

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 K' L' : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : K'.HasHomology i
inst_5 : L'.HasHomology i
hf' :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K')
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f')
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)

Tactic:
ShortComplex.quasiIso_of_retract (h.map (shortComplexFunctor C c i))

Premises used: CategoryTheory.ShortComplex.quasiIso_of_retract, CategoryTheory.RetractArrow.map, HomologicalComplex.shortComplexFunctor
-- 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
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : K'.HasHomology i
inst_5 : L'.HasHomology i
hf' :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K')
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f')
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)

Tactic:
exact ShortComplex.quasiIso_of_retract (h.map (shortComplexFunctor C c i))

Premises used: CategoryTheory.ShortComplex.quasiIso_of_retract, CategoryTheory.RetractArrow.map, HomologicalComplex.shortComplexFunctor
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
rw :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsIso (X := K.homology i) (Y := L.homology i) (homologyMap f i)
⊢ QuasiIsoAt f i ↔ IsIso (X := K.homology i) (Y := L.homology i) (homologyMap f i)

Tactic:
rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]

Premises used: CategoryTheory.ShortComplex.quasiIso_iff, 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsIso (X := K.homology i) (Y := L.homology i) (homologyMap f i)

Tactic:
rfl
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : K.ExactAt i
simp :
  ∀ (hK : IsZero.{v, u} (K.sc i).homology),
    IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
        (Functor.obj (shortComplexFunctor C c i) L).homology)
        (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
      IsZero.{v, u} (L.sc i).homology
⊢ QuasiIsoAt f i ↔ L.ExactAt i

Tactic:
simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff,
    ShortComplex.exact_iff_isZero_homology] at hK ⊢

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology, HomologicalComplex.exactAt_iff, CategoryTheory.ShortComplex.quasiIso_iff, 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
mp :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) →
    IsZero.{v, u} (L.sc i).homology
mpr :
  IsZero.{v, u} (L.sc i).homology →
    IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (L.sc i).homology

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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
h :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
⊢ IsZero.{v, u} (L.sc i).homology

Tactic:
IsZero.of_iso hK (@asIso _ _ _ _ _ h).symm

Premises used: CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
h :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
⊢ IsZero.{v, u} (L.sc i).homology

Tactic:
exact IsZero.of_iso hK (@asIso _ _ _ _ _ h).symm

Premises used: CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
hL : IsZero.{v, u} (L.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))

Tactic:
⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, And.intro, CategoryTheory.Limits.IsZero.eq_of_tgt, Exists.intro, OfNat.ofNat, CategoryTheory.IsIso.mk
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
hL : IsZero.{v, u} (L.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))

Tactic:
exact ⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : L.ExactAt i
simp :
  ∀ (hL : IsZero.{v, u} (L.sc i).homology),
    IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
        (Functor.obj (shortComplexFunctor C c i) L).homology)
        (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
      IsZero.{v, u} (K.sc i).homology
⊢ QuasiIsoAt f i ↔ K.ExactAt i

Tactic:
simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff,
    ShortComplex.exact_iff_isZero_homology] at hL ⊢

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology, HomologicalComplex.exactAt_iff, CategoryTheory.ShortComplex.quasiIso_iff, 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
mp :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) →
    IsZero.{v, u} (K.sc i).homology
mpr :
  IsZero.{v, u} (K.sc i).homology →
    IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (K.sc i).homology

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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
h :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
⊢ IsZero.{v, u} (K.sc i).homology

Tactic:
IsZero.of_iso hL (@asIso _ _ _ _ _ h)

Premises used: CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.asIso
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
h :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
⊢ IsZero.{v, u} (K.sc i).homology

Tactic:
exact IsZero.of_iso hL (@asIso _ _ _ _ _ h)

Premises used: CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.asIso
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
hK : IsZero.{v, u} (K.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))

Tactic:
⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, And.intro, CategoryTheory.Limits.IsZero.eq_of_tgt, Exists.intro, OfNat.ofNat, CategoryTheory.IsIso.mk
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hL : IsZero.{v, u} (L.sc i).homology
hK : IsZero.{v, u} (K.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))

Tactic:
exact ⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : QuasiIsoAt f i
⊢ K.ExactAt i ↔ L.ExactAt i

Tactic:
⟨fun hK => (quasiIsoAt_iff_exactAt f i hK).1 inferInstance,
    fun hL => (quasiIsoAt_iff_exactAt' f i hL).1 inferInstance⟩

Premises used: quasiIsoAt_iff_exactAt, inferInstance, Iff.intro, Iff.mp, quasiIsoAt_iff_exactAt'
-- 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
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hf : QuasiIsoAt f i
⊢ IsIso (X := K.homology i) (Y := L.homology i) (homologyMap f i)

Tactic:
simpa only [quasiIsoAt_iff, ShortComplex.quasiIso_iff] using hf

Premises used: CategoryTheory.ShortComplex.quasiIso_iff, 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : QuasiIsoAt f i
⊢ CategoryStruct.comp (Y := L.homology i) (homologyMap f i) (Iso.inv (isoOfQuasiIsoAt f i)) = 𝟙 (K.homology i)

Tactic:
(isoOfQuasiIsoAt f i).hom_inv_id

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.Iso.hom_inv_id, isoOfQuasiIsoAt, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.ShortComplex.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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : QuasiIsoAt f i
⊢ CategoryStruct.comp (Y := K.homology i) (Iso.inv (isoOfQuasiIsoAt f i)) (homologyMap f i) = 𝟙 (L.homology i)

Tactic:
(isoOfQuasiIsoAt f i).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.leftHomologyMap', isoOfQuasiIsoAt, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K L : CochainComplex.{v, u, 0} C ℕ
f : K ⟶ L
inst_2 : HasHomology K 0
inst_3 : HasHomology L 0
inst_4 : (sc' K 0 0 1).HasHomology
inst_5 : (sc' L 0 0 1).HasHomology
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K L : CochainComplex.{v, u, 0} C ℕ
f : K ⟶ L
inst_2 : HasHomology K 0
inst_3 : HasHomology L 0
inst_4 : (sc' K 0 0 1).HasHomology
inst_5 : (sc' L 0 0 1).HasHomology
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K L : ChainComplex.{v, u, 0} C ℕ
f : K ⟶ L
inst_2 : HasHomology K 0
inst_3 : HasHomology L 0
inst_4 : (sc' K 1 0 0).HasHomology
inst_5 : (sc' L 1 0 0).HasHomology
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.QuasiIso
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K L : ChainComplex.{v, u, 0} C ℕ
f : K ⟶ L
inst_2 : HasHomology K 0
inst_3 : HasHomology L 0
inst_4 : (sc' K 1 0 0).HasHomology
inst_5 : (sc' L 1 0 0).HasHomology
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp
-- 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 : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
⊢ QuasiIso f ↔ ∀ (i : ι), QuasiIsoAt f i

Tactic:
⟨fun h => h.quasiIsoAt, fun h => ⟨h⟩⟩

Premises used: QuasiIso.quasiIsoAt, QuasiIso.mk, Iff.intro