awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₃ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact

Tactic:
((X.exact₃' n₀ n₁ hn₁ (mk₂ f g))).exact 0

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.Abelian.SpectralObject.exact₃', CategoryTheory.ComposableArrows.mk₂, CategoryTheory.Abelian.SpectralObject.sc₃, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.Abelian.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, CategoryTheory.ComposableArrows.Exact.exact, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₃ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact

Tactic:
exact ((X.exact₃' n₀ n₁ hn₁ (mk₂ f g))).exact 0

Premises used: CategoryTheory.Abelian.SpectralObject.exact₃', CategoryTheory.ComposableArrows.mk₂, OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.composableArrows₅ f g fg h n₀ n₁ hn₁).Exact

Tactic:
exact_of_δ₀ (X.exact₂ _ _ _ h n₀).exact_toComposableArrows
    (exact_of_δ₀ (X.exact₃ _ _ _ h n₀ n₁ hn₁).exact_toComposableArrows
      (exact_of_δ₀ (X.exact₁ _ _ _ h n₀ n₁ hn₁).exact_toComposableArrows
        ((X.exact₂ _ _ _ h n₁).exact_toComposableArrows)))

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.Abelian.SpectralObject.exact₃, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.Abelian.SpectralObject.exact₁, CategoryTheory.ComposableArrows.exact_of_δ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯ ≫ (X.H n₂).map (𝟙 (mk₁ f))

Tactic:
have eq := X.δ_naturality f g f (g ≫ h) (𝟙 _) (twoδ₂Toδ₁ g h _ rfl) n₁ n₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯ ≫ (X.H n₂).map (𝟙 (mk₁ f))
⊢ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯

Tactic:
rw [Functor.map_id, comp_id] at eq

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
rw : X.δ g h n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = 0
rw₁ : Eq (α := (X.H n₀).obj (mk₁ h) ⟶ (X.H n₂).obj (mk₁ f)) (0 ≫ X.δ f (g ≫ h) n₁ n₂ ⋯) 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := (X.H n₀).obj (mk₁ h) ⟶ (X.H n₂).obj (mk₁ f)) 0 0
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0

Tactic:
rw [← eq, X.zero₁_assoc g h _ rfl n₀ n₁ hn₁, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, CategoryTheory.Abelian.SpectralObject.zero₁_assoc, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
⊢ f ≫ inv f = 𝟙 i₀

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
rw : IsIso (X := (mk₁ f).obj 0) (φ.app 0) ∧ IsIso (X := (mk₁ f).obj 1) (φ.app 1)
⊢ IsIso φ

Tactic:
rw [isIso_iff₁]

Premises used: CategoryTheory.ComposableArrows.isIso_iff₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
left : IsIso (X := (mk₁ f).obj 0) (φ.app 0)
right : IsIso (X := (mk₁ f).obj 1) (φ.app 1)
⊢ IsIso (X := (mk₁ f).obj 0) (φ.app 0) ∧ IsIso (X := (mk₁ f).obj 1) (φ.app 1)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
left : IsIso (𝟙 i₀ ≫ f)
⊢ IsIso (X := (mk₁ f).obj 0) (φ.app 0)

Tactic:
dsimp [φ]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
right : IsIso (inv f ≫ 𝟙 i₀)
⊢ IsIso (X := (mk₁ f).obj 1) (φ.app 1)

Tactic:
dsimp [φ]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (𝟙 i₀ ≫ f)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (inv f ≫ 𝟙 i₀)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso φ

Tactic:
have : IsIso φ := by
    rw [isIso_iff₁]
    constructor <;> dsimp [φ] <;> infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
rw : Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
⊢ IsZero.{u_4, u_1} ((X.H n).obj (mk₁ f))

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
⊢ f ≫ inv f = 𝟙 i₀

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
rw : 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₁ : (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₂ : (X.H n).map φ = 0
rw₃ : (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯)
rw₄ rw₅ : (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯)
⊢ Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0

Tactic:
rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.zero₂, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.inv, CategoryTheory.Limits.zero_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ : ℤ
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero.{u_3, u_1} ((X.H n₀).obj (mk₁ f))
⊢ Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
(X.exact₂ f g fg hfg n₀).mono_g (h₁.eq_of_src _ _)

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.ShortComplex.Exact.mono_g, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₂ : IsZero.{u_3, u_1} ((X.H n₁).obj (mk₁ f))
⊢ Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
(X.exact₃ f g fg hfg n₀ n₁ hn₁).epi_f (h₂.eq_of_tgt _ _)

Premises used: CategoryTheory.ShortComplex.Exact.epi_f, CategoryTheory.Abelian.SpectralObject.exact₃, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero.{u_3, u_1} ((X.H n₀).obj (mk₁ f))
h₂ : IsZero.{u_3, u_1} ((X.H n₁).obj (mk₁ f))
⊢ Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
have := X.mono_H_map_twoδ₁Toδ₀ n₀ f g fg hfg h₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero.{u_3, u_1} ((X.H n₀).obj (mk₁ f))
h₂ : IsZero.{u_3, u_1} ((X.H n₁).obj (mk₁ f))
this : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
⊢ Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
have := X.epi_H_map_twoδ₁Toδ₀ n₀ n₁ hn₁ f g fg hfg h₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero.{u_3, u_1} ((X.H n₀).obj (mk₁ f))
h₂ : IsZero.{u_3, u_1} ((X.H n₁).obj (mk₁ f))
this_1 : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
this : Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
ι' : Type u_3
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, u_4, u_3} C ι'
n₀ : ℤ
i₀ i₁ i₂ : ι'
h₀₁ : i₀ ≤ i₁
h₁₂ : i₁ ≤ i₂
h₁ : IsZero.{u_4, u_1} ((X'.H n₀).obj (mk₁ (homOfLE h₀₁)))
⊢ Mono ((X'.H n₀).map (twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))

Tactic:
X'.mono_H_map_twoδ₁Toδ₀ _ _ _ _ _ h₁

Premises used: CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
ι' : Type u_3
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, u_4, u_3} C ι'
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι'
h₀₁ : i₀ ≤ i₁
h₁₂ : i₁ ≤ i₂
h₂ : IsZero.{u_4, u_1} ((X'.H n₁).obj (mk₁ (homOfLE h₀₁)))
⊢ Epi ((X'.H n₀).map (twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))

Tactic:
X'.epi_H_map_twoδ₁Toδ₀ _ _ hn₁ _ _ _ _ h₂

Premises used: CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.Basic
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
ι' : Type u_3
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, u_4, u_3} C ι'
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι'
h₀₁ : i₀ ≤ i₁
h₁₂ : i₁ ≤ i₂
h₁ : IsZero.{u_4, u_1} ((X'.H n₀).obj (mk₁ (homOfLE h₀₁)))
h₂ : IsZero.{u_4, u_1} ((X'.H n₁).obj (mk₁ (homOfLE h₀₁)))
⊢ IsIso ((X'.H n₀).map (twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))

Tactic:
X'.isIso_H_map_twoδ₁Toδ₀ _ _ hn₁ _ _ _ _ h₁ h₂

Premises used: CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
⊢ Mono (X := X.cycles f g n) (kernel.ι (X.δ f g n (n + 1) ⋯))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
⊢ Epi (Y := X.opcycles f g n) (cokernel.π (X.δ f g (n - 1) n ⋯))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))
rw : X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n) = X.pOpcycles f g n ≫ 0
⊢ IsZero.{v_1, u_1} (X.opcycles f g n)

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_epi (X.pOpcycles ..)]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))
⊢ X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n) = X.pOpcycles f g n ≫ 0

Tactic:
apply h.eq_of_src

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ g))
rw : 𝟙 (X.cycles f g n) ≫ X.iCycles f g n = 0 ≫ X.iCycles f g n
⊢ IsZero.{v_1, u_1} (X.cycles f g n)

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_mono (X.iCycles ..)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.Abelian.SpectralObject.iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ g))
⊢ 𝟙 (X.cycles f g n) ≫ X.iCycles f g n = 0 ≫ X.iCycles f g n

Tactic:
apply h.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
subst : X.iCycles f g n₀ ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0
⊢ X.iCycles f g n₀ ≫ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
subst hn₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ : ℤ
⊢ X.iCycles f g n₀ ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0

Tactic:
simp [iCycles]

Premises used: CategoryTheory.Abelian.SpectralObject.iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₀ = n₁ - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁), X.δ f g (n₁ - 1) n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0
⊢ X.δ f g n₀ n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₁ : ℤ
hn₁ : n₁ - 1 + 1 = n₁
⊢ X.δ f g (n₁ - 1) n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0

Tactic:
simp [pOpcycles]

Premises used: CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
dsimp : Mono (X.iCycles f g n₀)
⊢ Mono (X.kernelSequenceCycles f g n₀ n₁ hn₁).f

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ Mono (X.iCycles f g n₀)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
dsimp : Epi (X.pOpcycles f g n₁)
⊢ Epi (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).g

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ Epi (X.pOpcycles f g n₁)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
subst : (X.kernelSequenceCycles f g n₀ (n₀ + 1) ⋯).Exact
⊢ (X.kernelSequenceCycles f g n₀ n₁ hn₁).Exact

Tactic:
subst hn₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ : ℤ
⊢ (X.kernelSequenceCycles f g n₀ (n₀ + 1) ⋯).Exact

Tactic:
apply ShortComplex.exact_kernel

Premises used: CategoryTheory.ShortComplex.exact_kernel
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁), (X.cokernelSequenceOpcycles f g (n₁ - 1) n₁ hn₁).Exact
⊢ (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).Exact

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₁ : ℤ
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.cokernelSequenceOpcycles f g (n₁ - 1) n₁ hn₁).Exact

Tactic:
apply ShortComplex.exact_cokernel

Premises used: CategoryTheory.ShortComplex.exact_cokernel
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
x : A ⟶ (X.H n₀).obj (mk₁ g)
hx : x ≫ X.δ f g n₀ n₁ hn₁ = 0
⊢ x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0

Tactic:
subst hn₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ : ℤ
A : C
x : A ⟶ (X.H n₀).obj (mk₁ g)
hx : x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0
⊢ x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0

Tactic:
hx
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ : ℤ
A : C
x : A ⟶ (X.H n₀).obj (mk₁ g)
hx : x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0
⊢ x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0

Tactic:
exact hx
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
x : A ⟶ (X.H n₀).obj (mk₁ g)
hx : x ≫ X.δ f g n₀ n₁ hn₁ = 0
⊢ X.liftCycles f g n₀ n₁ hn₁ x hx ≫ X.iCycles f g n₀ = x

Tactic:
apply kernel.lift_ι

Premises used: CategoryTheory.Limits.kernel.lift_ι