-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma exact₂_iff (S : ComposableArrows C 2) (hS : S.IsComplex) :
    S.Exact ↔ (S.sc' hS 0 1 2).Exact

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact → S.Exact

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact
⊢ S.Exact

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

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
hS : S.IsComplex
h : (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact
hi : autoParam (0 + 2 ≤ 2) _auto✝
⊢ (S.sc hS 0 ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ S.Exact ↔ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ S.Exact → (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact → S.Exact

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

Tactic:
omega

Result:
no goals

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

Tactic:
exact h

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact
⊢ S.Exact

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

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

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : S.Exact
⊢ 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
hS : S.IsComplex
h : S.Exact
⊢ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact

Tactic:
exact h.exact 0 (by 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
hS : S.IsComplex
⊢ S.Exact → (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : S.Exact
⊢ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact