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

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

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

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

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

Tactic:
simp

Result:
no goals

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

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

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

Tactic:
simp

Result:
no goals

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

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

Result:
no goals

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

Tactic:
rintro _ rfl hφ

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals