mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ n < i

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ i ≠ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n i : ℤ
hi : n < i
⊢ i ≠ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
h : ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
i : ℕ
⊢ n ≤ n + ↑i

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
i : ℤ
k : ℕ
h : ∀ (i_1 : ℕ) (i' : ℤ), (embeddingUpIntLE (i + ↑k)).f i_1 = i' → QuasiIsoAt φ i'
hi : i ≤ i + ↑k
⊢ i + ↑k - ↑k = i

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
h : ∀ i ≤ n, QuasiIsoAt φ i
i : ℕ
⊢ n - ↑i ≤ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsStrictlyLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ n < i + a

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : autoParam (i < n') isStrictlyGE_iff._auto_1
⊢ i + a < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ n < a + i

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : i < n'
⊢ a + i < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : n < i
⊢ 0 ≤ i - n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : n < i
h : i - n = 0
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
⊢ 0 ≤ n - i

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝³ : L.IsLocalization W
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z
α : W.Q.obj X ⟶ W.Q.obj Y
β : W.Q.obj Y ⟶ W.Q.obj Z
⊢ (homEquiv W W.Q L)
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z)).symm
        ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z))
          ((homEquiv W W.Q W.Q)
            ((homEquiv W W.Q W.Q)
                ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
              (homEquiv W W.Q W.Q)
                ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)))))) =
    (homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
      (homEquiv W W.Q L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β))

Tactic:
Equiv.symm_apply_apply

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝³ : L.IsLocalization W
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z
α : W.Q.obj X ⟶ W.Q.obj Y
β : W.Q.obj Y ⟶ W.Q.obj Z
⊢ (homEquiv W W.Q L)
      ((homEquiv W W.Q W.Q)
        ((homEquiv W W.Q W.Q) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
          (homEquiv W W.Q W.Q)
            ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)))) =
    (homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
      (homEquiv W W.Q L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β))
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
h : n - i = 0
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z T : C
inst✝⁵ : HasSmallLocalizedHom W X Y
inst✝⁴ : HasSmallLocalizedHom W X Z
inst✝³ : HasSmallLocalizedHom W X T
inst✝² : HasSmallLocalizedHom W Y Z
inst✝¹ : HasSmallLocalizedHom W Y T
inst✝ : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ (α.comp β).comp γ = α.comp (β.comp γ)

Tactic:
by
  apply (equiv W W.Q).injective
  simp only [equiv_comp, assoc]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ i < b

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (SmallHom.equiv W L) (f.shift n a' h) ≫ (Functor.commShiftIso L a').hom.app Y =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f ≫ (Functor.commShiftIso L a).hom.app Y) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
equiv_shift'

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ ((Functor.commShiftIso L n).hom.app X ≫
        (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
          (shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y) ≫
            (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (Functor.commShiftIso L a').inv.app Y) ≫
      (Functor.commShiftIso L a').hom.app Y =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f ≫ (Functor.commShiftIso L a).hom.app Y) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ a + -a = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
this : ((shiftFunctor (CochainComplex C ℤ) a).obj ((CochainComplex.singleFunctor C 0).obj X)).IsStrictlyLE (-a)
⊢ b + -b = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
this✝ : ((shiftFunctor (CochainComplex C ℤ) a).obj ((CochainComplex.singleFunctor C 0).obj X)).IsStrictlyLE (-a)
this : ((shiftFunctor (CochainComplex C ℤ) b).obj ((CochainComplex.singleFunctor C 0).obj Y)).IsStrictlyGE (-b)
⊢ -a < -b

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
⊢ ↑b + ↑a = ↑c

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁₂ + a₃ = a

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁ + a₂₃ = a

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ ↑a₃ + ↑a₂ + ↑a₁ = ↑a

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext X Y a₁
β : Ext Y Z 0
γ : Ext Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ a₁ + 0 + a₃ = a₁₃

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ a₁ + a₂ + 0 = a₁₂

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y Z T : C
inst✝ : HasDerivedCategory C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
⊢ ↑b + ↑a = ↑c

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ 0 + 0 + n = n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
α : ↑(AddCommGrpCat.of (Ext X X✝ n))
⊢ n + 0 + 0 = n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ 0 + n + 0 = n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ 1 + n₀ = n₁

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + 1 = 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + n = n'

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + 1 + n = n'

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + 0 = 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + n = n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + 0 + n = n'

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝))).op ≫
      ((shiftFunctorZero D A).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorZero (OppositeShift C A) A).hom.app x✝) ≫
      ((shiftFunctorZero D A).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op

Tactic:
oppositeShiftFunctorZero_hom_app

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝))).op ≫
      ((shiftFunctorZero D A).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝)).op ≫
      ((shiftFunctorZero D A).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ + b₂ = b₃

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ = -a₁

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₂ = -a₂

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₃ = -a₃

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X =
    (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
      (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
        ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorAdd'_op_hom_app X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃,
    assoc, assoc, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app]
  erw [Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]
  rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) opShiftFunctorEquivalence_unitIso_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) opShiftFunctorEquivalence_unitIso_inv_app._auto_1
⊢ m + n = 0

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : autoParam (m + n = p) opShiftFunctorEquivalence_add_unitIso_hom_app_eq._auto_1
⊢ n + m = p

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ n + m = p

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : autoParam (m + n = p) opShiftFunctorEquivalence_add_unitIso_inv_app_eq._auto_1
⊢ n + m = p

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) shiftFunctorCompIsoId_op_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m + n = 0

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
m n : ℤ
hmn : m + n = 0
⊢ m = -n

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ n + -n = 0

Tactic:
lia

Goal state after: