awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalBicomplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ : I₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      Iso.hom
            ((fun (x : I₂) ↦
                (Iso.refl (((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).X x) :
                  ((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).X x ≅
                    ((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).X x))
              i) ≫
          ((Functor.obj (flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁) K).X i₁).d i j =
        ((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).d i j ≫
          Iso.hom
            ((fun (x : I₂) ↦
                (Iso.refl (((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).X x) :
                  ((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).X x ≅
                    ((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂)) K).X i₁).X x))
              j)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalBicomplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_3, u_2} C c₂ c₁
i₂ : I₂
⊢ ∀ (i j : I₁),
    c₁.Rel i j →
      Iso.hom
            ((fun (x : I₁) ↦
                (Iso.refl (((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).X x) :
                  ((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).X x ≅
                    ((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).X x))
              i) ≫
          ((Functor.obj (𝟭 (HomologicalComplex₂.{v_1, u_1, u_3, u_2} C c₂ c₁)) K).X i₂).d i j =
        ((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).d i j ≫
          Iso.hom
            ((fun (x : I₁) ↦
                (Iso.refl (((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).X x) :
                  ((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).X x ≅
                    ((Functor.obj (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂) K).X i₂).X x))
              j)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalBicomplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
subst : (K.X x₁).X x₂ = (K.X x₁).X x₂
⊢ (K.X x₁).X x₂ = (K.X y₁).X y₂

Tactic:
subst h₁ h₂
-- Module: Mathlib.Algebra.Homology.HomologicalBicomplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
x₁ : I₁
x₂ : I₂
⊢ (K.X x₁).X x₂ = (K.X x₁).X x₂

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomologicalBicomplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ : I₁
i₂ : I₂
⊢ XXIsoOfEq C c₁ c₂ K ⋯ ⋯ = Iso.refl ((K.X i₁).X i₂)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, HomologicalComplex₂.XXIsoOfEq, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, 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 j k : ι
pos : ∀ (hij : c.Rel i j), C.d i j ≫ C.d j k = 0
neg : ∀ (hij : ¬c.Rel i j), C.d i j ≫ C.d j k = 0
⊢ C.d i j ≫ C.d j k = 0

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- 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 k : ι
hij : c.Rel i j
pos : ∀ (hjk : c.Rel j k), C.d i j ≫ C.d j k = 0
neg : ∀ (hjk : ¬c.Rel j k), C.d i j ≫ C.d j k = 0
⊢ C.d i j ≫ C.d j k = 0

Tactic:
by_cases hjk : c.Rel j k

Premises used: ComplexShape.Rel
-- 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 k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
C.d_comp_d' i j k hij hjk

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
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
exact C.d_comp_d' i j k hij hjk

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
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
neg : Eq (α := C.X i ⟶ C.X k) (C.d i j ≫ 0) 0
neg₁ neg₂ : Eq.{v + 1} (α := C.X i ⟶ C.X k) 0 0
⊢ C.d i j ≫ C.d j k = 0

Tactic:
rw [C.shape j k hjk, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- 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 k : ι
hij : ¬c.Rel i j
neg : Eq (α := C.X i ⟶ C.X k) (0 ≫ C.d j k) 0
neg₁ neg₂ : Eq.{v + 1} (α := C.X i ⟶ C.X k) 0 0
⊢ C.d i j ≫ C.d j k = 0

Tactic:
rw [C.shape i j hij, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- 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
h_X : C₁.X = C₂.X
h_d : ∀ (i j : ι), c.Rel i j → C₁.d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ C₂.d i j
obtain :
  ∀ (X₁ : ι → V) (d₁ : (i j : ι) → X₁ i ⟶ X₁ j) (s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0)
    (h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0)
    (h_X : { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.X = C₂.X)
    (h_d :
      ∀ (i j : ι),
        c.Rel i j →
          { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
            eqToHom ⋯ ≫ C₂.d i j),
    { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } = C₂
⊢ C₁ = C₂

Tactic:
obtain ⟨X₁, d₁, s₁, h₁⟩ := C₁
-- 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
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
h_X : { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.X = C₂.X
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ C₂.d i j
obtain :
  ∀ (X₂ : ι → V) (d₂ : (i j : ι) → X₂ i ⟶ X₂ j) (s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0)
    (h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0)
    (h_X :
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.X =
        { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.X)
    (h_d :
      ∀ (i j : ι),
        c.Rel i j →
          { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
            eqToHom ⋯ ≫ { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j),
    { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
      { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ }
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } = C₂

Tactic:
obtain ⟨X₂, d₂, s₂, h₂⟩ := C₂
-- 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
X₂ : ι → V
d₂ : (i j : ι) → X₂ i ⟶ X₂ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_X : X₁ = X₂
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
subst :
  ∀ (d₂ : (i j : ι) → X₁ i ⟶ X₁ j) (s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0)
    (h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0)
    (h_d :
      ∀ (i j : ι),
        c.Rel i j →
          { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
            eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j),
    { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
      { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
    { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ }

Tactic:
subst h_X
-- 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
simp : d₁ = d₂
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
    { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }

Tactic:
simp only [mk.injEq, heq_eq_eq, true_and]

Premises used: heq_eq_eq, HomologicalComplex.mk.injEq, true_and
-- 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
h : ∀ (i j : ι), d₁ i j = d₂ i j
⊢ d₁ = d₂

Tactic:
ext i j
-- 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
pos : ∀ (hij : c.Rel i j), d₁ i j = d₂ i j
neg : ∀ (hij : ¬c.Rel i j), d₁ i j = d₂ i j
⊢ d₁ i j = d₂ i j

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
hij : c.Rel i j
⊢ d₁ i j = d₂ i j

Tactic:
simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
hij : ¬c.Rel i j
neg : 0 = d₂ i j
neg₁ neg₂ : Eq.{v + 1} (α := X₁ i ⟶ X₁ j) 0 0
⊢ d₁ i j = d₂ i j

Tactic:
rw [s₁ i j hij, s₂ 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p q : ι
h : p = q
rw rw₁ : K.X q = K.X q
⊢ K.X p = K.X q

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
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p : ι
⊢ K.XIsoOfEq ⋯ = Iso.refl (K.X p)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, HomologicalComplex.XIsoOfEq, 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)
⊢ (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Premises used: HomologicalComplex.XIsoOfEq
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp only [eqToHom_trans]

Premises used: CategoryTheory.eqToHom_trans
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)
⊢ (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Premises used: HomologicalComplex.XIsoOfEq
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp only [eqToHom_trans]

Premises used: CategoryTheory.eqToHom_trans
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)
⊢ (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Premises used: HomologicalComplex.XIsoOfEq
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp only [eqToHom_trans]

Premises used: CategoryTheory.eqToHom_trans
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
dsimp : Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)
⊢ (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Premises used: HomologicalComplex.XIsoOfEq
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ Eq.{v + 1} (α := K.X p₁ ⟶ K.X p₃) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp only [eqToHom_trans]

Premises used: CategoryTheory.eqToHom_trans
-- 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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
subst : (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃
⊢ (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₁ p₃ : ι
⊢ (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃

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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
subst : (K.XIsoOfEq ⋯).inv ≫ K.d p₂ p₃ = K.d p₂ p₃
⊢ (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₃ : ι
⊢ (K.XIsoOfEq ⋯).inv ≫ K.d p₂ p₃ = K.d p₂ p₃

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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
subst : K.d p₁ p₂ ≫ (K.XIsoOfEq ⋯).hom = K.d p₁ p₂
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq ⋯).hom = K.d p₁ p₂

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 ι
K : HomologicalComplex.{v, u, u_1} V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
subst : K.d p₁ p₃ ≫ (K.XIsoOfEq ⋯).inv = K.d p₁ p₃
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
p₃ p₁ : ι
⊢ K.d p₁ p₃ ≫ (K.XIsoOfEq ⋯).inv = K.d p₁ p₃

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
α : Type u_2
inst : AddRightCancelSemigroup α
inst_1 : One α
i : α
⊢ (ComplexShape.down α).prev i = i + 1

Tactic:
(ComplexShape.down α).prev_eq' rfl

Premises used: ComplexShape.prev_eq', ComplexShape.down, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
α : Type u_2
inst : AddGroup α
inst_1 : One α
i : α
⊢ (ComplexShape.down α).next i = i - 1

Tactic:
(ComplexShape.down α).next_eq' <| sub_add_cancel _ _

Premises used: ComplexShape.down, sub_add_cancel, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
dif_neg ?_

Premises used: dif_neg, ComplexShape.next
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
refine : ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
refine dif_neg ?_

Premises used: dif_neg
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
push : ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j
⊢ ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
j : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel 0 j

Tactic:
apply Nat.noConfusion

Premises used: Nat.noConfusion
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
refine : ¬∃ (j : ℕ), (ComplexShape.down ℕ).Rel 0 j
refine₁ refine₂ : ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
classical
    refine dif_neg ?_
    push Not
    intro
    apply Nat.noConfusion

Premises used: dif_neg, Not, Nat.noConfusion
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
i : ℕ
⊢ (ComplexShape.down ℕ).next (i + 1) = i

Tactic:
(ComplexShape.down ℕ).next_eq' rfl

Premises used: Nat, ComplexShape.down, rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
α : Type u_2
inst : AddGroup α
inst_1 : One α
i : α
⊢ (ComplexShape.up α).prev i = i - 1

Tactic:
(ComplexShape.up α).prev_eq' <| sub_add_cancel _ _

Premises used: ComplexShape.prev_eq', sub_add_cancel, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
α : Type u_2
inst : AddRightCancelSemigroup α
inst_1 : One α
i : α
⊢ (ComplexShape.up α).next i = i + 1

Tactic:
(ComplexShape.up α).next_eq' rfl

Premises used: rfl, ComplexShape.up, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
dif_neg ?_

Premises used: ComplexShape.prev, dif_neg
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
refine : ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
refine dif_neg ?_

Premises used: dif_neg
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
push : ∀ (j : ℕ), ¬(ComplexShape.up ℕ).Rel j 0
⊢ ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
j : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel j 0

Tactic:
apply Nat.noConfusion

Premises used: Nat.noConfusion