awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Single
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
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
i : ι
pos : ∀ (h : i = j), f.f i = g.f i
neg : ∀ (h : ¬i = j), f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
by_cases h : i = j
-- Module: Mathlib.Algebra.Homology.Single
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
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
i : ι
h : i = j
pos : ∀ {f g : K ⟶ Functor.obj (single V c i) A} (hfg : f.f i = g.f i), f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Single
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
A : V
i : ι
f g : K ⟶ Functor.obj (single V c i) A
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
hfg
-- Module: Mathlib.Algebra.Homology.Single
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
A : V
i : ι
f g : K ⟶ Functor.obj (single V c i) A
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
exact hfg
-- Module: Mathlib.Algebra.Homology.Single
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
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i

Tactic:
apply (isZero_single_obj_X c j A i h).eq_of_tgt

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Single
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)
rw₄ 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)
⊢ f = g

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]

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.single_map_f_self, HomologicalComplex.singleObjXSelf, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.Single
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)
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
⊢ CategoryTheory.Functor.map (single V c j) (Iso.inv (singleObjXSelf c j A) ≫ f.f j ≫ Iso.hom (singleObjXSelf c j B)) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Single
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)
⊢ 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:
simp [single_map_f_self]

Premises used: HomologicalComplex.single_map_f_self
-- Module: Mathlib.Algebra.Homology.Single
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
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Single
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
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)
⊢ 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:
rw [comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Single
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))
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)
⊢ 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:
split_ifs with hk
-- Module: Mathlib.Algebra.Homology.Single
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
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 ⋯).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c k A k ⋯))
⊢ 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:
subst hk
-- Module: Mathlib.Algebra.Homology.Single
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
A : V
i k : ι
hik : c.Rel i k
φ : 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 ⋯).hom ≫ φ ≫ Iso.inv (singleObjXIsoOfEq c k A k ⋯))

Tactic:
simp only [XIsoOfEq_rfl, Iso.refl_hom, id_comp, reassoc_of% hφ i hik, zero_comp]

Premises used: HomologicalComplex.XIsoOfEq_rfl, CategoryTheory.Limits.zero_comp, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Single
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 ≫ 0)

Tactic:
apply (isZero_single_obj_X c j A k hk).eq_of_tgt

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Single
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
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))
⊢ 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))

Tactic:
dsimp [mkHomToSingle]

Premises used: HomologicalComplex.mkHomToSingle
-- Module: Mathlib.Algebra.Homology.Single
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
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 ⋯))
    (φ ≫ Iso.inv (singleObjXSelf c j A))
⊢ 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:
rw [dif_pos rfl, id_comp]

Premises used: dif_pos, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Single
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) (φ ≫ Iso.inv (singleObjXIsoOfEq c j A j ⋯))
    (φ ≫ Iso.inv (singleObjXSelf c j A))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Single
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
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))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Single
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
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
⊢ 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:
rw [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Single
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
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
⊢ 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:
split_ifs with hi
-- Module: Mathlib.Algebra.Homology.Single
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
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 ⋯) ≫ φ ≫ (K.XIsoOfEq ⋯).inv) ≫ K.d i k) 0
⊢ 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:
subst hi
-- Module: Mathlib.Algebra.Homology.Single
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
A : V
i k : ι
hik : c.Rel i k
φ : 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 ⋯) ≫ φ ≫ (K.XIsoOfEq ⋯).inv) ≫ K.d i k) 0

Tactic:
simp only [XIsoOfEq_rfl, Iso.refl_inv, comp_id, assoc, hφ k hik, comp_zero]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.XIsoOfEq_rfl, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv
-- Module: Mathlib.Algebra.Homology.Single
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) (0 ≫ K.d i k) 0

Tactic:
apply (isZero_single_obj_X c j A i hi).eq_of_src

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Single
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
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) ≫ φ)
⊢ 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) ≫ φ)

Tactic:
dsimp [mkHomFromSingle]

Premises used: HomologicalComplex.mkHomFromSingle
-- Module: Mathlib.Algebra.Homology.Single
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
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 ⋯) ≫ φ)
    (Iso.hom (singleObjXSelf c j A) ≫ φ)
⊢ 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:
rw [dif_pos rfl, comp_id]

Premises used: dif_pos, CategoryTheory.Category.comp_id, rfl
-- Module: Mathlib.Algebra.Homology.Single
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) (Iso.hom (singleObjXIsoOfEq c j A j ⋯) ≫ φ)
    (Iso.hom (singleObjXSelf c j A) ≫ φ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A : V
⊢ HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) A) 0 = A

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Algebra.Homology.Single
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 :
  Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A) ≫
      f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B) =
    f
⊢ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (single₀ V) f) 0 = f

Tactic:
rw [HomologicalComplex.single_map_f_self]

Premises used: HomologicalComplex.single_map_f_self
-- Module: Mathlib.Algebra.Homology.Single
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
dsimp : 𝟙 A ≫ f ≫ 𝟙 B = f
⊢ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A) ≫
      f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B) =
    f

Tactic:
dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]

Premises used: HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.singleObjXSelf
-- Module: Mathlib.Algebra.Homology.Single
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
rw₁ rw₂ : f = f
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f

Tactic:
rw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
X : V
⊢ HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X =
    Iso.refl (HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single V (ComplexShape.down ℕ) 0) X) 0)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.singleObjXSelf, rfl, ite
-- Module: Mathlib.Algebra.Homology.Single
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
rw₂ rw₃ : Eq.{v + 1} (α := C.X 1 ⟶ 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)

Tactic:
rw [← φ.comm 1 0, HomologicalComplex.single_obj_d, comp_zero]

Premises used: HomologicalComplex.single_obj_d, CategoryTheory.Limits.comp_zero, OfNat.ofNat, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.Single
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
⊢ i = 1

Tactic:
simpa using hi.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Homology.Single
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
obtain : ∀ (hi : (ComplexShape.down ℕ).Rel 1 0), Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ (↑f : C.X 0 ⟶ X)) 0
⊢ C.d i 0 ≫ (↑f : C.X 0 ⟶ X) = 0

Tactic:
obtain rfl : i = 1 := by simpa using hi.symm

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Single
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 }
hi : (ComplexShape.down ℕ).Rel 1 0
⊢ Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ (↑f : C.X 0 ⟶ X)) 0

Tactic:
f.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Homology.Single
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 }
hi : (ComplexShape.down ℕ).Rel 1 0
⊢ Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ (↑f : C.X 0 ⟶ X)) 0

Tactic:
exact f.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Homology.Single
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 }
⊢ (fun (φ : C ⟶ Functor.obj (single₀ V) X) ↦
        (Subtype.mk (p := fun (f : C.X 0 ⟶ X) ↦ Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0) (φ.f 0) ⋯ :
          { f : C.X 0 ⟶ X // Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0 }))
      ((fun (f : { f : C.X 0 ⟶ X // Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0 }) ↦
          (HomologicalComplex.mkHomToSingle (↑f : C.X 0 ⟶ X) ⋯ :
            C ⟶ Functor.obj (HomologicalComplex.single V (ComplexShape.down ℕ) 0) X))
        f) =
    f

Tactic:
simp