awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
inst_3 : HomologicalComplex.HasHomology L 0
⊢ Eq (α := HomologicalComplex.homology K 0 ⟶ HomologicalComplex.cycles L 0)
    (HomologicalComplex.homologyMap φ 0 ≫ Iso.inv L.isoHomologyπ₀)
    (Iso.inv K.isoHomologyπ₀ ≫ HomologicalComplex.cyclesMap φ 0)

Tactic:
simp only [← cancel_epi (K.homologyπ 0), HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.isoHomologyπ_hom_inv_id, comp_id,
    HomologicalComplex.isoHomologyπ_hom_inv_id_assoc]

Premises used: HomologicalComplex.homologyπ, HomologicalComplex.homologyπ_naturality_assoc, CategoryTheory.Category.comp_id, HomologicalComplex.isoHomologyπ_hom_inv_id, OfNat.ofNat, CategoryTheory.cancel_epi, HomologicalComplex.isoHomologyπ_hom_inv_id_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
dsimp :
  Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
    (-ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
⊢ Eq (α := K.homology i ⟶ L.homology i) (homologyMap (-φ) i) (-homologyMap φ i)

Tactic:
dsimp [homologyMap]

Premises used: HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
rw :
  Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
    (ShortComplex.homologyMap (-CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
⊢ Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
    (-ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))

Tactic:
rw [← ShortComplex.homologyMap_neg]

Premises used: CategoryTheory.ShortComplex.homologyMap_neg
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
    (ShortComplex.homologyMap (-CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
dsimp :
  ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)) =
    HAdd.hAdd (α := K.homology i ⟶ L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
⊢ homologyMap (φ + ψ) i = HAdd.hAdd (α := K.homology i ⟶ L.homology i) (homologyMap φ i) (homologyMap ψ i)

Tactic:
dsimp [homologyMap]

Premises used: HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
rw :
  Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)))
    (ShortComplex.homologyMap
      (HAdd.hAdd (α := Functor.obj (shortComplexFunctor C c i) K ⟶ Functor.obj (shortComplexFunctor C c i) L)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)) =
    HAdd.hAdd (α := K.homology i ⟶ L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))

Tactic:
rw [← ShortComplex.homologyMap_add]

Premises used: CategoryTheory.ShortComplex.homologyMap_add
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)))
    (ShortComplex.homologyMap
      (HAdd.hAdd (α := Functor.obj (shortComplexFunctor C c i) K ⟶ Functor.obj (shortComplexFunctor C c i) L)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
dsimp :
  ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)) =
    HSub.hSub (α := K.homology i ⟶ L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
⊢ homologyMap (φ - ψ) i = HSub.hSub (α := K.homology i ⟶ L.homology i) (homologyMap φ i) (homologyMap ψ i)

Tactic:
dsimp [homologyMap]

Premises used: HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
rw :
  Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)))
    (ShortComplex.homologyMap
      (HSub.hSub (α := Functor.obj (shortComplexFunctor C c i) K ⟶ Functor.obj (shortComplexFunctor C c i) L)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)) =
    HSub.hSub (α := K.homology i ⟶ L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))

Tactic:
rw [← ShortComplex.homologyMap_sub]

