-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma exact_iff_δ₀ (S : ComposableArrows C (n + 2)) :
    S.Exact ↔ (mk₂ (S.map' 0 1) (S.map' 1 2)).Exact ∧ S.δ₀.Exact

Proof state:
case mp.left
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact

Tactic:
rw [exact₂_iff]

Result:
case mp.left
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).sc' ?mp.left.hS 0 1 2 ⋯ ⋯ ⋯).Exact

case mp.left.hS
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).IsComplex

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact ↔ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact → (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact → S.Exact

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

Tactic:
exact h₀.toIsComplex.zero i

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor

Result:
case mp.left
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact

case mp.right
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δ₀.Exact

Proof state:
case mpr.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : autoParam (i + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

Tactic:
obtain _ | i := i

Result:
case mpr.intro.refine_2.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
hi : autoParam (0 + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ 0 ⋯).Exact

case mpr.intro.refine_2.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : autoParam (i + 1 + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ (i + 1) ⋯).Exact

Proof state:
case mpr.intro.refine_2.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : autoParam (i + 1 + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ (i + 1) ⋯).Exact

Tactic:
exact h₀.exact i

Result:
no goals

Proof state:
case mpr.intro.refine_2.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
hi : autoParam (0 + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ 0 ⋯).Exact

Tactic:
exact h.exact 0

Result:
no goals

Proof state:
case mp.right
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δ₀.Exact

Tactic:
exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1)))
  (fun i hi => h.exact (i + 1))

Result:
no goals

Proof state:
case mp.left
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).sc' ⋯ 0 1 2 ⋯ ⋯ ⋯).Exact

Tactic:
exact h.exact 0 (by omega)

Result:
no goals

Proof state:
case mpr.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact

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

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

case mpr.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : autoParam (i + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

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

Tactic:
omega

Result:
no goals

Proof state:
case mp.left.hS
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯ = 0

Tactic:
exact h.toIsComplex.zero 0

Result:
no goals

Proof state:
case mp.left.hS
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).IsComplex

Tactic:
rw [isComplex₂_iff]

Result:
case mp.left.hS
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯ = 0

Proof state:
case mpr.intro.refine_1.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
hi : autoParam (0 + 2 ≤ n + 2) _auto✝
⊢ S.map' 0 (0 + 1) ⋯ ⋯ ≫ S.map' (0 + 1) (0 + 2) ⋯ hi = 0

Tactic:
exact h.toIsComplex.zero 0

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact → S.Exact

Tactic:
rintro ⟨h, h₀⟩

Result:
case mpr.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact

Proof state:
case mp.left
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).sc' ?mp.left.hS 0 1 2 ⋯ ⋯ ⋯).Exact

case mp.left.hS
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).IsComplex

Tactic:
swap

Result:
case mp.left.hS
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).IsComplex

case mp.left
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).sc' ?mp.left.hS 0 1 2 ⋯ ⋯ ⋯).Exact