awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
inst_3 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
inst :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
inst₁ :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₂) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₂)
inst₂ :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₃) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₃)
⊢ IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ :
      X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)

Tactic:
apply +allowSynthFailures ShortComplex.isIso_of_isIso

Premises used: CategoryTheory.ShortComplex.isIso_of_isIso
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₁)

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₂) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₂)

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₃) (Y := (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).X₃)

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ :
      X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)

Tactic:
have : IsIso (shortComplexMap X f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂) := by
    apply +allowSynthFailures ShortComplex.isIso_of_isIso <;> assumption
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ :
  IsIso (X :=
    (X.H n₀).obj (Functor.obj (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) (mk₃ f₁ f₂ f₃)))
    ((X.H n₀).map (Functor.map (functorArrows ι 2 3 3 isIso_map._proof_3 shortComplexMap._proof_7) α))
h₁ :
  IsIso (X := (X.H n₁).obj (Functor.obj (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) (mk₃ f₁ f₂ f₃)))
    ((X.H n₁).map (Functor.map (functorArrows ι 1 2 3 isIso_map._proof_5 isIso_map._proof_3) α))
h₂ :
  IsIso (X := (X.H n₂).obj (Functor.obj (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) (mk₃ f₁ f₂ f₃)))
    ((X.H n₂).map (Functor.map (functorArrows ι 0 1 3 isIso_map._proof_7 isIso_map._proof_9) α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
this :
  IsIso (X := X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (Y := X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ :
      X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯)
⊢ IsIso (X := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (Y := X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂)
    (ShortComplex.homologyMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homology ⟶ (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).homology)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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
hf : IsIso f
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
simpa only [Preadditive.IsIso.comp_left_eq_zero] using X.zero₃ f g _ rfl n₀ n₁

Premises used: CategoryTheory.Preadditive.IsIso.comp_left_eq_zero, CategoryTheory.Abelian.SpectralObject.zero₃, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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
hg : IsIso g
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
simpa only [Preadditive.IsIso.comp_right_eq_zero] using X.zero₁ f g _ rfl n₀ n₁

Premises used: CategoryTheory.Preadditive.IsIso.comp_right_eq_zero, CategoryTheory.Abelian.SpectralObject.zero₁, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
⊢ map' (mk₁ (𝟙 i)) 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ (asIso f).hom =
    Iso.hom (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) ≫
      (mk₁ f).map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))

Tactic:
IsZero.of_iso ?_ ((X.H n).mapIso e.symm)

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
refine : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (𝟙 i)))
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))

Tactic:
refine IsZero.of_iso ?_ ((X.H n).mapIso e.symm)

Premises used: CategoryTheory.Abelian.SpectralObject.H, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ Eq.{v_2 + 1} (α := i ⟶ i) (𝟙 i ≫ 𝟙 i) (𝟙 i)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0

Tactic:
have h := X.zero₂ (𝟙 i) (𝟙 i) (𝟙 i) (by simp) n
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
h :
  Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0
⊢ Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0

Tactic:
rw [← Functor.map_comp] at h

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
h :
  Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0
rw : (X.H n).map (𝟙 (mk₁ (𝟙 i))) = (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (𝟙 i)))

Tactic:
rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← h]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl (obj'.{v_2, u_2} (mk₁ (𝟙 i)) 0 homMk₁._proof_4)) (asIso f) ⋯
h :
  Eq (α := (X.H n).obj (mk₁ (𝟙 i)) ⟶ (X.H n).obj (mk₁ (𝟙 i)))
    ((X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)) 0
e_a :
  Eq.{v_2 + 1} (α := Quiver.Hom (V := ComposableArrows.{v_2, u_2} ι 1) (mk₁ (𝟙 i)) (mk₁ (𝟙 i))) (𝟙 (mk₁ (𝟙 i)))
    (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)
⊢ (X.H n).map (𝟙 (mk₁ (𝟙 i))) = (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
⊢ hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) ≫
      Fork.ι (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯ ≫ Fork.ι (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯)

Tactic:
simpa using hi.fac _ .zero

Premises used: CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
⊢ hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯

Tactic:
have : hi.lift (KernelFork.ofι _ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).zero) =
      X.δToCycles f₁ f₂ f₃ n₀ n₁ :=
    Fork.IsLimit.hom_ext hi (by simpa using hi.fac _ .zero)
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ X.iCycles f₁ f₂ n₁ ≫ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
rw :
  Eq (α := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt ⟶ cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯))
    (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯ ≫ cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) 0
⊢ Eq (α := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt ⟶ cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯))
    (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯) ≫
      cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯))
    0

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ Eq (α := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt ⟶ cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯))
    (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯ ≫ cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
refine_1 :
  parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
      (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0 ≅
    parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) 0
refine_2 :
  (Cocone.precompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
                      (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (Iso.refl
                ((parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
                      (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).inv).obj
      (CokernelCofork.ofπ (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) ⋯) ≅
    Cofork.ofπ (P := cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) ⋯
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (cokernelIsCokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁))

Premises used: CategoryTheory.Abelian.SpectralObject.δToCycles, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.cokernelIsCokernel, Equiv.invFun
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ (parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
            (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).map
        WalkingParallelPairHom.left ≫
      Iso.hom
        (Iso.refl
          ((parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
                (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.one)) =
    Iso.hom
        (Iso.refl
          ((parallelPair (X := (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯).pt)
                (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.zero)) ≫
      (parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) 0).map WalkingParallelPairHom.left

Tactic:
simpa