awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
this : HasDerivedCategory C := HasDerivedCategory.standard C
mp :
  (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          (Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory C) n) (Functor.obj (singleFunctor C 0) Y)))) →
    ∀ (X Y : C) (n : ℕ),
      Small.{w', max u v}
        (ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          (Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory C) n) (Functor.obj (singleFunctor C 0) Y)))) ↔
    ∀ (X Y : C) (n : ℕ),
      Small.{w', max u v}
        (ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
have mpr : (∀ (X Y : C) (n : ℕ),
    Small.{w', max u v}
      (ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))) →
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        (Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory C) n) (Functor.obj (singleFunctor C 0) Y)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  ∀ (X Y : C) (n : ℕ),
    Small.{w', max u v}
      (ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
X Y : C
n : ℤ
hn : 0 ≤ n
⊢ Small.{w', max u v}
    (Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory C) n) (Functor.obj (singleFunctor C 0) Y)))
have mpr : ∀ (n : ℕ),
  Small.{w', max u v}
    (Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) (↑n : ℤ)) (Functor.obj (singleFunctor C 0) Y)))
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- 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
hS : S.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k, ⋯⟩)
    (CategoryStruct.comp (Y := S.obj ⟨j, ⋯⟩) (S.map' i j ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨j, ⋯⟩)
        (S.map' j k ⋯ hk : S.obj (⟨j, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k, ⋯⟩) :
      S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k, ⋯⟩)
have subst : ∀ (hk : i + 1 + 1 ≤ n),
  Eq (α := S.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, sorry⟩)
    (S.map' i (i + 1) sorry sorry ≫ S.map' (i + 1) (i + 1 + 1) sorry hk : S.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, sorry⟩)
    (0 : S.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, sorry⟩)
Tactic: subst hij hjk
Cleared hypotheses: j, k, hij, hjk, hk
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ Eq (α := S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (0 : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
have rw : Eq (α := S₁.obj' i sorry ⟶ S₂.obj ⟨i + 2, sorry⟩) (app' e.hom i sorry ≫ S₂.map' i (i + 1) sorry sorry ≫ S₂.map' (i + 1) (i + 2) sorry hi)
  (app' e.hom i sorry ≫ 0)
Tactic: rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
rw :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi)
    (app' e.hom i ⋯ ≫ 0)
⊢ Eq (α := S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (0 : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
have rw₁ : Eq (α := S₁.obj' i sorry ⟶ S₂.obj ⟨i + 2, sorry⟩) (app' e.hom i sorry ≫ S₂.map' i (i + 1) sorry sorry ≫ S₂.map' (i + 1) (i + 2) sorry hi) 0
Tactic: rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
rw :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi)
    (app' e.hom i ⋯ ≫ 0)
rw₁ :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi) 0
⊢ Eq (α := S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (0 : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
have rw₂ : S₁.map (homOfLE sorry) ≫ e.hom.app (⟨i + 1, sorry⟩ : Fin (n + 1)) ≫ S₂.map' (i + 1) (i + 2) sorry hi = 0
Tactic: rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
rw :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi)
    (app' e.hom i ⋯ ≫ 0)
rw₁ :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi) 0
rw₂ : S₁.map (homOfLE ⋯) ≫ e.hom.app (⟨i + 1, ⋯⟩ : Fin (n + 1)) ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0
⊢ Eq (α := S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (0 : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
have rw₃ : S₁.map (homOfLE sorry) ≫ S₁.map (homOfLE sorry) ≫ e.hom.app (⟨i + 2, sorry⟩ : Fin (n + 1)) = 0
Tactic: rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
rw :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi)
    (app' e.hom i ⋯ ≫ 0)
rw₁ :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi) 0
rw₂ : S₁.map (homOfLE ⋯) ≫ e.hom.app (⟨i + 1, ⋯⟩ : Fin (n + 1)) ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0
rw₃ : S₁.map (homOfLE ⋯) ≫ S₁.map (homOfLE ⋯) ≫ e.hom.app (⟨i + 2, ⋯⟩ : Fin (n + 1)) = 0
⊢ Eq (α := S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (0 : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
have rw₄ : Eq (α := S₁.obj' i sorry ⟶ S₂.obj ⟨i + 2, sorry⟩) (0 ≫ e.hom.app (⟨i + 2, sorry⟩ : Fin (n + 1))) 0
Tactic: rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
rw :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi)
    (app' e.hom i ⋯ ≫ 0)
rw₁ :
  Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi) 0
rw₂ : S₁.map (homOfLE ⋯) ≫ e.hom.app (⟨i + 1, ⋯⟩ : Fin (n + 1)) ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0
rw₃ : S₁.map (homOfLE ⋯) ≫ S₁.map (homOfLE ⋯) ≫ e.hom.app (⟨i + 2, ⋯⟩ : Fin (n + 1)) = 0
rw₄ : Eq (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) (0 ≫ e.hom.app (⟨i + 2, ⋯⟩ : Fin (n + 1))) 0
⊢ Eq (α := S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
    (0 : S₂.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S₂.obj ⟨i + 2, ⋯⟩)
have rw₅ : Eq.{v_1 + 1} (α := S₁.obj' i sorry ⟶ S₂.obj ⟨i + 2, sorry⟩) 0 0
Tactic: rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]
-- 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
hS : S.Exact
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (S.sc' ⋯ i j k hij hjk hk).Exact
have subst : ∀ (hk : i + 1 + 1 ≤ n), (S.sc' sorry i (i + 1) (i + 1 + 1) sorry sorry hk).Exact
Tactic: subst hij hjk
Cleared hypotheses: j, k, hij, hjk, hk
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk = 𝟙 (S₁.sc' h₁ i j k hij hjk hk)
have h₃ : (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₁ =
  ShortComplex.Hom.τ₁ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
h₃ :
  (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))
⊢ sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk = 𝟙 (S₁.sc' h₁ i j k hij hjk hk)
have h₄ : (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₂ =
  ShortComplex.Hom.τ₂ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
h₃ :
  (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))
h₄ :
  (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))
⊢ sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk = 𝟙 (S₁.sc' h₁ i j k hij hjk hk)
have h₅ : (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₃ =
  ShortComplex.Hom.τ₃ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk = 𝟙 (S₂.sc' h₂ i j k hij hjk hk)
have h₃ : (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₁ =
  ShortComplex.Hom.τ₁ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
h₃ :
  (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))
⊢ sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk = 𝟙 (S₂.sc' h₂ i j k hij hjk hk)
have h₄ : (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₂ =
  ShortComplex.Hom.τ₂ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
h₃ :
  (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))
h₄ :
  (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))
⊢ sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk = 𝟙 (S₂.sc' h₂ i j k hij hjk hk)
have h₅ : (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₃ =
  ShortComplex.Hom.τ₃ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi = 𝟙 (S₁.sc h₁ i hi)
have h₃ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₁.sc h₁ i hi))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
h₃ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₁.sc h₁ i hi))
⊢ scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi = 𝟙 (S₁.sc h₁ i hi)
have h₄ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₁.sc h₁ i hi))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
h₃ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₁.sc h₁ i hi))
h₄ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₁.sc h₁ i hi))
⊢ scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi = 𝟙 (S₁.sc h₁ i hi)
have h₅ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₃ = ShortComplex.Hom.τ₃ (𝟙 (S₁.sc h₁ i hi))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi = 𝟙 (S₂.sc h₂ i hi)
have h₃ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₂.sc h₂ i hi))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
h₃ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₂.sc h₂ i hi))
⊢ scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi = 𝟙 (S₂.sc h₂ i hi)
have h₄ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₂.sc h₂ i hi))
Tactic: ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
h₃ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₂.sc h₂ i hi))
h₄ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₂.sc h₂ i hi))
⊢ scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi = 𝟙 (S₂.sc h₂ i hi)
have h₅ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₃ = ShortComplex.Hom.τ₃ (𝟙 (S₂.sc h₂ i hi))
Tactic: ext
-- 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
S : ComposableArrows.{v_1, u_1} C 1
i : ℕ
hi : i + 2 ≤ 1
⊢ ShortComplex.Exact (S.sc ⋯ i hi)
have exfalso : False
Tactic: exfalso
-- 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
S : ComposableArrows.{v_1, u_1} C 2
⊢ S.IsComplex ↔
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0
have mp : S.IsComplex →
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
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
S : ComposableArrows.{v_1, u_1} C 2
mp :
  S.IsComplex →
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0
⊢ S.IsComplex ↔
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0
have mpr : S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0 →
  S.IsComplex
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
S : ComposableArrows.{v_1, u_1} C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
⊢ S.IsComplex
have mpr : ∀ (i : ℕ) (hi : i + 2 ≤ 2),
  Eq (α := S.obj (⟨i, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 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 (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
    (0 : S.obj (⟨i, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, sorry⟩)
Tactic: refine IsComplex.mk (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
S : ComposableArrows.{v_1, u_1} C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
i : ℕ
hi : i + 2 ≤ 2
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi :
      S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
have mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2),
  Eq (α := S.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 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 (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩)
    (0 : S.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩)
Tactic: obtain rfl : i = 0 := by lia
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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
⊢ S.Exact ↔ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
have mp : S.Exact → (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
mp : S.Exact → (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
⊢ S.Exact ↔ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
have mpr : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
⊢ S.Exact
have mpr : ∀ (i : ℕ) (hi : i + 2 ≤ 2), (S.sc hS i hi).Exact
Tactic: refine Exact.mk hS (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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
i : ℕ
hi : i + 2 ≤ 2
⊢ (S.sc hS i hi).Exact
have mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2), (S.sc hS 0 hi).Exact
Tactic: obtain rfl : i = 0 := by lia
Cleared hypotheses: i, hi