mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
obtain ⟨γ, hγ₁, hγ₂⟩ := (RightFraction₂.mk _ α.hs β.f β.f').exists_leftFraction₂

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
γ : W.LeftFraction₂ α.Y' β.Y'
hγ₁ :
  { X' := Y, s := α.s, hs := ⋯, f := β.f, f' := β.f' }.f ≫ γ.s =
    { X' := Y, s := α.s, hs := ⋯, f := β.f, f' := β.f' }.s ≫ γ.f
hγ₂ :
  { X' := Y, s := α.s, hs := ⋯, f := β.f, f' := β.f' }.f' ≫ γ.s =
    { X' := Y, s := α.s, hs := ⋯, f := β.f, f' := β.f' }.s ≫ γ.f'
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.f ≫ z₁.s = { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.f ≫ z₂.s = { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
fac₁' :
  { X' := Y, s := a₁.s ≫ t₁, hs := ht, f := b.f ≫ z₁.s }.f ≫ w₁.s =
    { X' := Y, s := a₁.s ≫ t₁, hs := ht, f := b.f ≫ z₁.s }.s ≫ w₁.f
⊢ W (a₂.s ≫ t₂)

Tactic:
rw [← hst]; exact ht

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

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
⊢ LeftFractionRel p₁ p₂

Tactic:
obtain ⟨q, fac₃⟩ := exists_leftFraction (RightFraction.mk (z₁.s ≫ w₁.s)
        (W.comp_mem _ _ z₁.hs w₁.hs) (z₂.s ≫ w₂.s))

Goal state after:
case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
q : W.LeftFraction w₁.Y' w₂.Y'
fac₃ :
  { X' := b.Y', s := z₁.s ≫ w₁.s, hs := ⋯, f := z₂.s ≫ w₂.s }.f ≫ q.s =
    { X' := b.Y', s := z₁.s ≫ w₁.s, hs := ⋯, f := z₂.s ≫ w₂.s }.s ≫ q.f
⊢ LeftFractionRel p₁ p₂
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderColimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)

Tactic:
rw [P.isClosedUnderColimitsOfShape_iff_of_equivalence
      (Discrete.equivalence (equivShrink.{w} _))]
    exact H _

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ P X

Tactic:
have hX : IsInitial X :=
      (IsColimit.equivOfNatIsoOfIso p.diag.uniqueFromEmpty _ _
        (by exact Cocone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩))).1 p.isColimit

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
hX : IsInitial X
⊢ P X
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact

Tactic:
distinguished_iff_iso_trianglehOfDegreewiseSplit

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT✝ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
hT : ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ (F' a).map ((shiftFunctorAdd D m n).hom.app (L.obj K)) ≫
      (F' a).map ((shiftFunctor D n).map ((commShiftIso L m).inv.app K)) ≫
        (F' a).map ((commShiftIso L n).inv.app ((shiftFunctor C m).obj K)) ≫
          (F' a).map (L.map ((shiftFunctorAdd C m n).inv.app K)) ≫
            (F' a).map (L.map ((shiftFunctorAdd C m n).hom.app K)) ≫
              (e' a).hom.app ((shiftFunctor C n).obj ((shiftFunctor C m).obj K)) ≫
                (G.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj K) ≫
                  (G.shiftIso m a' a'' ha'').hom.app K ≫ (e' a'').inv.app K =
    (F' a).map ((shiftFunctorAdd D m n).hom.app (L.obj K)) ≫
      (induced.shiftIso L G M F' e' n a a' ha').hom.app ((shiftFunctor D m).obj (L.obj K)) ≫
        (F' a').map ((commShiftIso L m).inv.app K) ≫
          (e' a').hom.app ((shiftFunctor C m).obj K) ≫ (G.shiftIso m a' a'' ha'').hom.app K ≫ (e' a'').inv.app K

Tactic:
simp only [← NatTrans.naturality_assoc, induced.shiftIso_hom_app_obj,
      ← Functor.map_comp_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, comp_obj,
      Functor.map_id, id_comp]

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ (F' a).map
        ((shiftFunctorAdd D m n).hom.app (L.obj K) ≫
          (shiftFunctor D n).map ((commShiftIso L m).inv.app K) ≫
            (commShiftIso L n).inv.app ((shiftFunctor C m).obj K)) ≫
      (e' a).hom.app ((shiftFunctor C n).obj ((shiftFunctor C m).obj K)) ≫
        (G.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj K) ≫
          (G.shiftIso m a' a'' ha'').hom.app K ≫ (e' a'').inv.app K =
    (F' a).map ((shiftFunctorAdd D m n).hom.app (L.obj K)) ≫
      (shiftFunctor D n ⋙ F' a).map ((commShiftIso L m).inv.app K) ≫
        ((F' a).map ((commShiftIso L n).inv.app ((shiftFunctor C m).obj K)) ≫
            (e' a).hom.app ((shiftFunctor C n).obj ((shiftFunctor C m).obj K)) ≫
              (G.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj K) ≫ (e' a').inv.app ((shiftFunctor C m).obj K)) ≫
          (e' a').hom.app ((shiftFunctor C m).obj K) ≫ (G.shiftIso m a' a'' ha'').hom.app K ≫ (e' a'').inv.app K
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ (f.comp g h).map F = (f.map F).comp (g.map F) h

Tactic:
dsimp [comp, map]
  simp only [Functor.map_comp, assoc, ← Functor.commShiftIso_hom_naturality_assoc]
  simp only [F.commShiftIso_add' h, Functor.CommShift.isoAdd'_hom_app,
    ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.comp_obj, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i i' : ℤ
hi : n + i = i'
⊢ n + (up ℤ).prev i = (up ℤ).prev i'

Tactic:
simp only [prev]; lia

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

Goal state before:
pp: case mp
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
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1) →
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
rintro ⟨Z, g, h, H, mem⟩

Goal state after:
case mp
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
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z✝ : C
g✝ : Y ⟶ Z✝
Z : C
g : Z✝ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk g✝ g h ∈ distinguishedTriangles
mem : P Z
⊢ ∃ X f h, ∃ (_ : Triangle.mk f g✝ h ∈ distinguishedTriangles), P X
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case mpr
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
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X) →
    ∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1

Tactic:
rintro ⟨Z, g, h, H, mem⟩

Goal state after:
case mpr
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
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z✝ : C
g✝ : Y ⟶ Z✝
Z : C
g : Z ⟶ Y
h : Z✝ ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g g✝ h ∈ distinguishedTriangles
mem : P Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk g✝ g h ∈ distinguishedTriangles), P Z
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
J : Type
x✝ : Finite J
⊢ ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), P.isoClosure.trW (f j)) → P.isoClosure.trW (Limits.Pi.map f)

Tactic:
intro _ _ X₁ X₂ f hf

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
J : Type
x✝ : Finite J
X₁✝ X₂✝ : J → C
X₁ : HasProduct X₁✝
X₂ : HasProduct X₂✝
f : (j : J) → X₁✝ j ⟶ X₂✝ j
hf : ∀ (j : J), P.isoClosure.trW (f j)
⊢ P.isoClosure.trW (Limits.Pi.map f)
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₃
⊢ -1 + -1 = -2

Tactic:
decide

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₃
⊢ 1 + -2 = -1

Tactic:
decide

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₃
⊢ -1 + 1 = 0

Tactic:
decide

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₃
⊢ 1 + 1 = 2

Tactic:
decide

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₃
⊢ -2 + 1 = -1

Tactic:
decide

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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                (δ (-2) (-1) ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)) ⋯ +
              (-2).negOnePow •
                (δ 1 2 ↑(fst (f ≫ g))).comp
                  ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
δ_comp _ _ (show (-1) + (-1) = -2 by decide) 0 0 (-1) (by decide)
          (by decide) (by decide),

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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp (δ (-1) 0 (inl (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  (-1).negOnePow • (δ (-1) 0 (inl f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                ⋯ +
              (-2).negOnePow •
                (δ 1 2 ↑(fst (f ≫ g))).comp
                  ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
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₃
⊢ 2 = 1 + 1

Tactic:
decide

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 : ℤ
⊢ 1 + -2 = -1

Tactic:
decide

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 : ℤ
⊢ -1 + -1 = -2

Tactic:
decide

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

Goal state before:
pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)

Tactic:
intro k hk
    apply hk' k
    rw [← c'.next_eq' hj, c'.next_eq' hk]

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

Goal state before:
pp: case pos
ι : 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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ Projective ((K.extend e).X i')

pp: case neg
ι : 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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Projective ((K.extend e).X i')

Tactic:
· obtain ⟨i, hi⟩ := hi'
    exact Projective.of_iso (K.extendXIso e hi).symm inferInstance

Goal state after:
case neg
ι : 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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Projective ((K.extend e).X i')
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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ h.ι ≫
      (isColimitCokernelCofork K e hj' hi hi' (CokernelCofork.ofπ h.p ⋯) h.hp).desc
        (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    0

Tactic:
← d_comp_desc_eq_zero_iff K e hj' hi hi' hk hk' _ h.hp

Goal state after:
ι : 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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) ⋯) = 0
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: case e_a
ι : 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 k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ K.iCycles j' ≫ (K.sc j').pOpcycles = K.homologyπ j' ≫ (K.sc j').homologyι

Tactic:
symm

Goal state after:
case e_a
ι : 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 k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ K.homologyπ j' ≫ (K.sc j').homologyι = K.iCycles j' ≫ (K.sc j').pOpcycles
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : 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.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : ¬c.Rel i j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
simp [HomologicalComplex.shape _ _ _ hij]

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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ QuasiIsoAt (extendMap φ e) j' ↔ QuasiIsoAt φ j

Tactic:
by
  simp only [quasiIsoAt_iff_isIso_homologyMap]
  exact (MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.extendHomologyIso e hj') (L.extendHomologyIso e hj'))

Goal state after: