mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n : A
X : C
⊢ (shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) =
    (shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((shiftFunctor C (-n)).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_hom_app

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ 1 • D a - a • D 1 = D a

Tactic:
one_smul,

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D a - a • D 1 = D a
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
I : C
inst✝ : Injective I
hij : j = i
⊢ Injective (((single C c i).obj I).X j)

Tactic:
subst hij

Goal state after:
case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
j : ι
I : C
inst✝ : Injective I
⊢ Injective (((single C c j).obj I).X j)
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
I : C
inst✝ : Injective I
⊢ Injective (((single C c i).obj I).X j)

Tactic:
by
  by_cases hij : j = i
  · subst hij
    simp only [single_obj_X_self]
    infer_instance
  · exact (isZero_single_obj_X _ _ _ _ hij).injective

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

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
P : C
inst✝ : Projective P
hij : j = i
⊢ Projective (((single C c i).obj P).X j)

Tactic:
subst hij

Goal state after:
case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
j : ι
P : C
inst✝ : Projective P
⊢ Projective (((single C c j).obj P).X j)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (((y * (algebraMap R S) r)𝖣x) + (y * x)𝖣(algebraMap R S) r) = r • y𝖣x

Tactic:
KaehlerDifferential.kerTotal_mkQ_single_algebraMap,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ ((y * (algebraMap R S) r)𝖣x) + 0 = r • y𝖣x
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
apply ext_to_X _ _ _ hj
      · simp [d_fstX φ _ _ _ hij]
      · simp [d_sndX φ _ _ hij]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : j + 1 = i
⊢ i + -1 = j

Tactic:
rw [← hij, add_neg_cancel_right]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
⊢ δ n m ↑z = 0

Tactic:
by
  by_cases h : n + 1 = m
  · rw [← mem_iff n m h]
    exact z.2
  · exact δ_shape n m h _

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Tactic:
simp [δ_comp_zero_cochain _ _ _ hnm]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (mapHomologicalComplexXIso φ H i).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d i j =
        ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d i j ≫
          (mapHomologicalComplexXIso φ H j).hom

Tactic:
rintro n _ rfl

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
      (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) =
    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
      (mapHomologicalComplexXIso φ H (n + 1)).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b : ℤ
⊢ shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
rw [← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ F.mapCochainComplexShiftIso 0 = CommShift.isoZero (F.mapHomologicalComplex (ComplexShape.up ℤ)) ℤ

Tactic:
ext
    rw [CommShift.isoZero_hom_app]
    dsimp
    simp only [CochainComplex.shiftFunctorZero_inv_app_f, CochainComplex.shiftFunctorZero_hom_app_f,
       HomologicalComplex.XIsoOfEq, eqToIso, eqToHom_map, eqToHom_trans, eqToHom_refl]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
⊢ n.negOnePow • h.hom (i + { as := n }.as) (j + { as := n }.as) = 0

Tactic:
by
    dsimp
    rw [h.zero, smul_zero]
    intro hij'
    dsimp at hij hij'
    lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow • (a * n' + a * (a - 1) / 2).negOnePow • γ.v p q hpq = γ.v p q hpq

Tactic:
smul_smul,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q hpq = γ.v p q hpq
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq

Tactic:
smul_smul,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ rightUnshift 0 n hn' = 0

Tactic:
by
  change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0
  apply map_zero

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

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
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁸ : AddMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : HasShift C A
inst✝⁵ : HasShift D A
inst✝⁴ : HasShift E A
inst✝³ : HasShift C B
inst✝² : HasShift D B
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
X : C
⊢ 𝟙 (G.obj (F.obj ((shiftFunctor C 0).obj X))) ≫
      G.map ((commShiftIso F 0).hom.app X) ≫
        𝟙 (G.obj ((shiftFunctor D 0).obj (F.obj X))) ≫
          (commShiftIso G 0).hom.app (F.obj X) ≫ 𝟙 ((shiftFunctor E 0).obj (G.obj (F.obj X))) =
    (isoZero (F ⋙ G) A).hom.app X

Tactic:
simp only [id_comp, comp_id, commShiftIso_zero, isoZero_hom_app, ← Functor.map_comp_assoc,
      assoc, Iso.inv_hom_id_app, id_obj, comp_map, comp_obj]

Goal state after:
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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    b.negOnePow •
      a.negOnePow •
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
          (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁)

Tactic:
smul_smul,

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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁)
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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    b.negOnePow •
      a.negOnePow •
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
          (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂)

Tactic:
smul_smul,

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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂)
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 •
      a.negOnePow •
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
          (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:
smul_smul,

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 * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (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.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

Tactic:
· ext p q hpq
    dsimp
    simp only [shift_v', shiftFunctor_obj_d',
      δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl,
      δ_v n m hnm _ (p + a) (q + a) (by lia) (q - 1 + a) (p + 1 + a)
        (by lia) (by lia),
      smul_add, Linear.units_smul_comp, Linear.comp_units_smul, add_right_inj]
    rw [smul_comm]

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
smul_smul,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + a * (a - 1) / 2).negOnePow) • γ.shift a
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
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
⊢ IsIso T.mor₂

Tactic:
have := T.epi₂ hT h₃

Goal state after:
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
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
⊢ IsIso T.mor₂
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
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Epi f
⊢ IsSplitEpi f

Tactic:
by
    obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
    obtain ⟨r, hr⟩ := Triangle.coyoneda_exact₂ _ hT (𝟙 _)
      (by rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, comp_zero])
    exact ⟨r, hr.symm⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ (contractibleTriangle { as := X }).mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl (contractibleTriangle { as := X }).obj₁).hom =
    h.isoZero.symm.hom ≫ (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₃

Tactic:
by dsimp; ext

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
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ ((σ p).s ≫ S.X₂.d p (p + 1) ≫ (σ (p + 1)).r) ≫ S.X₁.d (p + 1) (p + 2) +
      1 • S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r =
    0

Tactic:
one_smul,

Goal state after:
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
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ ((σ p).s ≫ S.X₂.d p (p + 1) ≫ (σ (p + 1)).r) ≫ S.X₁.d (p + 1) (p + 2) +
      S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r =
    0
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶ binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
  { hom₁ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₁, hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso φ.hom₁

Tactic:
dsimp [φ]

Goal state after:
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶ binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
  { hom₁ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₁, hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso (𝟙 (F.obj X₁))
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶ binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
  { hom₁ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₁, hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso φ.hom₃

Tactic:
dsimp [φ]

Goal state after:
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶ binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
  { hom₁ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₁, hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso (𝟙 (F.obj X₃))