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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₄, u₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

Tactic:
Φ.isEquivalence_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₄, u₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ G.IsEquivalence
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Tactic:
refine ⟨ψ, ?_, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f = ψ.fst.map L ⋯

case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f' = ψ.snd.map L ⋯

case refine_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f'' = ψ.thd.map L ⋯
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ X₂ : C
this✝ : HasBinaryBiproduct (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex A := { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := biprod.inl, g := biprod.snd, zero := ⋯ }.map F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf : (g ≫ S.f) ≫ F.biprodComparison X₁ X₂ = 0
⊢ g ≫ S.f = 0

Tactic:
dsimp [S] at hf ⊢

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ X₂ : C
this✝ : HasBinaryBiproduct (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex A := { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := biprod.inl, g := biprod.snd, zero := ⋯ }.map F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf : (g ≫ F.map biprod.inl) ≫ F.biprodComparison X₁ X₂ = 0
⊢ g ≫ F.map biprod.inl = 0
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
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a

Tactic:
rw [← h₁₂, ← add_assoc, h]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f) → P.retracts ≤ P

Tactic:
intro h₁

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
⊢ P.retracts ≤ P
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.retracts ≤ P → ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f

Tactic:
intro h₁

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
⊢ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
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
P : ObjectProperty C
i✝ : C
⊢ P.extensionProduct ⊥ i✝ ≤ ⊥ i✝

Tactic:
⟨_, _, _, _, _, _, _, h⟩

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
P : ObjectProperty C
i✝ w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ i✝
w✝¹ : i✝ ⟶ w✝³
w✝ : w✝³ ⟶ (shiftFunctor C 1).obj w✝⁴
left✝¹ : Triangle.mk w✝² w✝¹ w✝ ∈ distinguishedTriangles
left✝ : P w✝⁴
h : ⊥ w✝³
⊢ ⊥ i✝
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
P Q P' : ObjectProperty C
h : P ≤ P'
X : C
⊢ P.extensionProduct Q X ≤ P'.extensionProduct Q X

Tactic:
⟨Y, Z, f, g, k, hT, hP, hQ⟩

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
P Q P' : ObjectProperty C
h : P ≤ P'
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
k : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g k ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ P'.extensionProduct Q X
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
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X : C
⊢ P.extensionProduct Q X ≤ P.extensionProduct Q' X

Tactic:
⟨Y, Z, f, g, k, hT, hP, hQ⟩

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
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
k : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g k ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ P.extensionProduct Q' X
Module: Mathlib.Algebra.Homology.ShortComplex.Retract

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        ⋯ ≫
      Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        ⋯ =
    𝟙 (Arrow.mk (homologyMap f₁))

Tactic:
ext <;> simp [← homologyMap_comp]

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

Goal state before:
pp: case succ
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✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')

Tactic:
| succ n hn =>

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
inst✝ : CategoryWithHomology C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ ShiftSequence.shiftIso C (m + n) a a'' ⋯ =
    Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex C (up ℤ)) m n) (homologyFunctor C (up ℤ) a) ≪≫
      (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).associator
          (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) (homologyFunctor C (up ℤ) a) ≪≫
        (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).isoWhiskerLeft
            (ShiftSequence.shiftIso C n a a' ha') ≪≫
          ShiftSequence.shiftIso C m a' a'' ha''

