awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
obtain : ∀ (r : c.Rel i (c.next i)), C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv
⊢ C.dFrom i = C.d i j ≫ (C.xNextIso r).inv

Tactic:
obtain rfl := c.next_eq' r

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
r : c.Rel i (c.next i)
⊢ C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv

Tactic:
(Category.comp_id _).symm

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
r : c.Rel i (c.next i)
⊢ C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
⊢ (C.xPrevIso r).inv ≫ C.dTo j = C.d i j

Tactic:
simp [C.dTo_eq r]

Premises used: HomologicalComplex.dTo_eq
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ (C.xPrevIsoSelf h).inv ≫ C.dTo j = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i ≫ (C.xNextIso r).hom = C.d i j

Tactic:
simp [C.dFrom_eq r]

Premises used: HomologicalComplex.dFrom_eq
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i ≫ (C.xNextIsoSelf h).hom = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
⊢ C.dTo j ≫ C.dFrom j = 0

Tactic:
C.d_comp_d _ _ _

Premises used: HomologicalComplex.d_comp_d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasKernels.{v, u} V
i j : ι
r : c.Rel i j
rw : kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)
⊢ kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)

Tactic:
rw [C.dFrom_eq r]

Premises used: HomologicalComplex.dFrom_eq
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasKernels.{v, u} V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)

Tactic:
apply kernelSubobject_comp_mono

Premises used: CategoryTheory.Limits.kernelSubobject_comp_mono
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasImages.{v, u} V
inst_3 : HasEqualizers.{v, u} V
i j : ι
r : c.Rel i j
rw : imageSubobject ((C.xPrevIso r).hom ≫ C.d i j) = imageSubobject (C.d i j)
⊢ imageSubobject (C.dTo j) = imageSubobject (C.d i j)

Tactic:
rw [C.dTo_eq r]

Premises used: HomologicalComplex.dTo_eq
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasImages.{v, u} V
inst_3 : HasEqualizers.{v, u} V
i j : ι
r : c.Rel i j
⊢ imageSubobject ((C.xPrevIso r).hom ≫ C.d i j) = imageSubobject (C.d i j)

Tactic:
apply imageSubobject_iso_comp

Premises used: CategoryTheory.Limits.imageSubobject_iso_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ C₁.d i j = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
rw rw₁ : (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv
⊢ (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv

Tactic:
rw [hf i j hij]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv = C₂.d i j ≫ (f j).inv

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
h :
  ∀ (i : ι),
    Hom.f ({ f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } ≫ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ }) i =
      Hom.f (𝟙 C₁) i
⊢ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } ≫ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } = 𝟙 C₁

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ Hom.f ({ f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } ≫ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ }) i =
    Hom.f (𝟙 C₁) i

Tactic:
(f i).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ Hom.f ({ f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } ≫ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ }) i =
    Hom.f (𝟙 C₁) i

Tactic:
exact (f i).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
h :
  ∀ (i : ι),
    Hom.f ({ f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ }) i =
      Hom.f (𝟙 C₂) i
⊢ { f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ } = 𝟙 C₂

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ Hom.f ({ f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ }) i =
    Hom.f (𝟙 C₂) i

Tactic:
(f i).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ Hom.f ({ f := fun (i : ι) ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun (i : ι) ↦ (f i).hom, comm' := hf : C₁.Hom C₂ }) i =
    Hom.f (𝟙 C₂) i

Tactic:
exact (f i).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
w : (isoApp (isoOfComponents f hf) i).hom = (f i).hom
⊢ isoApp (isoOfComponents f hf) i = f i

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f hf) i).hom = (f i).hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : ∀ (n : ι), IsIso (f.f n)
⊢ IsIso f

Tactic:
(HomologicalComplex.Hom.isoOfComponents fun n => asIso (f.f n)).isIso_hom

Premises used: HomologicalComplex.Hom.f, HomologicalComplex.Hom.isoOfComponents, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
obtain : ∀ (w : c.Rel (c.prev j) j), f.prev j = (C₁.xPrevIso w).hom ≫ f.f (c.prev j) ≫ (C₂.xPrevIso w).inv
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv

Tactic:
obtain rfl := c.prev_eq' w

Premises used: ComplexShape.prev_eq', rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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₂
j : ι
w : c.Rel (c.prev j) j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f (c.prev j) ≫ (C₂.xPrevIso w).inv

Tactic:
simp only [xPrevIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.eqToIso_refl, CategoryTheory.Iso.refl_inv, HomologicalComplex.xPrevIso, CategoryTheory.Iso.refl_hom, 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
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
obtain : ∀ (w : c.Rel i (c.next i)), f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv

Tactic:
obtain rfl := c.next_eq' w

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : ι
w : c.Rel i (c.next i)
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv

Tactic:
simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Premises used: HomologicalComplex.xNextIso, CategoryTheory.Category.comp_id, CategoryTheory.eqToIso_refl, CategoryTheory.Iso.refl_inv, CategoryTheory.Iso.refl_hom, 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
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
f : C₁.Hom C₂
i : ι
⊢ f.f i ≫ C₂.dFrom i = C₁.dFrom i ≫ f.next i

Tactic:
f.comm _ _

Premises used: HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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₂
j : ι
⊢ f.prev j ≫ C₂.dTo j = C₁.dTo j ≫ f.f j

Tactic:
f.comm _ _

Premises used: HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : ι
⊢ Arrow.Hom.left (f.sqFrom i) = f.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : ι
⊢ Arrow.Hom.right (f.sqFrom i) = f.next i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ : HomologicalComplex.{v, u, u_1} V c
i : ι
⊢ sqFrom (𝟙 C₁) i = 𝟙 (Arrow.mk (C₁.dFrom i))

Tactic:
rfl

Premises used: rfl, CategoryTheory.Arrow.homMk, HomologicalComplex.Hom.sqFrom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ sqFrom (f ≫ g) i = sqFrom f i ≫ sqFrom g i

Tactic:
rfl

Premises used: rfl, CategoryTheory.Arrow.homMk, HomologicalComplex.Hom.sqFrom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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₂
j : ι
⊢ Arrow.Hom.left (f.sqTo j) = f.prev j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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₂
j : ι
⊢ Arrow.Hom.right (f.sqTo j) = f.f j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : C₁ ⟶ C₂
inst_2 : IsIso f
j : ι
⊢ IsIso (f.f j)

Tactic:
inferInstanceAs (IsIso ((eval _ _ j).map f))

Premises used: _private.0.HomologicalComplex.Hom.instIsIsoF._proof_1
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : C₁ ⟶ C₂
inst_2 : IsSplitEpi f
j : ι
⊢ IsSplitEpi (f.f j)

Tactic:
inferInstanceAs (IsSplitEpi ((eval _ _ j).map f))

Premises used: _private.0.HomologicalComplex.Hom.instIsSplitEpiF._proof_1
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : C₁ ⟶ C₂
inst_2 : IsSplitMono f
j : ι
⊢ IsSplitMono (f.f j)

Tactic:
inferInstanceAs (IsSplitMono ((eval _ _ j).map f))

Premises used: _private.0.HomologicalComplex.Hom.instIsSplitMonoF._proof_1
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 : ι
hom_inv_id : (inv f).f j ≫ f.f j = 𝟙 (C₂.X j)
⊢ (inv f).f j = inv (f.f j)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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 ≫ f.f j = 𝟙 (C₂.X j)

Tactic:
simp [← comp_f]

Premises used: HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
rw rw₁ : X (j + 1) = X (j + 1)
⊢ X i = X (j + 1)

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
α : 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 : α
w : ¬(ComplexShape.down α).Rel i j
⊢ of.d X d i j = 0

Tactic:
simp [of.d, (Ne.symm w)]

Premises used: Ne.symm, ChainComplex.of.d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
dsimp :
  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
⊢ of.d X d i j ≫ of.d X d j k = 0

Tactic:
dsimp [of.d] at hij hjk ⊢

Premises used: ChainComplex.of.d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
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 ⋯ ≫ d (k + 1) else 0)
      (if h : k + 1 = k + 1 then eqToHom ⋯ ≫ d k else 0))
    0
⊢ 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

Tactic:
substs hij hjk
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
k : α
⊢ 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 ⋯ ≫ d (k + 1) else 0)
      (if h : k + 1 = k + 1 then eqToHom ⋯ ≫ d k else 0))
    0

Tactic:
simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq]

Premises used: CategoryTheory.eqToHom_refl, ite_true, dite_eq_ite, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ (of X d sq).X = 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
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
dsimp : (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
⊢ of.d X d (j + 1) j = d j

Tactic:
dsimp [of.d]

Premises used: ChainComplex.of.d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
rw₁ rw₂ : d j = d j
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j

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
α : 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
⊢ of.d X d i j = 0

Tactic:
simp [of.d, dif_neg h]

Premises used: dif_neg, ChainComplex.of.d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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_1 : α → V
d_X : (n : α) → X_1 (n + 1) ⟶ X_1 n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y_1 : α → V
d_Y : (n : α) → Y_1 (n + 1) ⟶ Y_1 n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex.{v, u, u_2} V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), Eq (α := X.X (i + 1) ⟶ Y.X i) (f (i + 1) ≫ Y.d (i + 1) i) (X.d (i + 1) i ≫ f i)
m : α
⊢ Eq (α := X.X (m + 1) ⟶ Y.X m) (f (m + 1) ≫ Y.d (m + 1) m) (X.d (m + 1) m ≫ f m)

Tactic:
simpa using comm m
-- 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
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X 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₁ 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).X 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₁ 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).X 2 = X₂

Tactic:
rfl

Premises used: rfl