awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c) (Functor.obj (single V c j) A) (Functor.obj (single V c j) B))
    (CategoryTheory.Functor.map (single V c j) f) (CategoryTheory.Functor.map (single V c j) g)
rw :
  Eq (α := A ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j) (f ≫ Iso.inv (singleObjXSelf c j B))
    (g ≫ Iso.inv (singleObjXSelf c j B))
⊢ f = g
have rw₁ : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
  (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B))
  (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
Tactic: rw [← cancel_mono (singleObjXSelf c j B).inv,
      ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self,
      ← single_map_f_self, w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c) (Functor.obj (single V c j) A) (Functor.obj (single V c j) B))
    (CategoryTheory.Functor.map (single V c j) f) (CategoryTheory.Functor.map (single V c j) g)
rw :
  Eq (α := A ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j) (f ≫ Iso.inv (singleObjXSelf c j B))
    (g ≫ Iso.inv (singleObjXSelf c j B))
rw₁ :
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B))
    (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
⊢ f = g
have rw₂ : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
  (Hom.f (CategoryTheory.Functor.map (single V c j) f) j)
  (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
Tactic: rw [← cancel_mono (singleObjXSelf c j B).inv,
      ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self,
      ← single_map_f_self, w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c) (Functor.obj (single V c j) A) (Functor.obj (single V c j) B))
    (CategoryTheory.Functor.map (single V c j) f) (CategoryTheory.Functor.map (single V c j) g)
rw :
  Eq (α := A ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j) (f ≫ Iso.inv (singleObjXSelf c j B))
    (g ≫ Iso.inv (singleObjXSelf c j B))
rw₁ :
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B))
    (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
rw₂ :
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Hom.f (CategoryTheory.Functor.map (single V c j) f) j)
    (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
⊢ f = g
have rw₃ : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
  (Hom.f (CategoryTheory.Functor.map (single V c j) f) j) (Hom.f (CategoryTheory.Functor.map (single V c j) g) j)
Tactic: rw [← cancel_mono (singleObjXSelf c j B).inv,
      ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self,
      ← single_map_f_self, w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c) (Functor.obj (single V c j) A) (Functor.obj (single V c j) B))
    (CategoryTheory.Functor.map (single V c j) f) (CategoryTheory.Functor.map (single V c j) g)
rw :
  Eq (α := A ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j) (f ≫ Iso.inv (singleObjXSelf c j B))
    (g ≫ Iso.inv (singleObjXSelf c j B))
rw₁ :
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B))
    (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
rw₂ :
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Hom.f (CategoryTheory.Functor.map (single V c j) f) j)
    (Iso.hom (singleObjXSelf c j A) ≫ g ≫ Iso.inv (singleObjXSelf c j B))
rw₃ :
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Hom.f (CategoryTheory.Functor.map (single V c j) f) j) (Hom.f (CategoryTheory.Functor.map (single V c j) g) j)
⊢ f = g
have rw₄ : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
  (Hom.f (CategoryTheory.Functor.map (single V c j) g) j) (Hom.f (CategoryTheory.Functor.map (single V c j) g) j)
Tactic: rw [← cancel_mono (singleObjXSelf c j B).inv,
      ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self,
      ← single_map_f_self, w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c) (Functor.obj (single V c j) A) (Functor.obj (single V c j) B)
⊢ CategoryTheory.Functor.map (single V c j) (Iso.inv (singleObjXSelf c j A) ≫ f.f j ≫ Iso.hom (singleObjXSelf c j B)) =
    f
have hfg : Hom.f
    (CategoryTheory.Functor.map (single V c j)
      (Iso.inv (singleObjXSelf c j A) ≫ f.f j ≫ Iso.hom (singleObjXSelf c j B)))
    j =
  f.f j
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
⊢ Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k)
    ((if hi : i = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A i hi) else 0) ≫
      d (Functor.obj (single V c j) A) i k)
    (K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hi) else 0)
have dsimp : Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k)
  (CategoryStruct.comp (Y := X.{v, u, u_1} (Functor.obj (single V c j) A) i)
    (if hi : i = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A i hi) else 0) 0)
  (K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hi) else 0)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
⊢ Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k)
    (CategoryStruct.comp (Y := X.{v, u, u_1} (Functor.obj (single V c j) A) i)
      (if hi : i = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A i hi) else 0) 0)
    (K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hi) else 0)
have rw : Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
  (K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hi) else 0)
Tactic: rw [comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
⊢ Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
    (K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hi) else 0)