Tactic:
by
    ext K
    dsimp [homologyMap]
    simp only [ShiftSequence.shiftIso_hom_app, id_comp,
      ← ShortComplex.homologyMap_comp, shiftFunctorAdd'_eq_shiftFunctorAdd,
      shiftShortComplexFunctorIso_add'_hom_app n m _ rfl a a' a'' ha' ha'' K]

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
P : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P.trW T.mor₂ ↔ P T.obj₁

Tactic:
by
  simpa [P.prop_shift_iff_of_isStableUnderShift]
    using! P.trW_iff_of_distinguished _ (rot_of_distTriang _ hT)

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

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ (if i + n = a + n then X else 0) = 0

Tactic:
if_neg (fun h' => h (by lia))

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ 0 = 0
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
⊢ (mappingCone.snd φ).v (p + -1) (p + -1) ⋯ ≫ (δ (m + 1) (m + 2) β).v (p + -1) q ⋯ +
      (m.negOnePow • (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq +
        (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ (δ m (m + 1) α).v p q hpq) =
    (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ (δ m (m + 1) α).v p q hpq +
        m.negOnePow • (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq +
      (mappingCone.snd φ).v (p + -1) (p + -1) ⋯ ≫ (δ (m + 1) (m + 2) β).v (p + -1) q ⋯

Tactic:
abel

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 n' α).v p q hpq ≫ (mappingCone.inl φ).v q (q + -1) ⋯ +
      (-(δ m n β).v p (q + -1) ⋯ ≫ (mappingCone.inr φ).f (q + -1) +
        -α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ (mappingCone.inr φ).f (q + -1)) =
    (δ n n' α).v p q hpq ≫ (mappingCone.inl φ).v q (q + -1) ⋯ -
      ((δ m n β).v p (q + -1) ⋯ ≫ (mappingCone.inr φ).f (q + -1) +
        α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ (mappingCone.inr φ).f (q + -1))

Tactic:
abel

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) =
    δ (-1) 0
        (-(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:
rw [δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
        Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul,
        δ_comp _ _ (show 1 + (-2) = -1 by decide) 2 (-1) 0 (by decide)
          (by decide) (by decide),
        δ_comp _ _ (show (-1) + (-1) = -2 by decide) 0 0 (-1) (by decide)
          (by decide) (by decide), Int.negOnePow_neg, Int.negOnePow_neg,
        Int.negOnePow_even 2 ⟨1, by decide⟩, Int.negOnePow_one, Units.neg_smul,
        one_smul, one_smul, δ_inl, δ_inl, δ_snd, Cocycle.δ_eq_zero, Cochain.zero_comp, add_zero,
        Cochain.neg_comp, neg_neg]

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
                  (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
              ⋯)
            ⋯ +
          ((↑(fst (mappingConeCompTriangle f g).mor₁)).comp (Cochain.ofHom (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.Embedding.Boundary

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hij : ¬c.Rel (c.prev j) j
⊢ ¬e.BoundaryLE (c.prev j)

Tactic:
simpa only [c.prev_eq_self j hij] using hj

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

Goal state before:
pp: case neg
ι : 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 ⟶ L.extend e
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

Tactic:
· apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_tgt

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

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryGE i
i' : ι'
h : e.f i = i'
⊢ (truncGE'Map φ e).f i = (K.truncGE'XIsoOpcycles e h hi).hom ≫ opcyclesMap φ i' ≫ (L.truncGE'XIsoOpcycles e h hi).inv

Tactic:
by
  subst h
  exact dif_pos hi

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'
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
hk'' : e.f k = k'
⊢ (rightHomologyData K e hj' hi hi' hk hk' h).g' = h.g' ≫ (K.extendXIso e hk'').inv

Tactic:
by
  rw [← cancel_epi h.p, ← cancel_epi (extendXIso K e hj').hom]
  have := (rightHomologyData K e hj' hi hi' hk hk' h).p_g'
  dsimp at this
  rw [assoc] at this
  rw [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]

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

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ ¬c.Rel j (c.next j)

Tactic:
by simpa only [hk] using hjk

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

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✝⁴ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ Epi ((K.restrictionToTruncGE' e).f i)

Tactic:
K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e rfl hi

Goal state after:
case pos
ι : 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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ Epi ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv)
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e rfl hi

Goal state after:
case pos
ι : 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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv)
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₂ L₃) ((homEquiv W L₁ L₂) f) = (homEquiv W L₁ L₃) f

Tactic:
by
  dsimp only [homEquiv_apply]
  apply LocalizerMorphism.homMap_homMap

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
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a

Tactic:
rw [← h₁₂, ← add_assoc, h]

Goal state after: