awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
inst_3 : One α
ha : Ne.{u_2 + 1} (α := α) 1 0
⊢ (up α).HasNoLoop

Tactic:
hasNoLoop_up' _ ha

Premises used: ComplexShape.hasNoLoop_up', ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
inst_3 : One α
ha : Ne.{u_2 + 1} (α := α) 1 0
⊢ (down α).HasNoLoop

Tactic:
hasNoLoop_down' _ ha

Premises used: ComplexShape.hasNoLoop_down', ComplexShape.down
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
⊢ Ne (α := ℤ) 1 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
⊢ Ne (α := ℕ) 1 0

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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
i₁ : I₁
i₂ : I₂
⊢ toGradedObjectMap φ (i₁, i₂) = (φ.f i₁).f i₂

Tactic:
rfl

Premises used: HomologicalComplex₂.toGradedObjectMap, 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₂
x x_1 : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ₁ φ₂ : x ⟶ x_1
h :
  Eq (α := Functor.obj (toGradedObjectFunctor C c₁ c₂) x ⟶ Functor.obj (toGradedObjectFunctor C c₁ c₂) x_1)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₁)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₂)
h₁ : ∀ (i₁ : I₁) (i₂ : I₂), (φ₁.f i₁).f i₂ = (φ₂.f i₁).f i₂
⊢ φ₁ = φ₂

Tactic:
ext i₁ i₂
-- 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₂
x x_1 : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ₁ φ₂ : x ⟶ x_1
h :
  Eq (α := Functor.obj (toGradedObjectFunctor C c₁ c₂) x ⟶ Functor.obj (toGradedObjectFunctor C c₁ c₂) x_1)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₁)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₂)
i₁ : I₁
i₂ : I₂
⊢ (φ₁.f i₁).f i₂ = (φ₂.f i₁).f i₂

Tactic:
congr_fun h ⟨i₁, i₂⟩

Premises used: HomologicalComplex₂.toGradedObject, HomologicalComplex₂.toGradedObjectMap, Prod.mk, congr_fun
-- 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₂
x x_1 : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ₁ φ₂ : x ⟶ x_1
h :
  Eq (α := Functor.obj (toGradedObjectFunctor C c₁ c₂) x ⟶ Functor.obj (toGradedObjectFunctor C c₁ c₂) x_1)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₁)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₂)
i₁ : I₁
i₂ : I₂
⊢ (φ₁.f i₁).f i₂ = (φ₂.f i₁).f i₂

Tactic:
exact congr_fun h ⟨i₁, i₂⟩

Premises used: Prod.mk, congr_fun
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ : I₁
i j k : I₂
h : c₂.Rel i j
h_1 : c₂.Rel j k
⊢ d₂ i₁ i j ≫ d₂ i₁ j k = 0

Tactic:
apply d₂_comp_d₂
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
i j : I₂
h : c₂.Rel i j
⊢ d₁ i₁ i₁' i ≫
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.d
        i j =
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.d
        i j ≫
      d₁ i₁ i₁' j

Tactic:
apply comm
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
h₁ :
  ∀ (i₂ : I₂),
    Eq.{v_1 + 1} (α :=
      { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
          i₂ ⟶
        { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
          i₂)
      (Hom.f { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } i₂) (Hom.f 0 i₂)
⊢ Eq (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v_1, u_1, u_3} C c₂ } ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } 0

Tactic:
ext i₂
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ Eq.{v_1 + 1} (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂ ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂)
    (Hom.f { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } i₂) (Hom.f 0 i₂)

Tactic:
shape₁ i₁ i₁' h i₂
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ Eq.{v_1 + 1} (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂ ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂)
    (Hom.f { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } i₂) (Hom.f 0 i₂)

Tactic:
exact shape₁ i₁ i₁' h i₂
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
h_1 : c₁.Rel i₁ i₁'
h_2 : c₁.Rel i₁' i₁''
h :
  ∀ (i₂ : I₂),
    Eq.{v_1 + 1} (α :=
      { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
          i₂ ⟶
        { X := fun (i₂ : I₂) ↦ X (i₁'', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁'' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
          i₂)
      (Hom.f
        (CategoryStruct.comp (Y :=
          { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
          { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } { f := fun (i₂ : I₂) ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ })
        i₂)
      (Hom.f 0 i₂)
⊢ Eq (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v_1, u_1, u_3} C c₂ } ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁'', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁'' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
    (CategoryStruct.comp (Y :=
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
      { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } { f := fun (i₂ : I₂) ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ })
    0

Tactic:
ext i₂
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
h : c₁.Rel i₁ i₁'
h_1 : c₁.Rel i₁' i₁''
i₂ : I₂
⊢ Eq.{v_1 + 1} (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂ ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁'', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁'' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂)
    (Hom.f
      (CategoryStruct.comp (Y :=
        { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
        { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } { f := fun (i₂ : I₂) ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ })
      i₂)
    (Hom.f 0 i₂)

Tactic:
apply d₁_comp_d₁
-- 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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
⊢ (ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X

Tactic:
rfl

Premises used: HomologicalComplex₂.toGradedObject, 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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ :
  ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁').X i₂) (f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂)
        ((K.d i₁ i₁').f i₂ ≫ f (i₁', i₂))
comm₂ :
  ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁).X i₂') (f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂')
        ((K.X i₁).d i₂ i₂' ≫ f (i₁, i₂'))
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
h :
  ∀ (i₂ : I₂),
    Hom.f ({ f := fun (i₂ : I₂) ↦ f (i₁, i₂), comm' := ⋯ : (K.X i₁).Hom (L.X i₁) } ≫ L.d i₁ i₁') i₂ =
      (K.d i₁ i₁' ≫ { f := fun (i₂ : I₂) ↦ f (i₁', i₂), comm' := ⋯ : (K.X i₁').Hom (L.X i₁') }).f i₂
⊢ { f := fun (i₂ : I₂) ↦ f (i₁, i₂), comm' := ⋯ : (K.X i₁).Hom (L.X i₁) } ≫ L.d i₁ i₁' =
    K.d i₁ i₁' ≫ { f := fun (i₂ : I₂) ↦ f (i₁', i₂), comm' := ⋯ : (K.X i₁').Hom (L.X i₁') }

Tactic:
ext i₂
-- 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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ :
  ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁').X i₂) (f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂)
        ((K.d i₁ i₁').f i₂ ≫ f (i₁', i₂))
comm₂ :
  ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁).X i₂') (f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂')
        ((K.X i₁).d i₂ i₂' ≫ f (i₁, i₂'))
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ Hom.f ({ f := fun (i₂ : I₂) ↦ f (i₁, i₂), comm' := ⋯ : (K.X i₁).Hom (L.X i₁) } ≫ L.d i₁ i₁') i₂ =
    (K.d i₁ i₁' ≫ { f := fun (i₂ : I₂) ↦ f (i₁', i₂), comm' := ⋯ : (K.X i₁').Hom (L.X i₁') }).f i₂

Tactic:
comm₁ i₁ i₁' i₂ h₁

Premises used: HomologicalComplex₂.toGradedObject
-- 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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ :
  ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁').X i₂) (f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂)
        ((K.d i₁ i₁').f i₂ ≫ f (i₁', i₂))
comm₂ :
  ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁).X i₂') (f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂')
        ((K.X i₁).d i₂ i₂' ≫ f (i₁, i₂'))
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ Hom.f ({ f := fun (i₂ : I₂) ↦ f (i₁, i₂), comm' := ⋯ : (K.X i₁).Hom (L.X i₁) } ≫ L.d i₁ i₁') i₂ =
    (K.d i₁ i₁' ≫ { f := fun (i₂ : I₂) ↦ f (i₁', i₂), comm' := ⋯ : (K.X i₁').Hom (L.X i₁') }).f i₂

Tactic:
exact comm₁ i₁ i₁' i₂ 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₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
rw : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁').X i₂) (Hom.f 0 i₂) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁').X i₂) 0 0
⊢ (K.d i₁ i₁').f i₂ = 0

Tactic:
rw [K.shape _ _ h, zero_f]

Premises used: HomologicalComplex.zero_f, HomologicalComplex.shape
-- 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₁
i₂ : I₂
rw : (K.d i₁ i₁' ≫ K.d i₁' i₁'').f i₂ = 0
rw₁ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁'').X i₂) (Hom.f 0 i₂) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁'').X i₂) 0 0
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0

Tactic:
rw [← comp_f, d_comp_d, zero_f]

Premises used: HomologicalComplex.comp_f, HomologicalComplex.zero_f, HomologicalComplex.d_comp_d
-- 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₂ i₂' : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂'

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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K ⟶ L
i₁ i₁' : I₁
i₂ : I₂
⊢ (f.f i₁).f i₂ ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ (f.f i₁').f i₂

Tactic:
congr_hom (f.comm i₁ i₁') i₂

Premises used: HomologicalComplex.congr_hom, HomologicalComplex.Hom.comm
-- 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₂
w : ¬c₂.Rel i i'
h :
  ∀ (j : I₁),
    Eq.{v_1 + 1} (α :=
      { X := fun (j : I₁) ↦ (K.X j).X i, d := fun (j j' : I₁) ↦ (K.d j j').f i, shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
          j ⟶
        { X := fun (j : I₁) ↦ (K.X j).X i', d := fun (j j' : I₁) ↦ (K.d j j').f i', shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
          j)
      (Hom.f { f := fun (j : I₁) ↦ (K.X j).d i i', comm' := ⋯ } j) (Hom.f 0 j)
⊢ Eq (α :=
    { X := fun (j : I₁) ↦ (K.X j).X i, d := fun (j j' : I₁) ↦ (K.d j j').f i, shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v_1, u_1, u_2} C c₁ } ⟶
      { X := fun (j : I₁) ↦ (K.X j).X i', d := fun (j j' : I₁) ↦ (K.d j j').f i', shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (j : I₁) ↦ (K.X j).d i i', comm' := ⋯ } 0

Tactic:
ext j
-- 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₂
w : ¬c₂.Rel i i'
j : I₁
⊢ Eq.{v_1 + 1} (α :=
    { X := fun (j : I₁) ↦ (K.X j).X i, d := fun (j j' : I₁) ↦ (K.d j j').f i, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
        j ⟶
      { X := fun (j : I₁) ↦ (K.X j).X i', d := fun (j j' : I₁) ↦ (K.d j j').f i', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
        j)
    (Hom.f { f := fun (j : I₁) ↦ (K.X j).d i i', comm' := ⋯ } j) (Hom.f 0 j)

Tactic:
(K.X j).shape i i' w

Premises used: HomologicalComplex.X, HomologicalComplex.shape
-- 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₂
w : ¬c₂.Rel i i'
j : I₁
⊢ Eq.{v_1 + 1} (α :=
    { X := fun (j : I₁) ↦ (K.X j).X i, d := fun (j j' : I₁) ↦ (K.d j j').f i, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
        j ⟶
      { X := fun (j : I₁) ↦ (K.X j).X i', d := fun (j j' : I₁) ↦ (K.d j j').f i', shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
        j)
    (Hom.f { f := fun (j : I₁) ↦ (K.X j).d i i', comm' := ⋯ } j) (Hom.f 0 j)

Tactic:
exact (K.X j).shape i i' w

Premises used: HomologicalComplex.X, HomologicalComplex.shape
-- 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₂
⊢ K.flip.flip = K

Tactic:
rfl

Premises used: HomologicalComplex₂.flip, 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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K ⟶ L
i : I₂
i_1 j : I₁
h : c₁.Rel i_1 j
⊢ (f.f i_1).f i ≫ (L.flip.X i).d i_1 j = (K.flip.X i).d i_1 j ≫ (f.f j).f i

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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K ⟶ L
i j : I₂
h_1 : c₂.Rel i j
h :
  ∀ (i_1 : I₁),
    Hom.f ({ f := fun (j : I₁) ↦ (f.f j).f i, comm' := ⋯ } ≫ L.flip.d i j) i_1 =
      Hom.f (K.flip.d i j ≫ { f := fun (j_1 : I₁) ↦ (f.f j_1).f j, comm' := ⋯ : (K.flip.X j).Hom (L.flip.X j) }) i_1
⊢ { f := fun (j : I₁) ↦ (f.f j).f i, comm' := ⋯ } ≫ L.flip.d i j =
    K.flip.d i j ≫ { f := fun (j_1 : I₁) ↦ (f.f j_1).f j, comm' := ⋯ : (K.flip.X j).Hom (L.flip.X j) }

Tactic:
ext
-- 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 L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K ⟶ L
i j : I₂
h : c₂.Rel i j
i_1 : I₁
⊢ Hom.f ({ f := fun (j : I₁) ↦ (f.f j).f i, comm' := ⋯ } ≫ L.flip.d i j) i_1 =
    Hom.f (K.flip.d i j ≫ { f := fun (j_1 : I₁) ↦ (f.f j_1).f j, comm' := ⋯ : (K.flip.X j).Hom (L.flip.X j) }) i_1

Tactic:
simp