Premises used: CategoryTheory.ShortComplex.homologyMap_sub
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)))
    (ShortComplex.homologyMap
      (HSub.hSub (α := Functor.obj (shortComplexFunctor C c i) K ⟶ Functor.obj (shortComplexFunctor C c i) L)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
        (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
this :
  ∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i) (hφ : φ ≫ K.d 0 i = 0),
    IsIso (Y := HomologicalComplex.cycles K 0) (HomologicalComplex.liftCycles K φ i hx hφ) ↔
      { X₁ := X, X₂ := K.X 0, X₃ := K.X i, f := φ, g := K.d 0 i, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Mono φ
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
suffices :
  ∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i) (hφ : φ ≫ K.d 0 i = 0),
    IsIso (Y := HomologicalComplex.cycles K 0) (HomologicalComplex.liftCycles K φ i hx hφ) ↔
      { X₁ := X, X₂ := K.X 0, X₃ := K.X i, f := φ, g := K.d 0 i, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Mono φ
⊢ IsIso (Y := HomologicalComplex.cycles K 0) (HomologicalComplex.liftCycles K φ 1 isIso_liftCycles_iff._proof_1 hφ) ↔
    { X₁ := X, X₂ := K.X 0, X₃ := K.X 1, f := φ, g := K.d 0 1, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Mono φ

Tactic:
suffices ∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i)
    (hφ : φ ≫ K.d 0 i = 0), IsIso (K.liftCycles φ i hx hφ) ↔
      (ShortComplex.mk _ _ hφ).Exact ∧ Mono φ from this 1 (by simp) hφ
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ_1 : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
hφ : Eq (α := X ⟶ K.X ((ComplexShape.up ℕ).next 0)) (φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0)) 0
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := X) 0 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ_1 : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
hφ : Eq (α := X ⟶ K.X ((ComplexShape.up ℕ).next 0)) (φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0)) 0
α : ShortComplex.mk (X₁ := X) (X₂ := X) (X₃ := X) 0 0 ⋯ ⟶ HomologicalComplex.sc K 0 :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (HomologicalComplex.sc K 0).f = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ_1 : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
hφ : Eq (α := X ⟶ K.X ((ComplexShape.up ℕ).next 0)) (φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0)) 0
α : ShortComplex.mk (X₁ := X) (X₂ := X) (X₃ := X) 0 0 ⋯ ⟶ HomologicalComplex.sc K 0 :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsIso (Y := HomologicalComplex.cycles K 0) (HomologicalComplex.liftCycles K φ ((ComplexShape.up ℕ).next 0) ⋯ hφ) ↔
    { X₁ := X, X₂ := K.X 0, X₃ := K.X ((ComplexShape.up ℕ).next 0), f := φ, g := K.d 0 ((ComplexShape.up ℕ).next 0),
          zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ

Tactic:
exact (ShortComplex.quasiIso_iff_isIso_liftCycles α rfl rfl (by simp)).symm.trans
    (ShortComplex.quasiIso_iff_of_zeros α rfl rfl (by simp))

Premises used: CategoryTheory.ShortComplex.quasiIso_iff_of_zeros, Iff.trans, Iff.symm, rfl, CategoryTheory.ShortComplex.quasiIso_iff_isIso_liftCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
this :
  ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
    IsIso (X := HomologicalComplex.opcycles K 0) (HomologicalComplex.descOpcycles K φ i hx hφ) ↔
      { X₁ := K.X i, X₂ := K.X 0, X₃ := X, f := K.d i 0, g := φ, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Epi φ
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
suffices :
  ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
    IsIso (X := HomologicalComplex.opcycles K 0) (HomologicalComplex.descOpcycles K φ i hx hφ) ↔
      { X₁ := K.X i, X₂ := K.X 0, X₃ := X, f := K.d i 0, g := φ, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Epi φ
⊢ IsIso (X := HomologicalComplex.opcycles K 0)
      (HomologicalComplex.descOpcycles K φ 1 isIso_descOpcycles_iff._proof_1 hφ) ↔
    { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := φ, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Epi φ

Tactic:
suffices ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i)
    (hφ : K.d i 0 ≫ φ = 0), IsIso (K.descOpcycles φ i hx hφ) ↔
      (ShortComplex.mk _ _ hφ).Exact ∧ Epi φ from this 1 (by simp) hφ
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ_1 : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
hφ : Eq (α := K.X ((ComplexShape.down ℕ).prev 0) ⟶ X) (K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ) 0
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := X) 0 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ_1 : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
hφ : Eq (α := K.X ((ComplexShape.down ℕ).prev 0) ⟶ X) (K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ) 0
α : HomologicalComplex.sc K 0 ⟶ ShortComplex.mk (X₁ := X) (X₂ := X) (X₃ := X) 0 0 ⋯ :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (HomologicalComplex.sc K 0).g = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ_1 : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
hφ : Eq (α := K.X ((ComplexShape.down ℕ).prev 0) ⟶ X) (K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ) 0
α : HomologicalComplex.sc K 0 ⟶ ShortComplex.mk (X₁ := X) (X₂ := X) (X₃ := X) 0 0 ⋯ :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsIso (X := HomologicalComplex.opcycles K 0)
      (HomologicalComplex.descOpcycles K φ ((ComplexShape.down ℕ).prev 0) ⋯ hφ) ↔
    { X₁ := K.X ((ComplexShape.down ℕ).prev 0), X₂ := K.X 0, X₃ := X, f := K.d ((ComplexShape.down ℕ).prev 0) 0, g := φ,
          zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Epi φ

Tactic:
exact (ShortComplex.quasiIso_iff_isIso_descOpcycles α (by simp) rfl rfl).symm.trans
    (ShortComplex.quasiIso_iff_of_zeros' α (by simp) rfl rfl)

Premises used: CategoryTheory.ShortComplex.quasiIso_iff_isIso_descOpcycles, CategoryTheory.ShortComplex.quasiIso_iff_of_zeros', Iff.trans, Iff.symm, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
dsimp :
  Eq (α := K.cycles j ⟶ K.X j)
    (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
        (ShortComplex.cyclesMap (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) K)) (K.sc' i j k).iCycles :
      K.cycles j ⟶ K.X j)
    (K.iCycles j : K.cycles j ⟶ K.X j)
⊢ Eq (α := K.cycles j ⟶ (K.sc' i j k).X₂)
    (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
      (Iso.hom (K.cyclesIsoSc' i j k hi hk) : K.cycles j ⟶ (K.sc' i j k).cycles)
      ((K.sc' i j k).iCycles : (K.sc' i j k).cycles ⟶ (K.sc' i j k).X₂))
    (K.iCycles j)

Tactic:
dsimp [cyclesIsoSc']

Premises used: HomologicalComplex.cyclesIsoSc'
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
simp :
  Eq (α := K.cycles j ⟶ K.X j) ((K.sc j).iCycles : (K.sc j).cycles ⟶ (K.sc j).X₂) (K.iCycles j : K.cycles j ⟶ K.X j)
⊢ Eq (α := K.cycles j ⟶ K.X j)
    (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
        (ShortComplex.cyclesMap (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) K)) (K.sc' i j k).iCycles :
      K.cycles j ⟶ K.X j)
    (K.iCycles j : K.cycles j ⟶ K.X j)

Tactic:
simp only [ShortComplex.cyclesMap_i, shortComplexFunctor_obj_X₂, shortComplexFunctor'_obj_X₂,
    natIsoSc'_hom_app_τ₂, comp_id]

Premises used: HomologicalComplex.shortComplexFunctor_obj_X₂, CategoryTheory.Category.comp_id, HomologicalComplex.shortComplexFunctor'_obj_X₂, HomologicalComplex.natIsoSc'_hom_app_τ₂, CategoryTheory.ShortComplex.cyclesMap_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.cycles j ⟶ K.X j) ((K.sc j).iCycles : (K.sc j).cycles ⟶ (K.sc j).X₂) (K.iCycles j : K.cycles j ⟶ K.X j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := (K.sc' i j k).cycles ⟶ K.X j)
    (CategoryStruct.comp (Y := K.cycles j) (Iso.inv (K.cyclesIsoSc' i j k hi hk)) (K.iCycles j) :
      (K.sc' i j k).cycles ⟶ K.X j)
    ((K.sc' i j k).iCycles : (K.sc' i j k).cycles ⟶ (K.sc' i j k).X₂)

Tactic:
simp [cyclesIsoSc', iCycles]

Premises used: HomologicalComplex.iCycles, HomologicalComplex.cyclesIsoSc'
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.X i ⟶ (K.sc' i j k).cycles)
    (CategoryStruct.comp (Y := K.cycles j) (K.toCycles i j) (Iso.hom (K.cyclesIsoSc' i j k hi hk)) :
      K.X i ⟶ (K.sc' i j k).cycles)
    ((K.sc' i j k).toCycles : (K.sc' i j k).X₁ ⟶ (K.sc' i j k).cycles)

Tactic:
simp only [← cancel_mono (K.sc' i j k).iCycles, assoc, cyclesIsoSc'_hom_iCycles,
    toCycles_i, ShortComplex.toCycles_i, shortComplexFunctor'_obj_f]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.toCycles_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.toCycles_i, HomologicalComplex.cyclesIsoSc'_hom_iCycles, CategoryTheory.ShortComplex.iCycles, HomologicalComplex.shortComplexFunctor'_obj_f, HomologicalComplex.sc'
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
dsimp :
  Eq (α := K.X j ⟶ K.opcycles j)
    (CategoryStruct.comp (Y := (K.sc' i j k).opcycles) (K.sc' i j k).pOpcycles
        (ShortComplex.opcyclesMap (NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) K)) :
      K.X j ⟶ K.opcycles j)
    (K.pOpcycles j : K.X j ⟶ K.opcycles j)
⊢ Eq (α := (K.sc' i j k).X₂ ⟶ K.opcycles j)
    (CategoryStruct.comp (Y := (K.sc' i j k).opcycles)
      ((K.sc' i j k).pOpcycles : (K.sc' i j k).X₂ ⟶ (K.sc' i j k).opcycles)
      (Iso.inv (K.opcyclesIsoSc' i j k hi hk) : (K.sc' i j k).opcycles ⟶ K.opcycles j))
    (K.pOpcycles j)

Tactic:
dsimp [opcyclesIsoSc']

Premises used: HomologicalComplex.opcyclesIsoSc'
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
simp :
  Eq (α := K.X j ⟶ K.opcycles j) ((K.sc j).pOpcycles : (K.sc j).X₂ ⟶ (K.sc j).opcycles)
    (K.pOpcycles j : K.X j ⟶ K.opcycles j)
⊢ Eq (α := K.X j ⟶ K.opcycles j)
    (CategoryStruct.comp (Y := (K.sc' i j k).opcycles) (K.sc' i j k).pOpcycles
        (ShortComplex.opcyclesMap (NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) K)) :
      K.X j ⟶ K.opcycles j)
    (K.pOpcycles j : K.X j ⟶ K.opcycles j)

Tactic:
simp only [ShortComplex.p_opcyclesMap, shortComplexFunctor'_obj_X₂, shortComplexFunctor_obj_X₂,
    natIsoSc'_inv_app_τ₂, id_comp]

Premises used: HomologicalComplex.natIsoSc'_inv_app_τ₂, HomologicalComplex.shortComplexFunctor_obj_X₂, HomologicalComplex.shortComplexFunctor'_obj_X₂, CategoryTheory.ShortComplex.p_opcyclesMap, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.X j ⟶ K.opcycles j) ((K.sc j).pOpcycles : (K.sc j).X₂ ⟶ (K.sc j).opcycles)
    (K.pOpcycles j : K.X j ⟶ K.opcycles j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.X j ⟶ (K.sc' i j k).opcycles)
    (CategoryStruct.comp (Y := K.opcycles j) (K.pOpcycles j) (Iso.hom (K.opcyclesIsoSc' i j k hi hk)) :
      K.X j ⟶ (K.sc' i j k).opcycles)
    ((K.sc' i j k).pOpcycles : (K.sc' i j k).X₂ ⟶ (K.sc' i j k).opcycles)

Tactic:
simp [opcyclesIsoSc', pOpcycles]

Premises used: HomologicalComplex.opcyclesIsoSc', HomologicalComplex.pOpcycles