awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀

Tactic:
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀

Premises used: CategoryTheory.CategoryStruct.id, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
rw : 𝟙 X₁ ≫ d₀ = d₀
rw₁ rw₂ : d₀ = d₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.id_comp]

Premises used: if_pos, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
change : (if 2 = HAdd.hAdd (α := ℕ) 1 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁

Tactic:
change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁

Premises used: CategoryTheory.CategoryStruct.id, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
rw : 𝟙 X₂ ≫ d₁ = d₁
rw₁ rw₂ : d₁ = d₁
⊢ (if 2 = HAdd.hAdd (α := ℕ) 1 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁

Tactic:
rw [if_pos rfl, Category.id_comp]

Premises used: if_pos, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex.{v, u} V
h : S = S'
rw rw₁ :
  (succ S').fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S'.X₁) ×' d₂ ≫ S'.f = 0) =
    (succ S').fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S'.X₁) ×' d₂ ≫ S'.f = 0)
⊢ (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) =
    (succ S').fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S'.X₁) ×' d₂ ≫ S'.f = 0)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex.{v, u} V
h : S = S'
subst :
  (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) =
    (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0)
⊢ (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) =
    (succ S').fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S'.X₁) ×' d₂ ≫ S'.f = 0)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S : ShortComplex.{v, u} V
⊢ (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) =
    (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex.{v, u} V
h : S = S'
subst : S.X₁ = S.X₁
⊢ S'.X₁ = S.X₁

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S : ShortComplex.{v, u} V
⊢ S.X₁ = S.X₁

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex.{v, u} V
h : S = S'
subst :
  (succ S).snd (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0).fst (β :=
      fun (d₂ : (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) ⟶ S.X₁) ↦ d₂ ≫ S.f = 0) =
    eqToHom ⋯ ≫
      (succ S).snd (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0).fst (β :=
          fun (d₂ : (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) ⟶ S.X₁) ↦ d₂ ≫ S.f = 0) ≫
        eqToHom ⋯
⊢ (succ S).snd (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0).fst (β :=
      fun (d₂ : (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) ⟶ S.X₁) ↦ d₂ ≫ S.f = 0) =
    eqToHom ⋯ ≫
      (succ S').snd (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S'.X₁) ×' d₂ ≫ S'.f = 0).fst (β :=
          fun (d₂ : (succ S').fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S'.X₁) ×' d₂ ≫ S'.f = 0) ⟶ S'.X₁) ↦ d₂ ≫ S'.f = 0) ≫
        eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S : ShortComplex.{v, u} V
⊢ (succ S).snd (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0).fst (β :=
      fun (d₂ : (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) ⟶ S.X₁) ↦ d₂ ≫ S.f = 0) =
    eqToHom ⋯ ≫
      (succ S).snd (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0).fst (β :=
          fun (d₂ : (succ S).fst (β := fun (X₃ : V) ↦ (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0) ⟶ S.X₁) ↦ d₂ ≫ S.f = 0) ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
rw :
  mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1 + 1)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
      ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1 + 1) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯
⊢ mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
      ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯

Tactic:
rw [show n + 2 = n + 1 + 1 from rfl]

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1 + 1)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
      ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1 + 1) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯

Tactic:
simp [mk, mkAux]

Premises used: ChainComplex.mk, ChainComplex.mkAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
rw :
  (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) =
    PSigma.fst (β := fun (X₃ : V) ↦
      (d₂ : X₃ ⟶ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁) ×' d₂ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f = 0)
      (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n))
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) =
    PSigma.fst (β := fun (X₃ : V) ↦
      (d₂ :
        X₃ ⟶
          (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
              ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).X₁) ×'
        d₂ ≫
            (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).f =
          0)
      (succ
        (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
          ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯))

Tactic:
rw [← mk_congr_succ_X₃ succ
      (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)]

