mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯ =
    (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v p
      p ⋯

Tactic:
rw [ext_from_iff _ (p + 1) _ rfl, ext_to_iff _ _ (p + 1) rfl]

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ (((inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯) ≫ (↑(fst g)).v p (p + 1) ⋯ =
        ((inl f).v (p + 1) p ⋯ ≫
            (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
              p p ⋯) ≫
          (↑(fst g)).v p (p + 1) ⋯ ∧
      ((inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯) ≫ (snd g).v p p ⋯ =
        ((inl f).v (p + 1) p ⋯ ≫
            (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
              p p ⋯) ≫
          (snd g).v p p ⋯) ∧
    (inr f).f p ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯ =
      (inr f).f p ≫
        (Cochain.ofHom
              ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
          p p ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ p + 1 = p + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ -1 + n' = n

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
m : ℤ
α : Cochain K M m
n' p q : ℤ
β : Cochain L M (m + 1)
hn' : m + 1 + 1 = n'
hpq : p + (m + 1) = q
⊢ n' = m + 2

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ m + 2 + -1 = m + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ m + 1 + 1 = m + 2

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ p + -1 + 1 = p

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ p + -1 + (m + 2) = q

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain K M m
β : Cocycle L M n
h : m + 1 = n
hαβ : δ m n α + m.negOnePow • (Cochain.ofHom φ).comp ↑β ⋯ = 0
⊢ n + 1 = n + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
α : Cochain K M 0
β : Cocycle L M 1
hαβ : δ 0 1 α + (Cochain.ofHom φ).comp ↑β ⋯ = 0
⊢ 0 + 1 = 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
⊢ n + -1 = m

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₁ + m = p₂ + -1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₂ + -1 + 1 = p₂

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ ((homologyFunctor C 0).shift a).map ((quotientCompQhIso C).inv.app K) ≫
      (homologyFunctor C 0).shiftMap (ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)) a a' h ≫
        ((homologyFunctor C 0).shift a').map ((quotientCompQhIso C).hom.app L) =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L

Tactic:
ShiftedHom.comp_map,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ ((homologyFunctor C 0).shift a).map ((quotientCompQhIso C).inv.app K) ≫
      (homologyFunctor C 0).shiftMap ((ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ))).map Qh) a a'
          h ≫
        ((homologyFunctor C 0).shift a').map ((quotientCompQhIso C).hom.app L) =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + -1 = p₃
⊢ p₁ + m = p₃

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ p + n = q + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ n' + -1 = n

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ p + n = q + -1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ q + -1 + 1 = q

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasBinaryBiproducts C
⊢ -1 + 1 = 0

Tactic:
lia

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

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

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝²³ : Category.{v_1, u_1} C
inst✝²² : HasZeroObject C
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : Preadditive C
inst✝¹⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁸ : Pretriangulated C
D✝ : Type u_2
inst✝¹⁷ : Category.{v_2, u_2} D✝
inst✝¹⁶ : Preadditive D✝
inst✝¹⁵ : HasZeroObject D✝
inst✝¹⁴ : HasShift D✝ ℤ
inst✝¹³ : ∀ (n : ℤ), (shiftFunctor D✝ n).Additive
inst✝¹² : Pretriangulated D✝
E : Type u_3
inst✝¹¹ : Category.{v_3, u_3} E
inst✝¹⁰ : HasShift E ℤ
P : ObjectProperty C
inst✝⁹ : P.IsTriangulated
D : Type u_4
inst✝⁸ : Category.{u_5, u_4} D
inst✝⁷ : HasZeroObject D
inst✝⁶ : Preadditive D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
⊢ (P.map F).IsTriangulated

Tactic:
rw [← F.essImage_ι_comp]

Goal state after:
C : Type u_1
inst✝²³ : Category.{v_1, u_1} C
inst✝²² : HasZeroObject C
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : Preadditive C
inst✝¹⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁸ : Pretriangulated C
D✝ : Type u_2
inst✝¹⁷ : Category.{v_2, u_2} D✝
inst✝¹⁶ : Preadditive D✝
inst✝¹⁵ : HasZeroObject D✝
inst✝¹⁴ : HasShift D✝ ℤ
inst✝¹³ : ∀ (n : ℤ), (shiftFunctor D✝ n).Additive
inst✝¹² : Pretriangulated D✝
E : Type u_3
inst✝¹¹ : Category.{v_3, u_3} E
inst✝¹⁰ : HasShift E ℤ
P : ObjectProperty C
inst✝⁹ : P.IsTriangulated
D : Type u_4
inst✝⁸ : Category.{u_5, u_4} D
inst✝⁷ : HasZeroObject D
inst✝⁶ : Preadditive D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
⊢ (P.ι ⋙ F).essImage.IsTriangulated
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), i₁ + 1 = i₂ ↔ ↑i₁ + 1 = ↑i₂

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), i₂ + 1 = i₁ ↔ -↑i₁ + 1 = -↑i₂

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
i : ℤ
j : ℕ
h : i + 1 = -↑j
⊢ -(↑j + 1) = i

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
x✝¹ x✝ : ℕ
h : p + ↑x✝¹ = p + ↑x✝
⊢ x✝¹ = x✝

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), i₁ + 1 = i₂ ↔ p + ↑i₁ + 1 = p + ↑i₂

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
j : ℕ
x✝ : ℤ
h : p + ↑j + 1 = x✝
⊢ p + (↑j + 1) = x✝

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
x✝¹ x✝ : ℕ
h : p - ↑x✝¹ = p - ↑x✝
⊢ x✝¹ = x✝

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), i₂ + 1 = i₁ ↔ p - ↑i₁ + 1 = p - ↑i₂

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p x✝ : ℤ
k : ℕ
h : x✝ + 1 = p - ↑k
⊢ p - (↑k + 1) = x✝

Tactic:
lia

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

Goal state before:
pp: p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ p - ↑(p - n).natAbs = n

Tactic:
lia

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

Goal state before:
pp: case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ ¬p - ↑i✝ = n

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 1 + 1 = n + 2

Tactic:
lia

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

Goal state before:
pp: p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ p + ↑(n - p).natAbs = n

Tactic:
lia

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

Goal state before:
pp: case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ ¬p + ↑i✝ = n

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 1 = n + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 2 + -2 = n

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 2 + -1 = n + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompTriangle f g).mor₂

Tactic:
mappingConeCompTriangle_mor₂

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯)
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
extend.d_eq K hi hj,

Goal state after:
case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ (extend.XIso K hi).hom ≫ K.d i j ≫ (extend.XIso K hj).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
extend.d_eq K hi hj,

Goal state after:
case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ ((extend.XIso K hi).hom ≫ K.d i j ≫ (extend.XIso K hj).inv) ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬p + ↑n + 1 = p + (↑n + 1)
⊢ n + 1 = 0

Tactic:
lia

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

Goal state before:
pp: case mpr.right
p : ℤ
i : ℕ
hi : p + ↑i + 1 = p + 0
⊢ False

Tactic:
lia

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

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
this : ¬p - (↑n + 1) + 1 = p - ↑n
⊢ n + 1 = 0

Tactic:
lia

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

Goal state before:
pp: case mpr.right
p : ℤ
i : ℕ
hi : p - 0 + 1 = p - ↑i
⊢ False

Tactic:
lia

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).inv ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

Tactic:
dsimp [restrictionXIso]

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ (L.extendXIso e ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j : ι
hi : c.prev j = i
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ (K.restriction e).pOpcycles j ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom =
    (K.restrictionXIso e hj').hom ≫ K.pOpcycles j'

Tactic:
simp [restrictionOpcyclesIso]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j : ι
hi : c.prev j = i
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.pOpcycles j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv =
    (K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j

Tactic:
simp [restrictionOpcyclesIso]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extend e).ExactAt j' ↔ K.ExactAt j

Tactic:
simp only [HomologicalComplex.exactAt_iff_isZero_homology]
  exact (K.extendHomologyIso e hj').isZero_iff

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
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ n ≤ n

Tactic:
lia

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

Goal state before:
pp: n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i₁ i₂ : ℕ
⊢ ¬n₀ - ↑i₁ = n₁ + ↑i₂

Tactic:
lia

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

Goal state before:
pp: n₁ i : ℤ
k : ℕ
h : i + ↑k + 1 = n₁
hi : i ≤ i + ↑k
⊢ i + ↑k - ↑k = i

Tactic:
lia

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

Goal state before:
pp: n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : ¬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 : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : i + 1 = 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✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n + 1 = 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 : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : i < n
⊢ i < n

Tactic:
lia

Goal state after: