awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
simp : p < 0
⊢ WithBotTop.coe (coreE₂Cohomological.deg (p, q)) < coreE₂Cohomological.i₁ (p, q)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
⊢ p < 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
h :
  IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE ⋯)))
⊢ IsZero.{v_1, u_1} ((Y.E₂SpectralSequence.page r ⋯).X (p, q))

Tactic:
apply isZero_spectralSequence_page_X_of_isZero_H' _ _ _ hr

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H'
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
h : WithBotTop.coe 0 < coreE₂Cohomological.i₁ (p, q)
⊢ IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE ⋯)))

Tactic:
apply Y.isZero₁_of_isThirdQuadrant

Premises used: CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
h : 0 < q
⊢ WithBotTop.coe 0 < coreE₂Cohomological.i₁ (p, q)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ 0 < q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
h :
  IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE ⋯)))
⊢ IsZero.{v_1, u_1} ((Y.E₂SpectralSequence.page r ⋯).X (p, q))

Tactic:
apply isZero_spectralSequence_page_X_of_isZero_H' _ _ _ hr

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H'
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
h : coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe (coreE₂Cohomological.deg (p, q))
⊢ IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE ⋯)))

Tactic:
apply Y.isZero₂_of_isThirdQuadrant

Premises used: CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
h : q + 1 ≤ p + q
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe (coreE₂Cohomological.deg (p, q))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ q + 1 ≤ p + q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.Basic
Goal:
C : Type u_1
inst : Category.{u_3, u_1} C
inst_1 : Abelian.{u_3, u_1} C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E : SpectralSequence.{u_1, u_2, u_3} C c r₀
pq : κ
r r' : ℤ
h : r = r'
hr : r₀ ≤ r
subst : (E.page r ⋯).X pq = (E.page r ⋯).X pq
⊢ (E.page r ⋯).X pq = (E.page r' ⋯).X pq

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.SpectralSequence.Basic
Goal:
C : Type u_1
inst : Category.{u_3, u_1} C
inst_1 : Abelian.{u_3, u_1} C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E : SpectralSequence.{u_1, u_2, u_3} C c r₀
pq : κ
r : ℤ
hr : r₀ ≤ r
⊢ (E.page r ⋯).X pq = (E.page r ⋯).X pq

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralSequence.Basic
Goal:
C : Type u_1
inst : Category.{u_3, u_1} C
inst_1 : Abelian.{u_3, u_1} C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
X Y Z : SpectralSequence.{u_1, u_2, u_3} C c r₀
f : X.Hom Y
g : Y.Hom Z
r r' : ℤ
hrr' : κ
pq : r + 1 = r'
hr : r₀ ≤ r
⊢ Eq (α := (X.page r ⋯).homology hrr' ⟶ (Z.page r' ⋯).X hrr')
    (CategoryStruct.comp (Y := (Z.page r ⋯).homology hrr')
        (HomologicalComplex.homologyMap
            (CategoryStruct.comp (Y := Y.page r ⋯) (f.hom r ⋯ : X.page r ⋯ ⟶ Y.page r ⋯)
              (g.hom r ⋯ : Y.page r ⋯ ⟶ Z.page r ⋯))
            hrr' :
          (X.page r ⋯).homology hrr' ⟶ (Z.page r ⋯).homology hrr')
        (Iso.hom (Z.iso r r' hrr' ⋯ ⋯) : (Z.page r ⋯).homology hrr' ⟶ (Z.page r' ⋯).X hrr') :
      (X.page r ⋯).homology hrr' ⟶ (Z.page r' ⋯).X hrr')
    (CategoryStruct.comp (Y := (X.page r' ⋯).X hrr')
        (Iso.hom (X.iso r r' hrr' ⋯ ⋯) : (X.page r ⋯).homology hrr' ⟶ (X.page r' ⋯).X hrr')
        (HomologicalComplex.Hom.f
            (CategoryStruct.comp (Y := Y.page r' ⋯) (f.hom r' ⋯ : X.page r' ⋯ ⟶ Y.page r' ⋯)
              (g.hom r' ⋯ : Y.page r' ⋯ ⟶ Z.page r' ⋯))
            hrr' :
          (X.page r' ⋯).X hrr' ⟶ (Z.page r' ⋯).X hrr') :
      (X.page r ⋯).homology hrr' ⟶ (Z.page r' ⋯).X hrr')

Tactic:
simp [HomologicalComplex.homologyMap_comp, assoc, g.comm r r', f.comm_assoc r r']

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.homologyMap_comp, CategoryTheory.SpectralSequence.Hom.comm_assoc, CategoryTheory.SpectralSequence.Hom.comm
-- Module: Mathlib.Algebra.Homology.SpectralSequence.Basic
Goal:
C : Type u_1
inst : Category.{u_3, u_1} C
inst_1 : Abelian.{u_3, u_1} C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E E' : SpectralSequence.{u_1, u_2, u_3} C c r₀
f f' : E ⟶ E'
h :
  ∀ (r : ℤ) (hr : r₀ ≤ r),
    Eq (α := E.page r ⋯ ⟶ E'.page r ⋯) (f.hom r ⋯ : E.page r ⋯ ⟶ E'.page r ⋯) (f'.hom r ⋯ : E.page r ⋯ ⟶ E'.page r ⋯)
⊢ @Hom.hom C inst inst_1 κ c r₀ E E' f = @Hom.hom C inst inst_1 κ c r₀ E E' f'

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
i j j' : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i.fst : ℤ) + u.fst = (↑j'.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j'.snd : ℤ)
fst : j.fst = j'.fst
snd : j.snd = j'.snd
⊢ j = j'

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
i j j' : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i.fst : ℤ) + u.fst = (↑j'.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j'.snd : ℤ)
⊢ j.fst = j'.fst

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
i j j' : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i.fst : ℤ) + u.fst = (↑j'.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j'.snd : ℤ)
⊢ j.snd = j'.snd

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
i i' j : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i'.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i'.snd : ℤ) + u.snd = (↑j.snd : ℤ)
fst : i.fst = i'.fst
snd : i.snd = i'.snd
⊢ i = i'

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
i i' j : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i'.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i'.snd : ℤ) + u.snd = (↑j.snd : ℤ)
⊢ i.fst = i'.fst

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
i i' j : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i'.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i'.snd : ℤ) + u.snd = (↑j.snd : ℤ)
⊢ i.snd = i'.snd

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
u : ℤ × ℤ
a b : ℕ × ℕ
⊢ (spectralSequenceNat u).Rel a b ↔ (↑a.fst : ℤ) + u.fst = (↑b.fst : ℤ) ∧ (↑a.snd : ℤ) + u.snd = (↑b.snd : ℤ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
i j j' : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i.fst + u.fst = j'.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j'.snd : ℕ) : ℤ)
fst : j.fst = j'.fst
snd : (↑j.snd : ℕ) = (↑j'.snd : ℕ)
⊢ j = j'

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
i j j' : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i.fst + u.fst = j'.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j'.snd : ℕ) : ℤ)
⊢ j.fst = j'.fst

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
i j j' : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i.fst + u.fst = j'.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j'.snd : ℕ) : ℤ)
⊢ (↑j.snd : ℕ) = (↑j'.snd : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
i i' j : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i'.fst + u.fst = j.fst ∧ (↑(↑i'.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
fst : i.fst = i'.fst
snd : (↑i.snd : ℕ) = (↑i'.snd : ℕ)
⊢ i = i'

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
i i' j : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i'.fst + u.fst = j.fst ∧ (↑(↑i'.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
⊢ i.fst = i'.fst

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
i i' j : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i'.fst + u.fst = j.fst ∧ (↑(↑i'.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
⊢ (↑i.snd : ℕ) = (↑i'.snd : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
Goal:
l : ℕ
u : ℤ × ℤ
a b : ℤ × Fin l
⊢ (spectralSequenceFin l u).Rel a b ↔ a.fst + u.fst = b.fst ∧ (↑(↑a.snd : ℕ) : ℤ) + u.snd = (↑(↑b.snd : ℕ) : ℤ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Homology.Square
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
sq : Square.{v_1, u_1} C
inst_2 : HasBinaryBiproduct.{v_1, u_1} sq.X₂ sq.X₃
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} sq.X₂ sq.X₃) (biprod.lift sq.f₁₂ (-sq.f₁₃)) (biprod.desc sq.f₂₄ sq.f₃₄) =
    0

Tactic:
simp [sq.fac]

Premises used: CategoryTheory.Square.fac
-- Module: Mathlib.Algebra.Homology.Square
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
sq : Square.{v_1, u_1} C
inst_2 : HasBinaryBiproduct.{v_1, u_1} sq.X₂ sq.X₃
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} sq.X₂ sq.X₃) (biprod.lift sq.f₁₂ sq.f₁₃) (biprod.desc sq.f₂₄ (-sq.f₃₄)) =
    0

Tactic:
simp [sq.fac]

Premises used: CategoryTheory.Square.fac
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
e : K ≅ L
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : K.HasTotal c₁₂
⊢ L.HasTotal c₁₂

Tactic:
GradedObject.hasMap_of_iso (GradedObject.isoMk K.toGradedObject L.toGradedObject
    (fun ⟨i₁, i₂⟩ =>
      (HomologicalComplex.eval _ _ i₁ ⋙ HomologicalComplex.eval _ _ i₂).mapIso e)) _

Premises used: HomologicalComplex₂.toGradedObject, CategoryTheory.GradedObject.isoMk, CategoryTheory.Functor.comp, HomologicalComplex, HomologicalComplex.eval, CategoryTheory.Iso, _private.0.HomologicalComplex₂.hasTotal_of_iso.match_1, CategoryTheory.Functor.mapIso, CategoryTheory.GradedObject.hasMap_of_iso
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
dsimp :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂)) =
    0
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂) 0

Tactic:
dsimp [d₁]

Premises used: HomologicalComplex₂.d₁
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (0 : (K.X i₁).X i₂ ⟶ (K.X (c₁.next i₁)).X i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ :
          K.toGradedObject (c₁.next i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
    0
rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂)) 0 = 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) 0 0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂)) =
    0

Tactic:
rw [K.shape_f _ _ h, zero_comp, smul_zero]

Premises used: smul_zero, HomologicalComplex₂.shape_f, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
dsimp :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂)) =
    0
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂) 0

Tactic:
dsimp [d₂]

Premises used: HomologicalComplex₂.d₂
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) (0 : (K.X i₁).X i₂ ⟶ (K.X i₁).X (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ :
          K.toGradedObject (i₁, c₂.next i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
    0
rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂)) 0 = 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) 0 0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂)) =
    0

Tactic:
rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]

Premises used: smul_zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
obtain :
  ∀ (h : c₁.Rel i₁ (c₁.next i₁)),
    K.d₁ c₁₂ i₁ i₂ i₁₂ =
      HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
        (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
          (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂))
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂)

Tactic:
obtain rfl := c₁.next_eq' h

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂) =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
rw₁ :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h') =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
h₁ : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
rw₂ :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h') =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
h₂ : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')

Tactic:
rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

Premises used: CategoryTheory.GradedObject.ιMapObjOrZero_eq, HomologicalComplex₂.toGradedObject, HomologicalComplex₂.totalAux.d₁_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
obtain :
  ∀ (h : c₂.Rel i₂ (c₂.next i₂)),
    K.d₂ c₁₂ i₁ i₂ i₁₂ =
      HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
        (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
          (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂))
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂)

Tactic:
obtain rfl := c₂.next_eq' h

Premises used: rfl, ComplexShape.next_eq'