mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      ((CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (a.negOnePow •
            (CategoryTheory.shiftFunctor C b).map
              ((CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁)) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)

Tactic:
Linear.units_smul_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      ((CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (a.negOnePow •
          (CategoryTheory.shiftFunctor C b).map
              ((CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
            (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁))
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₃ = 0 → Epi T.mor₂

pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ Epi T.mor₂ → T.mor₃ = 0

Tactic:
· intro h
    rw [epi_iff_cancel_zero]
    intro X g hg
    obtain ⟨f, rfl⟩ := yoneda_exact₃ T hT g hg
    rw [h, zero_comp]

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ Epi T.mor₂ → T.mor₃ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
⊢ f ≫ T.mor₂ = 0

Tactic:
by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : HasShift C ℤ
inst✝⁵ : HasShift D ℤ
inst✝⁴ : HasShift E ℤ
F : C ⥤ D
inst✝³ : F.CommShift ℤ
G : D ⥤ E
inst✝² : G.CommShift ℤ
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Triangle C
f : F.mapTriangle.obj X ⟶ F.mapTriangle.obj Y
⊢ F.map (X.mor₃ ≫ (shiftFunctor C 1).map (F.preimage f.hom₁)) = F.map (F.preimage f.hom₃ ≫ Y.mor₃)

Tactic:
by
        rw [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app Y.obj₁)]
        simpa only [mapTriangle_obj, map_comp, assoc, commShiftIso_hom_naturality,
          map_preimage, Triangle.mk_mor₃] using! f.comm₃

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
p q : ℤ
hpq : p + 1 = q
⊢ (S.g.f q ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v q p ⋯ -
        (σ q).r ≫ (XIsoOfEq S.X₁ ⋯).hom ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f p) ≫
      ((↑(mappingCone.fst (homOfDegreewiseSplit S σ))).v p q hpq ≫ (σ q).s -
        (mappingCone.snd (homOfDegreewiseSplit S σ)).v p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) q ⋯) =
    𝟙 (S.X₂.X q)

Tactic:
by
    subst hpq
    have h := (σ (p + 1)).id
    dsimp at h ⊢
    simp only [id_comp, Cochain.ofHom_v, comp_sub, sub_comp, assoc, mappingCone.inl_v_fst_v_assoc,
      mappingCone.inr_f_fst_v_assoc, shiftFunctor_obj_X', zero_comp, comp_zero, sub_zero,
      mappingCone.inl_v_snd_v_assoc, mappingCone.inr_f_snd_v_assoc, zero_sub, sub_neg_eq_add, ← h]
    abel

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k :
  { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i, g := opcyclesMap S.g i,
        zero := ⋯ }.X₂ ⟶
    A
hk :
  { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i, g := opcyclesMap S.g i,
          zero := ⋯ }.f ≫
      k =
    0
⊢ { l //
    { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i,
            g := opcyclesMap S.g i, zero := ⋯ }.g ≫
        l =
      k }

Tactic:
dsimp at k hk ⊢
    have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero])
    dsimp at H
    refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
    · rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯)

Tactic:
apply ShortComplex.isLimitOfIsLimitπ

Goal state after:
case h₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (ShortComplex.π₁.mapCone (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))

case h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (ShortComplex.π₂.mapCone (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))

case h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (ShortComplex.π₃.mapCone (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ ((cyclesFunctor C c j).mapShortComplex.obj S).Exact

Tactic:
have := hS.mono_f
    exact cycles_left_exact S hS.exact j

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ 𝟙 W.Q ◫ natTransExtension (eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯) = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)

Tactic:
natTransExtension_hcomp

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯ = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C ⥤ D₁
L₂ : C ⥤ D₂
W' : MorphismProperty C
inst✝¹ : L₁.IsLocalization W'
inst✝ : L₂.IsLocalization W'
⊢ (uniq L₁ L₂ W').symm = uniq L₂ L₁ W'

Tactic:
by
  dsimp [uniq, Equivalence.trans]
  ext <;> aesop

Goal state after:
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₁ : 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₃ : z₂.s ≫ w₂.s ≫ q.s = z₁.s ≫ w₁.s ≫ q.f
⊢ b.f ≫ z₁.s ≫ w₁.s ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s

Tactic:
← fac₃,

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
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₃ : z₂.s ≫ w₂.s ≫ q.s = z₁.s ≫ w₁.s ≫ q.f
⊢ b.f ≫ z₂.s ≫ w₂.s ≫ q.s = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (Q W).map f ≫ Qinv s hs = homMk { Y' := Y', f := f, s := s, hs := hs }

Tactic:
dsimp only [Q_map, Qinv]
  rw [homMk_comp_homMk (ofHom W f) (ofInv s hs) (ofHom W (𝟙 _)) (by simp)]
  simp

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
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
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap (T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁) n₀ n₁ ⋯ = 0

Tactic:
comp_distTriang_mor_zero₃₁ _ hT,

Goal state after:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
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
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap 0 n₀ n₁ ⋯ = 0
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
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
h : W.HasRightCalculusOfFractions
X' X Y : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.op s
eq : s ≫ f₁ = s ≫ f₂
Y' : C
t : Y' ⟶ Opposite.unop Y
ht : W t
fac : t ≫ f₁.unop = t ≫ f₂.unop
⊢ ∃ Y' t, ∃ (_ : W.op t), f₁ ≫ t = f₂ ≫ t

Tactic:
exact ⟨Opposite.op Y', t.op, ht, Quiver.Hom.unop_inj fac⟩

Goal state after:
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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ LeftFractionRel φ.op ψ.op

Tactic:
← LeftFraction.map_eq_iff L.op W.op φ.op ψ.op,

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ φ.op.map L.op ⋯ = ψ.op.map L.op ⋯
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 : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
⊢ (P.extensionProduct Q).retractClosure X

Tactic:
refine ⟨X', ⟨_, _, _, _, _, 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 : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
⊢ Retract X X'
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.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : P Z
⊢ P T.obj₃

Tactic:
obtain ⟨e, _⟩ := exists_iso_of_arrow_iso _ _ hT' hT (Iso.refl _)

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.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : P Z
e : Triangle.mk T.mor₁ g h ≅ T
h✝ :
  e.hom.hom₁ = Arrow.Hom.left (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom ∧
    e.hom.hom₂ = Arrow.Hom.right (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom
⊢ P T.obj₃
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 : ℤ
⊢ (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯) +
          (↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯).v
      p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯

Tactic:
dsimp [mappingConeCompTriangle, map]

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 : ℤ
⊢ (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯)).v p (p + 1) ⋯ +
      ((↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯)).comp
            (Cochain.ofHom
              (Triangle.mk
                  (desc f ((Cochain.ofHom (𝟙 X₁)).comp (inl (f ≫ g)) mapOfHomotopy._proof_2) (g ≫ inr (f ≫ g)) ⋯)
                  (desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) mapOfHomotopy._proof_2) (𝟙 X₃ ≫ inr g) ⋯)
                  ((triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (inr f))).mor₁)
            ⋯).v
        p (p + 1) ⋯ =
    0
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ IsIso (Qh.map f) → HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f → IsIso (Qh.map f)

Tactic:
· intro hf
    rw [HomotopyCategory.mem_quasiIso_iff]
    intro n
    rw [← NatIso.isIso_map_iff (homologyFunctorFactorsh C n) f]
    dsimp
    infer_instance

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f → IsIso (Qh.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₃
⊢ hom f g ≫ inv f g = 𝟙 (mappingCone g)

Tactic:
by
  ext n
  simp [hom, inv, lift_desc_f _ _ _ _ _ _ _ n (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

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₂
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (fst φ).f p₂ = α.v p₁ p₂ h₁₂

Tactic:
simp [liftCochain, mappingCocone, fst,
    Cochain.rightShift_v (n := m) _ _ _ _ p₁ _ _ (p₂ + -1) (by lia),
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p₂ _ (p₂ + -1) (by lia)]

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

Goal state before:
pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)

Tactic:
exact e.rel

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
⊢ c'.next (e.f j) = e.f k

Tactic:
by_cases hj : c'.Rel (e.f j) (c'.next (e.f j))

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k
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 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
⊢ (K.iCycles j' ≫ (K.restrictionXIso e hj').inv) ≫ (K.restriction e).d j k = 0

Tactic:
rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_comp]

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 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
⊢ (K.restriction e).liftCycles (K.iCycles j' ≫ (K.restrictionXIso e hj').inv) k hk ⋯ ≫
      K.liftCycles ((K.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom) k' hk'' ⋯ =
    𝟙 (K.cycles j')

Tactic:
simp [← cancel_mono (K.iCycles j')]

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.sc j).iCycles = (K.sc j).homologyData.left.cyclesIso.hom ≫ (K.sc j).homologyData.left.i

Tactic:
ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i

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 : 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.sc j).iCycles = (K.sc j).iCycles