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

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
⊢ ((mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).sc' ?mp.right.hS 0 1 2 ⋯ ⋯ ⋯).Exact

case mp.right.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' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex

Tactic:
swap

Result:
case mp.right.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' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex

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
⊢ ((mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).sc' ?mp.right.hS 0 1 2 ⋯ ⋯ ⋯).Exact

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

Tactic:
exact h.toIsComplex.zero i

Result:
no goals

Proof state:
case mp.right.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' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫
      (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).map' 1 2 ⋯ ⋯ =
    0

Tactic:
exact h.toIsComplex.zero n

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
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
rw [exact₂_iff]

Result:
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
⊢ ((mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).sc' ?mp.right.hS 0 1 2 ⋯ ⋯ ⋯).Exact

case mp.right.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' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex

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

Tactic:
intro h

Result:
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
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

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
⊢ ((mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).sc' ⋯ 0 1 2 ⋯ ⋯ ⋯).Exact

Tactic:
exact h.exact n (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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : autoParam (i + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

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

Tactic:
exact h'.exact 0

Result:
no goals

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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : autoParam (i + 2 ≤ n + 2) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

Tactic:
simp only [Nat.add_le_add_iff_right] at hi

Result:
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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝ : autoParam (i + 2 ≤ n + 2) _auto✝
hi : autoParam (i ≤ n) _auto✝
⊢ (S.sc ⋯ i ⋯).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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝ : autoParam (i + 2 ≤ n + 2) _auto✝
hi : autoParam (i ≤ n) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

Tactic:
obtain hi | rfl := hi.lt_or_eq

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

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

Proof state:
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 : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝ : autoParam (i + 2 ≤ n + 2) _auto✝
hi : autoParam (i ≤ n) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝ = 0

Tactic:
obtain hi | rfl := hi.lt_or_eq

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

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

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

Tactic:
exact h.exact i

Result:
no goals