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)
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)))).IsComplex
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)))).map'
      0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
    (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)))).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 : S.δlast.Exact
h' :
  (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
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 : S.δlast.Exact
h' :
  (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
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 (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)
h : S.δlast.Exact
h' :
  (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
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 hi₁ : i ≤ n
Tactic: simp only [Nat.add_le_add_iff_right] at 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 : S.δlast.Exact
h' :
  (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
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi : i ≤ n
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : 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 : i < n),
  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_1 : 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: obtain hi | rfl := hi.lt_or_eq
-- 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.δlast.Exact
h' :
  (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
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi : i ≤ n
mpr :
  ∀ (hi : i < n),
    Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 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_1 : 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₁ : ∀ (S : ComposableArrows.{v_1, u_1} C (i + 2)) (h : S.δlast.Exact)
  (h' :
    (mk₂ (X₀ := S.obj (⟨i, sorry⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, sorry⟩ : Fin (i + 2 + 1)))
        (S.map' i (i + 1) sorry sorry : S.obj (⟨i, sorry⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, sorry⟩ : Fin (i + 2 + 1)))
        (S.map' (i + 1) (i + 2) sorry sorry :
          S.obj (⟨i + 1, sorry⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, sorry⟩ : Fin (i + 2 + 1)))).Exact)
  (hi : i + 2 ≤ i + 2) (hi_2 : i ≤ i),
  Eq (α := S.obj (⟨i, sorry⟩ : Fin (i + 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 (i + 2 + 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
    (0 : S.obj (⟨i, sorry⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
Tactic: obtain hi | rfl := hi.lt_or_eq
Cleared hypotheses: n, S, h, h', hi_1, 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)
h : S.δlast.Exact
h' :
  (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
i : ℕ
hi : i + 2 ≤ n + 2
⊢ ShortComplex.Exact (S.sc ⋯ i hi)
have hi₁ : i ≤ n
Tactic: simp only [Nat.add_le_add_iff_right] at 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 : S.δlast.Exact
h' :
  (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
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi : i ≤ n
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)
have mpr : ∀ (hi : i < n), ShortComplex.Exact (S.sc sorry i hi_1)
Tactic: obtain hi | rfl := hi.lt_or_eq
-- 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.δlast.Exact
h' :
  (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
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi : i ≤ n
mpr : ∀ (hi : i < n), ShortComplex.Exact (S.sc ⋯ i hi_1)
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)
have mpr₁ : ∀ (S : ComposableArrows.{v_1, u_1} C (i + 2)) (h : S.δlast.Exact)
  (h' :
    (mk₂ (X₀ := S.obj (⟨i, sorry⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, sorry⟩ : Fin (i + 2 + 1)))
        (S.map' i (i + 1) sorry sorry : S.obj (⟨i, sorry⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, sorry⟩ : Fin (i + 2 + 1)))
        (S.map' (i + 1) (i + 2) sorry sorry :
          S.obj (⟨i + 1, sorry⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, sorry⟩ : Fin (i + 2 + 1)))).Exact)
  (hi : i + 2 ≤ i + 2) (hi_2 : i ≤ i), ShortComplex.Exact (S.sc sorry i hi)
Tactic: obtain hi | rfl := hi.lt_or_eq
Cleared hypotheses: n, S, h, h', hi_1, 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.δlast.Exact
have hS₁ : 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: rw [exact_iff_δlast] 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₁ : S.δlast.Exact
h₂ :
  (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
have rw : 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: rw [exact_iff_δlast]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (hypothesis)
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : Preadditive.{v_2, u_2} C
inst_2 : Balanced.{v_2, u_2} C
n : ℕ
S : ComposableArrows.{v_2, u_2} C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ :
  Eq (α := S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (0 : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
⊢ IsIso (X := S.obj ⟨k + 1, ⋯⟩) (Y := S.obj ⟨k + 2, ⋯⟩)
    (S.map' (k + 1) (k + 2) ⋯ ⋯ : S.obj (⟨k + 1, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
have this : Mono (S.sc sorry k sorry).g
Tactic: have := (hS.exact k).mono_g h₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequence (hypothesis)
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : Preadditive.{v_2, u_2} C
inst_2 : Balanced.{v_2, u_2} C
n : ℕ
S : ComposableArrows.{v_2, u_2} C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ :
  Eq (α := S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (0 : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
this : Mono (S.sc ⋯ k ⋯).g
⊢ IsIso (X := S.obj ⟨k + 1, ⋯⟩) (Y := S.obj ⟨k + 2, ⋯⟩)
    (S.map' (k + 1) (k + 2) ⋯ ⋯ : S.obj (⟨k + 1, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
have this₁ : Epi (S.sc sorry (k + 1) hk).f
Tactic: have := (hS.exact (k + 1)).epi_f h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ K.ExactAt j ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j
have rw : (K.sc' i j k).Exact ↔
  ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
    x₂ ≫ K.d j k = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j
Tactic: rw [K.exactAt_iff' i j k hi hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
γ : A ⟶ K.homology i
j : ι
hj : c.next i = j
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : z ≫ K.d i j = 0),
    π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i
have subst : ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : Eq (α := A' ⟶ K.X (c.next i)) (z ≫ K.d i (c.next i)) 0),
  π ≫ γ = K.liftCycles z (c.next i) sorry hz ≫ K.homologyπ i
Tactic: subst hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j
have subst : ∀ (hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0),
  Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) sorry hx₂ ≫ K.homologyπ j) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j
Tactic: subst hi hk
Cleared hypotheses: i, k, hi, hk, hx₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
hx₂' : x₂' ≫ K.d j k = 0
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j) (K.liftCycles x₂' k hk hx₂' ≫ K.homologyπ j) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d i j
have subst : ∀ (hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0)
  (hx₂' : Eq (α := A ⟶ K.X (c.next j)) (x₂' ≫ K.d j (c.next j)) 0),
  Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) sorry hx₂ ≫ K.homologyπ j)
      (K.liftCycles x₂' (c.next j) sorry hx₂' ≫ K.homologyπ j) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d (c.prev j) j
Tactic: subst hi hk
Cleared hypotheses: i, k, hi, hk, hx₂, hx₂'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
A : C
z₂ : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ z₂ = x₁ ≫ K.toCycles i j
have subst : z₂ ≫ K.homologyπ j = 0 ↔
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = x₁ ≫ K.toCycles (c.prev j) j
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
A : C
z₂ z₂' : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles i j
have subst : z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles (c.prev j) j
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
z : A ⟶ K.X i
j : ι
hj : c.prev i = j
⊢ Eq (α := A ⟶ K.opcycles i) (z ≫ K.pOpcycles i) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ K.X j), π ≫ z = x ≫ K.d j i
have subst : Eq (α := A ⟶ K.opcycles i) (z ≫ K.pOpcycles i) 0 ↔
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ K.X (c.prev i)), π ≫ z = x ≫ K.d (c.prev i) i
Tactic: subst hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ Mono (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 →
        ∀ (y₁ : A ⟶ L.X i),
          x₂ ≫ φ.f j = y₁ ≫ L.d i j → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j
have subst : Mono (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
  ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
    Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0 →
      ∀ (y₁ : A ⟶ L.X (c.prev j)),
        x₂ ≫ φ.f j = y₁ ≫ L.d (c.prev j) j →
          ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j
Tactic: subst hi hk
Cleared hypotheses: i, k, hi, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Refinements (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ Epi (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
      y₂ ≫ L.d j k = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ K.X j) (_ : x₂ ≫ K.d j k = 0) (y₁ : A' ⟶ L.X i),
          π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d i j
have subst : Epi (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
  ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
    Eq (α := A ⟶ L.X (c.next j)) (y₂ ≫ L.d j (c.next j)) 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ K.X j) (_ :
        Eq (α := A' ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0) (y₁ : A' ⟶ L.X (c.prev j)),
        π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d (c.prev j) j
Tactic: subst hi hk
Cleared hypotheses: i, k, hi, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
W' : C
k : W' ⟶ kernel S.g
hk rw : Eq (α := W' ⟶ cokernel S.f) (k ≫ kernel.ι S.g ≫ cokernel.π S.f) 0
⊢ Eq (α := W' ⟶ cokernel S.f) ((k ≫ kernel.ι S.g) ≫ cokernel.π S.f) 0
have rw₁ : Eq.{v + 1} (α := W' ⟶ cokernel S.f) 0 0
Tactic: rw [assoc, hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
have rw : f' = f'
Tactic: rw [kernel.lift_ι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ S.LeftHomologyData
have hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' sorry) (kernel.ι γ)
Tactic: have hf' : f' = kernel.lift γ f' (by simp [γ, f']) ≫ kernel.ι γ := by rw [kernel.lift_ι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
⊢ Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
have rw : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ))
  (CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' sorry) (kernel.ι γ) ≫ cokernel.π (kernel.ι γ)) 0
Tactic: rw [hf']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
⊢ S.LeftHomologyData
have wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
Tactic: have wπ : f' ≫ cokernel.π (kernel.ι γ) = 0 := by
    rw [hf']
    simp only [assoc, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
⊢ S.LeftHomologyData
have he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
Tactic: have he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel :=
    IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero