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 m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).inv.app X ≫ (shiftFunctorCompIsoId C n m h).hom.app X) =
    (shiftFunctorCompIsoId C m n ⋯).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).hom.app X)

Tactic:
Iso.inv_hom_id_app,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map (𝟙 ((𝟭 C).obj X)) =
    (shiftFunctorCompIsoId C m n ⋯).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).hom.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)

Tactic:
rw [← cancel_mono ((shiftFunctorAdd' C p' p 0 hp).inv.app X), Iso.hom_inv_id_app,
    Category.assoc, Category.assoc, Category.assoc, Category.assoc,
    ← shiftFunctorAdd'_assoc_inv_app p' m n n' p 0
      (by rw [← add_left_inj n, hn, add_assoc, h, hp]) h (by rw [add_assoc, h, hp]),
    ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc,
    Category.assoc, Category.assoc,
    shiftFunctorAdd'_assoc_inv_app n' m' m p' 0 n' _ hm
      (by rw [add_assoc, hm, add_zero]), Iso.hom_inv_id_app_assoc,
    ← shiftFunctorAdd'_add_zero_hom_app, Iso.hom_inv_id_app,
    Functor.map_id, Category.id_comp, Iso.hom_inv_id_app]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫
      (shiftFunctorComm C n 0).inv.app X ≫ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)

Tactic:
Iso.inv_hom_id_app,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫
      (shiftFunctorComm C n 0).inv.app X ≫ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map ((i (m₁ + m₂)).inv.app X ≫ (i (m₁ + m₂)).hom.app X) ≫
          (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))

Tactic:
Iso.inv_hom_id_app,

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map (𝟙 ((F ⋙ shiftFunctor D (m₁ + m₂)).obj X)) ≫
          (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).pOpcycles ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) = K.pOpcycles j

Tactic:
simp only [ShortComplex.p_opcyclesMap, shortComplexFunctor'_obj_X₂, shortComplexFunctor_obj_X₂,
    natIsoSc'_inv_app_τ₂, id_comp]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc j).pOpcycles = K.pOpcycles j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: 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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
rw [← cancel_mono (XIso φ i hi).hom]
  simpa only [sndX, dif_neg hi] using h

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 φ
p q : ℤ
hpq : p + -1 = q
⊢ (ComplexShape.up ℤ).Rel q p

Tactic:
by dsimp; lia

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 φ
⊢ δ 1 2 (Cochain.mk fun p q hpq ↦ homotopyCofiber.fstX φ p q hpq) = 0

Tactic:
ext p _ 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 φ
p : ℤ
⊢ (δ 1 2 (Cochain.mk fun p q hpq ↦ homotopyCofiber.fstX φ p q hpq)).v p (p + 2) ⋯ = Cochain.v 0 p (p + 2) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (ComplexShape.up ℤ).Rel j i

Tactic:
by dsimp; lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (ComplexShape.up ℤ).Rel i k

Tactic:
by dsimp; lia

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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ φ₁.f p =
    (F.d p (p + 1) ≫ if hij : p + 1 + -1 = p then (↑z).v (p + 1) p hij else 0) +
        (if hij : p + -1 = p - 1 then (↑z).v p (p - 1) hij else 0) ≫ G.d (p - 1) p +
      φ₂.f p

Tactic:
eq,

Goal state after:
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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p =
    (F.d p (p + 1) ≫ if hij : p + 1 + -1 = p then (↑z).v (p + 1) p hij else 0) +
        (if hij : p + -1 = p - 1 then (↑z).v p (p - 1) hij else 0) ≫ G.d (p - 1) p +
      φ₂.f p
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n✝ + 1)).fst =
    (toPrev (n✝ + 1)) fun i j ↦
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0

Tactic:
· dsimp [toPrev]
        simp only [CochainComplex.prev_nat_succ, dite_true]
        rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]
        dsimp [xPrevIso]
        rw [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Unique C
a : Quotient r
⊢ a = default

Tactic:
ext; subsingleton

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.inv ≫ Quot.out i.hom) = (quotient V c).map (𝟙 D)

Tactic:
rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
⊢ (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
have h : whiskerLeft F (zero F s i).hom = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
  exact (NatTrans.congr_app h X).trans (by simp)

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫
          F.map ((shiftFunctorAdd C n 0).hom.app X) ≫
            (i 0).inv.app ((shiftFunctor C n).obj X) ≫ (s 0).map ((i n).inv.app X ≫ (i n).hom.app X) =
    (eqToHom ⋯).app (F.obj X) ≫ (Induced.zero F s i).inv.app ((s n).obj (F.obj X)) ≫ (s 0).map ((i n).hom.app X)

Tactic:
Iso.inv_hom_id_app,

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫
          F.map ((shiftFunctorAdd C n 0).hom.app X) ≫
            (i 0).inv.app ((shiftFunctor C n).obj X) ≫ (s 0).map (𝟙 ((shiftFunctor C n ⋙ F).obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫ (Induced.zero F s i).inv.app ((s n).obj (F.obj X)) ≫ (s 0).map ((i n).hom.app X)
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
⊢ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
by
  simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_inv_app_obj]

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 ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
⊢ δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'

Tactic:
by
  obtain ⟨γ', rfl⟩ := (rightShiftAddEquiv K L n a n' hn).surjective γ
  dsimp
  simp only [rightUnshift_rightShift, γ'.δ_rightShift a n' m' hn m hm', rightUnshift_units_smul,
    smul_smul, Int.units_mul_self, one_smul]

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 : ℤ
z : Cocycle K L n
K' : CochainComplex C ℤ
g : K' ⟶ K
⊢ equivHomShift (equivHomShift.symm (z.precomp g)) = equivHomShift (g ≫ equivHomShift.symm z)

Tactic:
simp [equivHomShift_comp]

Goal state after:
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
g : A ⟶ T.obj₁
hf : (g ≫ T.mor₁) ≫ φ.hom₂ = 0
⊢ g ≫ T.mor₁ = 0

Tactic:
rw [assoc] at hf

Goal state after:
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
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ g ≫ 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
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = (shiftFunctor C (-1)).map φ.hom₃ ≫ T'.invRotate.mor₁
⊢ h ≫ inv ((shiftFunctor C (-1)).map φ.hom₃) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁

Tactic:
eq,

Goal state after:
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
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = (shiftFunctor C (-1)).map φ.hom₃ ≫ T'.invRotate.mor₁
⊢ h ≫ inv ((shiftFunctor C (-1)).map φ.hom₃) ≫ (shiftFunctor C (-1)).map φ.hom₃ ≫ T'.invRotate.mor₁ = g ≫ φ.hom₁
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case refine_1
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₃
this : Mono φ.hom₂
A : C
⊢ Function.Injective fun x ↦ x ≫ φ.hom₂

pp: case refine_2
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₃
this : Mono φ.hom₂
A : C
⊢ Function.Surjective fun x ↦ x ≫ φ.hom₂

Tactic:
· intro f₁ f₂ h
    simpa only [← cancel_mono φ.hom₂] using h

Goal state after:
case refine_2
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₃
this : Mono φ.hom₂
A : C
⊢ Function.Surjective fun x ↦ x ≫ φ.hom₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ δ (-1) 0 (n.negOnePow • (inl φ).shift n) =
    Cochain.ofHom
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ ≫
        (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ))

Tactic:
by
    ext p
    dsimp
    simp only [Int.reduceNeg, δ_units_smul, Cochain.δ_shift, δ_inl, Cochain.ofHom_comp, smul_smul,
      Int.units_mul_self, one_smul, Cochain.shift_v', Cochain.comp_zero_cochain_v,
      Cochain.ofHom_v, shiftFunctor_obj_X', shiftFunctor_map_f']

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
⊢ δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r) = 0

Tactic:
ext p _ rfl

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 : ℤ
⊢ (δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)).v p (p + 2) ⋯ = Cochain.v 0 p (p + 2) ⋯
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 Y : C
⊢ F.map 0 = 0

Tactic:
by
    have h₁ : (0 : X ⟶ Y) = 0 ≫ 𝟙 0 ≫ 0 := by simp
    have h₂ : 𝟙 (F.obj 0) = 0 := by
      rw [← IsZero.iff_id_eq_zero]
      apply Triangle.isZero₃_of_isIso₁ _
        (F.map_distinguished _ (contractible_distinguished (0 : C)))
      dsimp
      infer_instance
    rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]

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
n : ℤ
⊢ (homOfDegreewiseSplit S σ).f n = (↑(cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯

Tactic:
simp [homOfDegreewiseSplit, Cochain.rightShift_v _ _ _ _ _ _ _ _ rfl]

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

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
F : C ⥤ D
inst✝¹¹ : F.CommShift ℤ
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasZeroObject D
inst✝⁸ : Preadditive C
inst✝⁷ : Preadditive D
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
inst✝² : F.IsTriangulated
inst✝¹ : F.Full
inst✝ : F.Faithful
T : Triangle C
hT : F.mapTriangle.obj T ∈ distinguishedTriangles
⊢ T ∈ distinguishedTriangles

Tactic:
obtain ⟨Z, g, h, mem⟩ := distinguished_cocone_triangle T.mor₁

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
F : C ⥤ D
inst✝¹¹ : F.CommShift ℤ
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasZeroObject D
inst✝⁸ : Preadditive C
inst✝⁷ : Preadditive D
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
inst✝² : F.IsTriangulated
inst✝¹ : F.Full
inst✝ : F.Faithful
T : Triangle C
hT : F.mapTriangle.obj T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
mem : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
⊢ T ∈ distinguishedTriangles