awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv
have obtain : ∀ (w : c.Rel i (c.next i)), f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv
Tactic: obtain rfl := c.next_eq' w
Cleared hypotheses: j, w
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
f : C₁ ⟶ C₂
inst_2 : IsIso f
j : ι
⊢ (inv f).f j = inv (f.f j)
have hom_inv_id : (inv f).f j ≫ f.f j = 𝟙 (C₂.X j)
Tactic: apply IsIso.eq_inv_of_inv_hom_id
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
i j : α
h : i = j + 1
⊢ X i = X (j + 1)
have rw : X (j + 1) = X (j + 1)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : (ComplexShape.down α).Rel i j
hjk : (ComplexShape.down α).Rel j k
⊢ of.d X d i j ≫ of.d X d j k = 0
have dsimp : Eq.{v + 1} (α := X i ⟶ X k)
  (CategoryStruct.comp (Y := X j) (if h : i = j + 1 then eqToHom sorry ≫ d j else 0)
    (if h : j = k + 1 then eqToHom sorry ≫ d k else 0))
  0
Tactic: dsimp [of.d] at hij hjk ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : j + 1 = i
hjk : k + 1 = j
⊢ Eq.{v + 1} (α := X i ⟶ X k)
    (CategoryStruct.comp (Y := X j) (if h : i = j + 1 then eqToHom ⋯ ≫ d j else 0)
      (if h : j = k + 1 then eqToHom ⋯ ≫ d k else 0))
    0
have substs : Eq.{v + 1} (α := X (k + 1 + 1) ⟶ X k)
  (CategoryStruct.comp (Y := X (k + 1)) (if h : k + 1 + 1 = k + 1 + 1 then eqToHom sorry ≫ d (k + 1) else 0)
    (if h : k + 1 = k + 1 then eqToHom sorry ≫ d k else 0))
  0
Tactic: substs hij hjk
Cleared hypotheses: i, j, hij, hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
⊢ of.d X d (j + 1) j = d j
have dsimp : (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
Tactic: dsimp [of.d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
have rw : 𝟙 (X (j + 1)) ≫ d j = d j
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
rw : 𝟙 (X (j + 1)) ≫ d j = d j
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
have rw₁ : d j = d j
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀
have change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
Tactic: change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
have rw : 𝟙 X₁ ≫ d₀ = d₀
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
have rw₁ : d₀ = d₀
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁
have change : (if 2 = HAdd.hAdd (α := ℕ) 1 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
Tactic: change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (if 2 = HAdd.hAdd (α := ℕ) 1 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
have rw : 𝟙 X₂ ≫ d₁ = d₁
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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₁
⊢ (if 2 = HAdd.hAdd (α := ℕ) 1 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
have rw₁ : d₁ = d₁
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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'
⊢ (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)
have 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)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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'
⊢ (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)
have 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)
Tactic: subst h
Cleared hypotheses: S', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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'
⊢ S'.X₁ = S.X₁
have subst : S.X₁ = S.X₁
Tactic: subst h
Cleared hypotheses: S', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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'
⊢ (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 ⋯
have 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 sorry ≫
    (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 sorry
Tactic: subst h
Cleared hypotheses: S', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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₃ ⟶
          (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) ⋯))
have 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))
Tactic: rw [← mk_congr_succ_X₃ succ
      (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 1 0 = d₀
have change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
Tactic: change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
have rw : 𝟙 X₁ ≫ d₀ = d₀
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
have rw₁ : d₀ = d₀
Tactic: rw [if_pos rfl, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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 + 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))
have 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))
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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))
⊢ 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))
have 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)))
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ 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))
have 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))
Tactic: apply eqToIso
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ 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))
have 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)
Tactic: dsimp [mk', mk, of, mkAux, of.d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (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)
have 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)
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (succ' f).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ f = 0) =
    (succ' g).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X) ×' d ≫ g = 0)
have 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)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ (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)
have 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 sorry ≫
    (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: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
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
⊢ 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
have zero : d₀ = d₀
Tactic: rw [mk_d_1_0]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
i j : α
h : i + 1 = j
⊢ X (i + 1) = X j
have rw : X j = X j
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ (ComplexShape.up α).Rel i j → (ComplexShape.up α).Rel j k → of.d X d i j ≫ of.d X d j k = 0
have dsimp : i + 1 = j →
  j + 1 = k →
    Eq.{v + 1} (α := X i ⟶ X k)
      (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom sorry else 0)
        (if h : j + 1 = k then d j ≫ eqToHom sorry else 0))
      0
Tactic: dsimp [of.d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ i + 1 = j →
    j + 1 = k →
      Eq.{v + 1} (α := X i ⟶ X k)
        (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0)
          (if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0))
        0
have pos : ∀ (h : i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → (d i ≫ eqToHom sorry) ≫ d j ≫ eqToHom sorry = 0
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
pos : ∀ (h : i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → (d i ≫ eqToHom ⋯) ≫ d j ≫ eqToHom ⋯ = 0
⊢ i + 1 = j →
    j + 1 = k →
      Eq.{v + 1} (α := X i ⟶ X k)
        (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0)
          (if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0))
        0
have neg : ∀ (h : i + 1 = j) (h' : ¬j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) ((d i ≫ eqToHom sorry) ≫ 0) 0
Tactic: split_ifs with h h' h'