-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma isComplex₂_iff (S : ComposableArrows C 2) :
    S.IsComplex ↔ S.map' 0 1 ≫ S.map' 1 2 = 0

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
hi : autoParam (0 + 2 ≤ 2) _auto✝
⊢ S.map' 0 (0 + 1) ⋯ ⋯ ≫ S.map' (0 + 1) (0 + 2) ⋯ hi = 0

Tactic:
exact h

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.IsComplex ↔ S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.IsComplex → S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0 → S.IsComplex

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
i : ℕ
hi : autoParam (i + 2 ≤ 2) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
obtain rfl : i = 0 := by omega

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
hi : autoParam (0 + 2 ≤ 2) _auto✝
⊢ S.map' 0 (0 + 1) ⋯ ⋯ ≫ S.map' (0 + 1) (0 + 2) ⋯ hi = 0

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
⊢ S.IsComplex

Tactic:
refine IsComplex.mk (fun i hi => ?_)

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
i : ℕ
hi : autoParam (i + 2 ≤ 2) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0 → S.IsComplex

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
⊢ S.IsComplex

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0
i : ℕ
hi : autoParam (i + 2 ≤ 2) _auto✝
⊢ i = 0

Tactic:
omega

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.IsComplex → S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.IsComplex
⊢ S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.IsComplex
⊢ 0 + 2 ≤ 2

Tactic:
omega

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.IsComplex
⊢ S.map' 0 1 ⋯ ⋯ ≫ S.map' 1 2 ⋯ ⋯ = 0

Tactic:
exact h.zero 0 (by omega)

Result:
no goals