awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : (i : J) → Ext.{w, v, u} X (Y i) n
i b : J
_ : Membership.mem (γ := Finset J) Finset.univ b → b ≠ i → (x b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0
⊢ Membership.mem (γ := Finset J) Finset.univ b → b ≠ i → (x b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0

Tactic:
_
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : (i : J) → Ext.{w, v, u} X (Y i) n
i b : J
h : Membership.mem (γ := Finset J) Finset.univ b
hij : b ≠ i
rw : Eq (α := Ext.{w, v, u} X (Y i) n) ((x b).comp (mk₀ (if h : b = i then eqToHom ⋯ else 0)) ⋯) 0
rw₁ : Eq (α := Ext.{w, v, u} X (Y i) n) ((x b).comp (mk₀ 0) ⋯) 0
rw₂ : Eq (α := Ext.{w, v, u} X (Y i) n) ((x b).comp 0 ⋯) 0
rw₃ rw₄ : Eq.{w + 1} (α := Ext.{w, v, u} X (Y i) n) 0 0
⊢ (x b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0

Tactic:
rw [c.ι_π, dif_neg hij, mk₀_zero, comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, dif_neg, CategoryTheory.Abelian.Ext.mk₀_zero, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x x_1 : Ext.{w, v, u} X c.pt n
⊢ (fun (i : J) ↦ (x + x_1).comp (mk₀ (c.π i)) ⋯) =
    HAdd.hAdd (α := (i : J) → Ext.{w, v, u} X (Y i) n) (fun (i : J) ↦ x.comp (mk₀ (c.π i)) ⋯) fun (i : J) ↦
      x_1.comp (mk₀ (c.π i)) ⋯

Tactic:
simp only [add_comp, Pi.add_def]

Premises used: CategoryTheory.Abelian.Ext.add_comp, Pi.add_def
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X₁ X₂ Y : C
n : ℕ
x : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
⊢ (fun (e : Ext.{w, v, u} X₁ Y n × Ext.{w, v, u} X₂ Y n) ↦
        HAdd.hAdd (α := Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n) (comp (mk₀ biprod.fst) e.1 ⋯)
          (comp (mk₀ biprod.snd) e.2 ⋯))
      ((fun (e : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n) ↦ (comp (mk₀ biprod.inl) e ⋯, comp (mk₀ biprod.inr) e ⋯)) x) =
    x

Tactic:
simp only [mk₀_comp_mk₀_assoc, ← add_comp, ← mk₀_add, biprod.total, mk₀_id_comp]

Premises used: CategoryTheory.Abelian.Ext.add_comp, CategoryTheory.Abelian.Ext.mk₀_id_comp, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc, CategoryTheory.Abelian.Ext.mk₀_add, CategoryTheory.Limits.biprod.total
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X₁ X₂ Y : C
n : ℕ
x : Ext.{w, v, u} X₁ Y n × Ext.{w, v, u} X₂ Y n
⊢ (fun (e : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n) ↦ (comp (mk₀ biprod.inl) e ⋯, comp (mk₀ biprod.inr) e ⋯))
      ((fun (e : Ext.{w, v, u} X₁ Y n × Ext.{w, v, u} X₂ Y n) ↦
          HAdd.hAdd (α := Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n) (comp (mk₀ biprod.fst) e.1 ⋯)
            (comp (mk₀ biprod.snd) e.2 ⋯))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X₁ X₂ Y : C
n : ℕ
⊢ ∀ (x y : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n),
    (comp (mk₀ biprod.inl) (x + y) ⋯, comp (mk₀ biprod.inr) (x + y) ⋯) =
      (comp (mk₀ biprod.inl) x ⋯, comp (mk₀ biprod.inr) x ⋯) + (comp (mk₀ biprod.inl) y ⋯, comp (mk₀ biprod.inr) y ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y₁ Y₂ : C
n : ℕ
e : Ext.{w, v, u} X (biprod.{v, u} Y₁ Y₂) n
⊢ (fun (e : Ext.{w, v, u} X Y₁ n × Ext.{w, v, u} X Y₂ n) ↦
        HAdd.hAdd (α := Ext.{w, v, u} X (biprod.{v, u} Y₁ Y₂) n) (e.1.comp (mk₀ biprod.inl) ⋯)
          (e.2.comp (mk₀ biprod.inr) ⋯))
      ((fun (e : Ext.{w, v, u} X (biprod.{v, u} Y₁ Y₂) n) ↦ (e.comp (mk₀ biprod.fst) ⋯, e.comp (mk₀ biprod.snd) ⋯)) e) =
    e

Tactic:
simp only [comp_assoc_of_second_deg_zero, mk₀_comp_mk₀, ← comp_add, ← mk₀_add,
      biprod.total, comp_mk₀_id]

Premises used: CategoryTheory.Abelian.Ext.comp_add, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.Abelian.Ext.mk₀_add, CategoryTheory.Abelian.Ext.comp_mk₀_id, CategoryTheory.Limits.biprod.total, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y₁ Y₂ : C
n : ℕ
x : Ext.{w, v, u} X Y₁ n × Ext.{w, v, u} X Y₂ n
⊢ (fun (e : Ext.{w, v, u} X (biprod.{v, u} Y₁ Y₂) n) ↦ (e.comp (mk₀ biprod.fst) ⋯, e.comp (mk₀ biprod.snd) ⋯))
      ((fun (e : Ext.{w, v, u} X Y₁ n × Ext.{w, v, u} X Y₂ n) ↦
          HAdd.hAdd (α := Ext.{w, v, u} X (biprod.{v, u} Y₁ Y₂) n) (e.1.comp (mk₀ biprod.inl) ⋯)
            (e.2.comp (mk₀ biprod.inr) ⋯))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y₁ Y₂ : C
n : ℕ
⊢ ∀ (x y : Ext.{w, v, u} X (biprod.{v, u} Y₁ Y₂) n),
    ((x + y).comp (mk₀ biprod.fst) ⋯, (x + y).comp (mk₀ biprod.snd) ⋯) =
      (x.comp (mk₀ biprod.fst) ⋯, x.comp (mk₀ biprod.snd) ⋯) + (y.comp (mk₀ biprod.fst) ⋯, y.comp (mk₀ biprod.snd) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : HasExt.{w', v, u} C
X Y : C
n : ℕ
inst_4 : HasDerivedCategory.{w'', v, u} C
e : Ext.{w, v, u} X Y n
⊢ Eq.{w'' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w'', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    ((homEquiv : (a : Ext X Y n) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑n : ℤ))
        ((chgUniv : (a : Ext X Y n) → Ext X Y n) e) :
      ShiftedHom (C := DerivedCategory.{w'', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    ((homEquiv : (a : Ext X Y n) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑n : ℤ)) e :
      ShiftedHom (C := DerivedCategory.{w'', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
apply SmallShiftedHom.equiv_chgUniv

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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
simp :
  (∀ (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 : ℤ))
⊢ HasExt.{w', v, u} C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (Ext.{w, v, u} X Y n)

Tactic:
simp only [hasExt_iff, small_congr Ext.homEquiv]

Premises used: small_congr, CategoryTheory.Abelian.Ext.homEquiv, CategoryTheory.hasExt_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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 : ℤ))
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)))
⊢ (∀ (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 : ℤ))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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 : ℤ),
    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 : ℕ
⊢ LE.le (α := ℤ) 0 (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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 : ℤ),
    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 : ℤ))

Tactic:
exact h X Y n (by simp)

Premises used: Nat.cast
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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
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)))
⊢ 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:
lift n to ℕ using hn
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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 : ℕ
⊢ 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:
h X Y n
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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 : ℕ
⊢ 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:
exact h X Y n
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (mapToComposableArrows φ).app 0 = φ.τ₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (mapToComposableArrows φ).app 1 = φ.τ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (mapToComposableArrows φ).app 2 = φ.τ₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ExactSequence
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
subst :
  ∀ (hk : i + 1 + 1 ≤ n),
    Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
      (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
      (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
⊢ 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, ⋯⟩)

Tactic:
subst hij hjk
-- Module: Mathlib.Algebra.Homology.ExactSequence
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 : ℕ
hk : i + 1 + 1 ≤ n
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)

Tactic:
hS.zero i hk

Premises used: CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
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 : ℕ
hk : i + 1 + 1 ≤ n
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨i + 1 + 1, ⋯⟩)

Tactic:
exact hS.zero i hk

Premises used: CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
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
rw₅ rw₆ : Eq.{v_1 + 1} (α := S₁.obj' i ⋯ ⟶ S₂.obj ⟨i + 2, ⋯⟩) 0 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, ⋯⟩)

Tactic:
rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]

Premises used: CategoryTheory.ComposableArrows.app', CategoryTheory.Limits.comp_zero, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.zero_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.Algebra.Homology.ExactSequence
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₂
⊢ S₁.IsComplex ↔ S₂.IsComplex

Tactic:
⟨isComplex_of_iso e, isComplex_of_iso e.symm⟩

Premises used: CategoryTheory.ComposableArrows.isComplex_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ExactSequence
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 0
i : ℕ
hi : i + 2 ≤ 0
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi :
      S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
simp at hi
-- Module: Mathlib.Algebra.Homology.ExactSequence
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
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi :
      S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.ExactSequence
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
subst : ∀ (hk : i + 1 + 1 ≤ n), (S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ hk).Exact
⊢ (S.sc' ⋯ i j k hij hjk hk).Exact

Tactic:
subst hij hjk
-- Module: Mathlib.Algebra.Homology.ExactSequence
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 : ℕ
hk : i + 1 + 1 ≤ n
⊢ (S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ hk).Exact

Tactic:
hS.exact i hk

Premises used: CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
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 : ℕ
hk : i + 1 + 1 ≤ n
⊢ (S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ hk).Exact

Tactic:
exact hS.exact i hk

Premises used: CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
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))
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)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ExactSequence
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).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ExactSequence
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).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ExactSequence
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).τ₃ =
    ShortComplex.Hom.τ₃ (𝟙 (S₁.sc' h₁ i j k hij hjk hk))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ExactSequence
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))
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)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ExactSequence
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).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ExactSequence
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).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ExactSequence
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).τ₃ =
    ShortComplex.Hom.τ₃ (𝟙 (S₂.sc' h₂ i j k hij hjk hk))

Tactic:
simp