-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma isIso_descOpcycles_iff (K : ChainComplex C ℕ) {X : C} (φ : K.X 0 ⟶ X)
    [K.HasHomology 0] (hφ : K.d 1 0 ≫ φ = 0) :
    IsIso (K.descOpcycles φ 1 (by simp) hφ) ↔
      (ShortComplex.mk _ _ hφ).Exact ∧ Epi φ

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
α : HomologicalComplex.sc K 0 ⟶ ShortComplex.mk 0 0 ⋯ := { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsIso (HomologicalComplex.descOpcycles K φ ((ComplexShape.down ℕ).prev 0) ⋯ hφ) ↔
    (ShortComplex.mk (K.d ((ComplexShape.down ℕ).prev 0) 0) φ hφ).Exact ∧ Epi φ

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

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
⊢ IsIso (HomologicalComplex.descOpcycles K φ 1 ⋯ hφ) ↔ (ShortComplex.mk (K.d 1 0) φ hφ).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φ

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
⊢ ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
    IsIso (HomologicalComplex.descOpcycles K φ i hx hφ) ↔ (ShortComplex.mk (K.d i 0) φ hφ).Exact ∧ Epi φ

Proof state:
C : Type u_1
inst✝² : Category.{?u.188210, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
⊢ ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
    IsIso (HomologicalComplex.descOpcycles K φ i hx hφ) ↔ (ShortComplex.mk (K.d i 0) φ hφ).Exact ∧ Epi φ

Tactic:
rintro _ rfl hφ

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
⊢ IsIso (HomologicalComplex.descOpcycles K φ ((ComplexShape.down ℕ).prev 0) ⋯ hφ) ↔
    (ShortComplex.mk (K.d ((ComplexShape.down ℕ).prev 0) 0) φ hφ).Exact ∧ Epi φ

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
α : HomologicalComplex.sc K 0 ⟶ ShortComplex.mk 0 0 ⋯ := { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (HomologicalComplex.sc K 0).g = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
⊢ 0 ≫ 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
this :
  ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
    IsIso (HomologicalComplex.descOpcycles K φ i hx hφ) ↔ (ShortComplex.mk (K.d i 0) φ hφ).Exact ∧ Epi φ
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
⊢ IsIso (HomologicalComplex.descOpcycles K φ ((ComplexShape.down ℕ).prev 0) ⋯ hφ) ↔
    (ShortComplex.mk (K.d ((ComplexShape.down ℕ).prev 0) 0) φ hφ).Exact ∧ Epi φ

Tactic:
let α : K.sc 0 ⟶ ShortComplex.mk (0 : X ⟶ X) (0 : X ⟶ X) (by simp) :=
  { τ₁ := 0
    τ₂ := φ
    τ₃ := 0 }

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
α : HomologicalComplex.sc K 0 ⟶ ShortComplex.mk 0 0 ⋯ := { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsIso (HomologicalComplex.descOpcycles K φ ((ComplexShape.down ℕ).prev 0) ⋯ hφ) ↔
    (ShortComplex.mk (K.d ((ComplexShape.down ℕ).prev 0) 0) φ hφ).Exact ∧ Epi φ