have pos : ∀ (hk : k = j),
  Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
    (K.d i k ≫ (K.XIsoOfEq hk).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hk))
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
pos :
  ∀ (hk : k = j),
    Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
      (K.d i k ≫ (K.XIsoOfEq hk).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hk))
⊢ Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
    (K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hi) else 0)
have neg : ∀ (hk : ¬k = j), Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0 (K.d i k ≫ 0)
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
hk : k = j
⊢ Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
    (K.d i k ≫ (K.XIsoOfEq hk).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A k hk))
have pos : ∀ (φ : K.X k ⟶ A) (hφ : ∀ (i : ι), c.Rel i k → K.d i k ≫ φ = 0),
  Eq (α := K.X i ⟶ X.{v, u, u_1} (Functor.obj (single V c k) A) k) 0
    (K.d i k ≫ (K.XIsoOfEq sorry).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c k A k sorry))
Tactic: subst hk
Cleared hypotheses: j, φ, hφ, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ Eq (α := K.X j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) j) (Hom.f (mkHomToSingle φ hφ) j)
    (φ ≫ Iso.inv (singleObjXSelf c j A))
have dsimp : Eq (α := K.X j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) j)
  (if hi : j = j then 𝟙 (K.X j) ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A j hi) else 0)
  (φ ≫ Iso.inv (singleObjXSelf c j A))
Tactic: dsimp [mkHomToSingle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ Eq (α := K.X j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) j)
    (if hi : j = j then 𝟙 (K.X j) ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c j A j hi) else 0)
    (φ ≫ Iso.inv (singleObjXSelf c j A))
have rw : Eq (α := K.X j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) j) (φ ≫ Iso.inv (singleObjXIsoOfEq c j A j sorry))
  (φ ≫ Iso.inv (singleObjXSelf c j A))
Tactic: rw [dif_pos rfl, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
    ((if hi : i = j then Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k)
    (d (Functor.obj (single V c j) A) i k ≫
      if hi : k = j then Iso.hom (singleObjXIsoOfEq c j A k hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0)
have dsimp : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
  ((if hi : i = j then Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k)
  (CategoryStruct.comp (Y := X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
    (if hi : k = j then Iso.hom (singleObjXIsoOfEq c j A k hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
    ((if hi : i = j then Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k)
    (CategoryStruct.comp (Y := X.{v, u, u_1} (Functor.obj (single V c j) A) k) 0
      (if hi : k = j then Iso.hom (singleObjXIsoOfEq c j A k hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0))
have rw : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
  ((if hi : i = j then Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k) 0
Tactic: rw [zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
    ((if hi : i = j then Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k) 0
have pos : ∀ (hi : i = j),
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
    ((Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv) ≫ K.d i k) 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
pos :
  ∀ (hi : i = j),
    Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
      ((Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv) ≫ K.d i k) 0
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
    ((if hi : i = j then Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k) 0
have neg : ∀ (hi : ¬i = j), Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k) (0 ≫ K.d i k) 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
hi : i = j
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) i ⟶ K.X k)
    ((Iso.hom (singleObjXIsoOfEq c j A i hi) ≫ φ ≫ (K.XIsoOfEq hi).inv) ≫ K.d i k) 0
have pos : ∀ (φ : A ⟶ K.X i) (hφ : ∀ (k : ι), c.Rel i k → φ ≫ K.d i k = 0),
  Eq (α := X.{v, u, u_1} (Functor.obj (single V c i) A) i ⟶ K.X k)
    ((Iso.hom (singleObjXIsoOfEq c i A i sorry) ≫ φ ≫ (K.XIsoOfEq sorry).inv) ≫ K.d i k) 0
Tactic: subst hi
Cleared hypotheses: j, φ, hφ, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ K.X j) (Hom.f (mkHomFromSingle φ hφ) j)
    (Iso.hom (singleObjXSelf c j A) ≫ φ)
have dsimp : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ K.X j)
  (if hi : j = j then Iso.hom (singleObjXIsoOfEq c j A j hi) ≫ φ ≫ 𝟙 (K.X j) else 0)
  (Iso.hom (singleObjXSelf c j A) ≫ φ)
Tactic: dsimp [mkHomFromSingle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ K.X j)
    (if hi : j = j then Iso.hom (singleObjXIsoOfEq c j A j hi) ≫ φ ≫ 𝟙 (K.X j) else 0)
    (Iso.hom (singleObjXSelf c j A) ≫ φ)
have rw : Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ K.X j) (Iso.hom (singleObjXIsoOfEq c j A j sorry) ≫ φ)
  (Iso.hom (singleObjXSelf c j A) ≫ φ)
Tactic: rw [dif_pos rfl, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
⊢ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (single₀ V) f) 0 = f
have rw : Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A) ≫
    f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B) =
  f
Tactic: rw [HomologicalComplex.single_map_f_self]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
⊢ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A) ≫
      f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B) =
    f
have dsimp : 𝟙 A ≫ f ≫ 𝟙 B = f
Tactic: dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f
have rw : 𝟙 A ≫ f = f
Tactic: rw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
rw : 𝟙 A ≫ f = f
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f
have rw₁ : f = f
Tactic: rw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
φ : C ⟶ Functor.obj (single₀ V) X
⊢ Eq (α := C.X 1 ⟶ X) (CategoryStruct.comp (Y := C.X 0) (C.d 1 0) (φ.f 0) : C.X 1 ⟶ X) (0 : C.X 1 ⟶ X)
have rw : Eq (α := C.X 1 ⟶ X)
  (φ.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ V) X) 1 0 :
    C.X 1 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) 0)
  0
Tactic: rw [← φ.comm 1 0, HomologicalComplex.single_obj_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
φ : C ⟶ Functor.obj (single₀ V) X
rw :
  Eq (α := C.X 1 ⟶ X)
    (φ.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ V) X) 1 0 :
      C.X 1 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) 0)
    0
