awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
⊢ S.Exact ↔
    (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
            S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
      S.δ₀.Exact
have mp : S.Exact →
  (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
          S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
mp :
  S.Exact →
    (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
            S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
      S.δ₀.Exact
⊢ S.Exact ↔
    (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
            S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
      S.δ₀.Exact
have mpr : (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
          S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact →
  S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact
have mp : (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
    S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' 1 2 isComplex₂_iff._proof_4 sorry : S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
mp :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact
have mp₁ : S.δ₀.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp : ShortComplex.Exact
  ((mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
          S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).sc'
    sorry 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5)
Tactic: rw [exact₂_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
mp :
  ShortComplex.Exact
    ((mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
            S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).sc'
      ⋯ 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5)
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp₁ : (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
    S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
      S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).IsComplex
Tactic: rw [exact₂_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).IsComplex
have mp : (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
            S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).map'
      0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
    (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
            S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).map'
      1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
  0
Tactic: rw [isComplex₂_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact
have mpr : ∀ (i : ℕ) (hi : i + 2 ≤ n + 2),
  Eq (α := S.obj (⟨i, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
    (S.map' i (i + 1) sorry sorry ≫ S.map' (i + 1) (i + 2) sorry hi : S.obj (⟨i, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
    (0 : S.obj (⟨i, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
Tactic: refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
mpr :
  ∀ (i : ℕ) (hi : i + 2 ≤ n + 2),
    Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
⊢ S.Exact
have mpr₁ : ∀ (i : ℕ) (hi : i + 2 ≤ n + 2), ShortComplex.Exact (S.sc sorry i hi)
Tactic: refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
have mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2),
  Eq (α := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩)
    (S.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry sorry ≫ S.map' (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2) sorry hi :
      S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩)
    (0 : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
mpr :
  ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2),
    Eq (α := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
      (S.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ ⋯ ≫ S.map' (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2) ⋯ hi :
        S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
      (0 : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
have mpr₁ : ∀ (i : ℕ) (hi : i + 1 + 2 ≤ n + 2),
  Eq (α := S.obj (⟨i + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, sorry⟩)
    (S.map' (i + 1) (i + 1 + 1) sorry sorry ≫ S.map' (i + 1 + 1) (i + 1 + 2) sorry hi :
      S.obj (⟨i + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, sorry⟩)
    (0 : S.obj (⟨i + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, sorry⟩)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ ShortComplex.Exact (S.sc ⋯ i hi)
have mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2), ShortComplex.Exact (S.sc sorry 0 hi)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2), ShortComplex.Exact (S.sc ⋯ 0 hi)
⊢ ShortComplex.Exact (S.sc ⋯ i hi)
have mpr₁ : ∀ (i : ℕ) (hi : i + 1 + 2 ≤ n + 2), ShortComplex.Exact (S.sc sorry (i + 1) hi)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
hS : S.Exact
⊢ S.δ₀.Exact
have hS₁ : (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
        S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).Exact ∧
  S.δ₀.Exact
Tactic: rw [exact_iff_δ₀] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact
have rw : (mk₂ (X₀ := S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 sorry : S.obj (⟨0, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 sorry :
        S.obj (⟨1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, sorry⟩ : Fin (n + 2 + 1)))).Exact ∧
  S.δ₀.Exact
Tactic: rw [exact_iff_δ₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
⊢ S.Exact ↔
    S.δlast.Exact ∧
      (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' (n + 1) (n + 2) ⋯ ⋯ :
            S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp : S.Exact →
  S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) sorry sorry : S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) sorry sorry :
          S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, sorry⟩ : Fin (n + 2 + 1)))).Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
mp :
  S.Exact →
    S.δlast.Exact ∧
      (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' (n + 1) (n + 2) ⋯ ⋯ :
            S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.Exact ↔
    S.δlast.Exact ∧
      (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' (n + 1) (n + 2) ⋯ ⋯ :
            S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mpr : S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) sorry sorry : S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) sorry sorry :
          S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, sorry⟩ : Fin (n + 2 + 1)))).Exact →
  S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp : S.δlast.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
mp : S.δlast.Exact
⊢ S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp₁ : (mk₂ (X₀ := S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' n (n + 1) sorry sorry : S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' (n + 1) (n + 2) sorry sorry : S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, sorry⟩ : Fin (n + 2 + 1)))).Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp : ShortComplex.Exact
  ((mk₂ (X₀ := S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) sorry sorry : S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) sorry sorry : S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, sorry⟩ : Fin (n + 2 + 1)))).sc'
    sorry 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5)
Tactic: rw [exact₂_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
mp :
  ShortComplex.Exact
    ((mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' (n + 1) (n + 2) ⋯ ⋯ :
            S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).sc'
      ⋯ 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5)
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
have mp₁ : (mk₂ (X₀ := S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' n (n + 1) sorry sorry : S.obj (⟨n, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)))
    (S.map' (n + 1) (n + 2) sorry sorry :
      S.obj (⟨n + 1, sorry⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, sorry⟩ : Fin (n + 2 + 1)))).IsComplex
Tactic: rw [exact₂_iff]