Premises used: ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d, ChainComplex.mk_congr_succ_X₃
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) =
    PSigma.fst (β := fun (X₃ : V) ↦
      (d₂ : X₃ ⟶ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁) ×' d₂ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f = 0)
      (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0 = X₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 1 = X₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 1 0 = d₀

Tactic:
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀

Premises used: CategoryTheory.CategoryStruct.id, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
rw : 𝟙 X₁ ≫ d₀ = d₀
rw₁ rw₂ : d₀ = d₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.id_comp]

Premises used: if_pos, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
zero :
  HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 2) ≅
    PSigma.fst (β := fun (X₂ : V) ↦
      (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
        Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
      (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0))
succ₁ :
  (n : ℕ) →
    HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 2) ≅
      PSigma.fst (β := fun (X₂ : V) ↦
        (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
          Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
            (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
        (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)))
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 2) ≅
    PSigma.fst (β := fun (X₂ : V) ↦
      (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1)) ×'
        d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n = 0)
      (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n))

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
zero :
  HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 2) =
    PSigma.fst (β := fun (X₂ : V) ↦
      (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
        Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
      (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0))
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 2) ≅
    PSigma.fst (β := fun (X₂ : V) ↦
      (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
        Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
      (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0))

Tactic:
apply eqToIso

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
zero :
  (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) =
    (succ' (𝟙 X₁ ≫ d₀)).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ 𝟙 X₁ ≫ d₀ = 0)
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 2) =
    PSigma.fst (β := fun (X₂ : V) ↦
      (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
        Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
      (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0))

Tactic:
dsimp [mk', mk, of, mkAux, of.d]

Premises used: ChainComplex.of, ChainComplex.mk', ChainComplex.of.d, ChainComplex.mk, ChainComplex.mkAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
zero zero₁ :
  (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) =
    (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)
⊢ (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) =
    (succ' (𝟙 X₁ ≫ d₀)).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ 𝟙 X₁ ≫ d₀ = 0)

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 2) ≅
    PSigma.fst (β := fun (X₂ : V) ↦
      (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
        Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
      (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)))

Tactic:
exact mkXIso _ _ _ _ _ (succ' d₀).2.2 (fun S => succ' S.f) n

Premises used: PSigma.snd, ChainComplex.mkXIso, CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
X Y : V
f g : X ⟶ Y
h : f = g
rw rw₁ :
  (succ' g).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ g = 0) =
    (succ' g).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ g = 0)
⊢ (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) =
    (succ' g).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ g = 0)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
X Y : V
f g : X ⟶ Y
h : f = g
subst :
  (succ' f).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0).fst (β :=
      fun (d : (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) ⟶ X) ↦ d ≫ f = 0) =
    eqToHom ⋯ ≫
      (succ' f).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0).fst (β :=
        fun (d : (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) ⟶ X) ↦ d ≫ f = 0)
⊢ (succ' f).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0).fst (β :=
      fun (d : (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) ⟶ X) ↦ d ≫ f = 0) =
    eqToHom ⋯ ≫
      (succ' g).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ g = 0).fst (β :=
        fun (d : (succ' g).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ g = 0) ⟶ X) ↦ d ≫ g = 0)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
X Y : V
f : X ⟶ Y
⊢ (succ' f).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0).fst (β :=
      fun (d : (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) ⟶ X) ↦ d ≫ f = 0) =
    eqToHom ⋯ ≫
      (succ' f).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0).fst (β :=
        fun (d : (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) ⟶ X) ↦ d ≫ f = 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
zero zero₁ : d₀ = d₀
⊢ d₀ =
    (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
      1 0

Tactic:
rw [mk_d_1_0]

Premises used: ChainComplex.mk_d_1_0
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 2) ⟶
      HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1))
    (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 2) (n + 1 + 1))
    (Iso.hom (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁ : V} ↦ succ') (n + 1)) ≫
      PSigma.fst (β :=
        fun
          (d :
            PSigma.fst (β := fun (X₂ : V) ↦
                (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
                  Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
                    (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
                (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1))) ⟶
              HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ↦
        Eq (α :=
          PSigma.fst (β := fun (X₂ : V) ↦
              (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
                Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
                  (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
              (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1))) ⟶
            HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
        (PSigma.snd (β := fun (X₂ : V) ↦
          (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
            Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
              (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
          (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)))))

Tactic:
apply mk_d

Premises used: ChainComplex.mk_d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        f'' ≫ Q.d (n + 2) (n + 1) =
          P.d (n + 2) (n + 1) ≫
            p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f).fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              f' ≫ Q.d (n + 1) n =
                P.d (n + 1) n ≫
                  p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f))
m : ℕ
⊢ Eq (α := P.X (m + 1) ⟶ Q.X m)
    (PSigma.fst (β := fun (f : P.X (m + 1) ⟶ Q.X (m + 1)) ↦
        (f' : P.X (m + 1 + 1) ⟶ Q.X (m + 1 + 1)) ×' f' ≫ Q.d (m + 1 + 1) (m + 1) = P.d (m + 1 + 1) (m + 1) ≫ f)
        (P.mkHomAux Q zero one one_zero_comm succ (m + 1)) ≫
      Q.d (m + 1) m)
    (P.d (m + 1) m ≫
      (P.mkHomAux Q zero one one_zero_comm succ m).fst (β := fun (f : P.X m ⟶ Q.X m) ↦
        (f' : P.X (m + 1) ⟶ Q.X (m + 1)) ×' f' ≫ Q.d (m + 1) m = P.d (m + 1) m ≫ f))

Tactic:
(mkHomAux P Q zero one one_zero_comm succ m).2.2

Premises used: PSigma.snd, ChainComplex.mkHomAux