⊢ Eq (α := C.X 1 ⟶ X) (CategoryStruct.comp (Y := C.X 0) (C.d 1 0) (φ.f 0) : C.X 1 ⟶ X) (0 : C.X 1 ⟶ X)
have rw₁ : Eq (α := C.X 1 ⟶ X) (φ.f 1 ≫ 0) 0
Tactic: rw [← φ.comm 1 0, HomologicalComplex.single_obj_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
φ : C ⟶ Functor.obj (single₀ V) X
rw :
  Eq (α := C.X 1 ⟶ X)
    (φ.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ V) X) 1 0 :
      C.X 1 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) 0)
    0
rw₁ : Eq (α := C.X 1 ⟶ X) (φ.f 1 ≫ 0) 0
⊢ Eq (α := C.X 1 ⟶ X) (CategoryStruct.comp (Y := C.X 0) (C.d 1 0) (φ.f 0) : C.X 1 ⟶ X) (0 : C.X 1 ⟶ X)
have rw₂ : Eq.{v + 1} (α := C.X 1 ⟶ X) 0 0
Tactic: rw [← φ.comm 1 0, HomologicalComplex.single_obj_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : { f : C.X 0 ⟶ X // Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0 }
i : ℕ
hi : (ComplexShape.down ℕ).Rel i 0
⊢ C.d i 0 ≫ (↑f : C.X 0 ⟶ X) = 0
have obtain : ∀ (hi : (ComplexShape.down ℕ).Rel 1 0), Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ (↑f : C.X 0 ⟶ X)) 0
Tactic: obtain rfl : i = 1 := by simpa using hi.symm
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
⊢ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (single₀ V) f) 0 = f
have rw : Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A) ≫
    f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B) =
  f
Tactic: rw [HomologicalComplex.single_map_f_self]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
⊢ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A) ≫
      f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B) =
    f
have dsimp : 𝟙 A ≫ f ≫ 𝟙 B = f
Tactic: dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
φ : Functor.obj (single₀ V) X ⟶ C
⊢ Eq (α := X ⟶ C.X 1) (CategoryStruct.comp (Y := C.X 0) (φ.f 0) (C.d 0 1) : X ⟶ C.X 1) (0 : X ⟶ C.X 1)
have rw : Eq (α := X ⟶ C.X 1)
  (HomologicalComplex.d (Functor.obj (single₀ V) X) 0 1 ≫ φ.f 1 :
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) 0 ⟶ C.X 1)
  0
Tactic: rw [φ.comm 0 1, HomologicalComplex.single_obj_d, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
φ : Functor.obj (single₀ V) X ⟶ C
rw :
  Eq (α := X ⟶ C.X 1)
    (HomologicalComplex.d (Functor.obj (single₀ V) X) 0 1 ≫ φ.f 1 :
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) 0 ⟶ C.X 1)
    0
⊢ Eq (α := X ⟶ C.X 1) (CategoryStruct.comp (Y := C.X 0) (φ.f 0) (C.d 0 1) : X ⟶ C.X 1) (0 : X ⟶ C.X 1)
have rw₁ : Eq (α := X ⟶ C.X 1) (0 ≫ φ.f 1) 0
Tactic: rw [φ.comm 0 1, HomologicalComplex.single_obj_d, zero_comp]