mathlib-initiative/mathlib-tactics huggingface dataset:
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 j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij

Goal state after:
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
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f = g
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 j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
⊢ f = g

Tactic:
have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij

Goal state after:
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 j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct (F.X i) (G.X j)
⊢ f = g
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₁ k₀ ≫ hom k₀ k₁ + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁

Tactic:
prevD,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₁ k₀ ≫ hom k₀ k₁ + (AddMonoidHom.mk' (fun f ↦ f k₁ (c.prev k₁) ≫ D.d (c.prev k₁) k₁) ⋯) hom =
    C.d k₁ k₀ ≫ hom k₀ k₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯)).v p q hpq =
    (z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯).v p q hpq + n₂.negOnePow • ((δ n₁ (n₁ + 1) z₁).comp z₂ ⋯).v p q hpq

Tactic:
rw [z₁.comp_v _ (add_assoc n₁ n₂ 1).symm p _ q rfl (by lia),
    Cochain.comp_v _ _ (show n₁ + 1 + n₂ = n₁ + n₂ + 1 by lia) p (p + n₁ + 1) q
      (by lia) (by lia),
    δ_v (n₁ + n₂) _ rfl (z₁.comp z₂ rfl) p q hpq (p + n₁ + n₂) _ (by lia) rfl,
    z₁.comp_v z₂ rfl p _ _ rfl rfl,
    z₁.comp_v z₂ rfl (p + 1) (p + n₁ + 1) q (by lia) (by lia),
    δ_v n₂ (n₂ + 1) rfl z₂ (p + n₁) q (by lia) (p + n₁ + n₂) _ (by lia) rfl,
    δ_v n₁ (n₁ + 1) rfl z₁ p (p + n₁ + 1) (by lia) (p + n₁) _ (by lia) rfl]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q +
      (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫
        (z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q +
          (n₂ + 1).negOnePow • G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯) +
      n₂.negOnePow •
        (z₁.v p (p + n₁) ⋯ ≫ G.d (p + n₁) (p + n₁ + 1) +
            (n₁ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯) ≫
          z₂.v (p + n₁ + 1) q ⋯
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 ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j

Tactic:
← cancel_epi (biprodXIso K K j).inv

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ (K.biprodXIso K j).inv ≫
      biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j

Tactic:
← cancel_epi (biprodXIso K K j).inv

Goal state after:
case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ (K.biprodXIso K j).inv ≫
      biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (K.biprodXIso K j).inv ≫
      ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)
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 φ)
⊢ (H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ H).hom =
    inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

Tactic:
ext n
  dsimp [mapHomologicalComplexIso]
  simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl, mappingCone.ext_to_iff _ _ _ rfl,
    Functor.mapHomologicalComplex_obj_X, mapHomologicalComplexXIso'_hom, comp_add,
    add_comp, assoc, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero, add_zero, inl_v_snd_v,
    inr_f_snd_v, zero_add, ← H.map_comp, H.map_zero, H.map_id, and_self]

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : 𝟙 ((quotient V c).obj C) = 0
⊢ (quotient V c).map (𝟙 C) = (quotient V c).map 0

Tactic:
by simp [h]

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

Goal state before:
pp: case mp
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : 𝟙 ((quotient V c).obj C) = 0
⊢ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
exact ⟨(homotopyOfEq _ _ (by simp [h]))⟩

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
n : ℤ
h : n = 0
K : CochainComplex C ℤ
x✝² x✝¹ : ℤ
x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹
⊢ (K.shiftFunctorObjXIso n x✝² x✝² ⋯).hom ≫ ((𝟭 (CochainComplex C ℤ)).obj K).d x✝² x✝¹ =
    ((shiftFunctor C n).obj K).d x✝² x✝¹ ≫ (K.shiftFunctorObjXIso n x✝¹ x✝¹ ⋯).hom

Tactic:
by simp [h]

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
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ ab + c = abc

Tactic:
← hab

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
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
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ a + b + c = abc
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
eq : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ (Induced.add F s i 0 n).hom.app (F.obj X) =
    (eqToHom ⋯).app (F.obj X) ≫ (s n).map ((Induced.zero F s i).inv.app (F.obj X))

Tactic:
simp only [Induced.add_hom_app_obj, eq, shiftFunctorAdd_zero_add_hom_app,
          Functor.map_comp, eqToHom_map, Category.assoc, eqToHom_trans_assoc,
          eqToHom_refl, Category.id_comp, eqToHom_app, Induced.zero_inv_app_obj]

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
eq : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        F.map ((shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X)) ≫
          (i n).inv.app ((shiftFunctor C 0).obj X) ≫ (s n).map ((i 0).inv.app X) =
    eqToHom ⋯ ≫ (s n).map (F.map ((shiftFunctorZero C A).inv.app X)) ≫ (s n).map ((i 0).inv.app X)
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁
comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂
comm₃ : A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃
⊢ B.mor₁ ≫ iso₂.inv = iso₁.inv ≫ A.mor₁

Tactic:
simp only [← cancel_mono iso₂.hom, assoc, Iso.inv_hom_id, comp_id,
      comm₁, Iso.inv_hom_id_assoc]

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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₃ = 0 ↔ Mono T.mor₁

Tactic:
have h := mor₁_eq_zero_iff_mono₂ _ (inv_rot_of_distTriang _ hT)
  dsimp at h
  rw [← h, neg_eq_zero, IsIso.comp_right_eq_zero]
  exact (Functor.map_eq_zero_iff (CategoryTheory.shiftFunctor C (-1))).symm

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
X₁ X₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem : Triangle.mk inl snd 0 ∈ distinguishedTriangles
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
⊢ (𝟙 X₂ - snd ≫ inr) ≫ snd = 0

Tactic:
simp only [sub_comp, assoc, id_comp, ← inr_snd, comp_id, sub_self]

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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
hT' : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
let T' := Triangle.mk f₁ f₂ f₃

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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
hT' : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
T' : Triangle C := Triangle.mk f₁ f₂ f₃
⊢ productTriangle T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T.rotate ∈ distinguishedTriangles C → T ∈ distinguishedTriangles C

Tactic:
intro hT

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T.rotate ∈ distinguishedTriangles C
⊢ T ∈ distinguishedTriangles C
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) ≫ S.f.f (p + 2) +
      S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r ≫ S.f.f (p + 2) =
    0

Tactic:
← S.f.comm,

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.f.f (p + 1) ≫ 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 ≫ S.f.f (p + 2) =
    0
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles → ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
intro hT

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
⊢ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
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 ℤ
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
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
inst✝³ : F.IsTriangulated
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : IsTriangulated D
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
H : Octahedron comm' ⋯ ⋯ ⋯ := someOctahedron comm' ⋯ ⋯ ⋯
⊢ F.map (F.preimage H.m₁ ≫ w₁₃) = F.map w₁₂

Tactic:
by
          simpa [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app X₁)] using H.comm₂

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
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
⊢ x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k

Tactic:
← S.f.comm,

Goal state after:
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
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
⊢ x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
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
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ φ.map L hL ≫ L.map φ.s = L.map φ.f

Tactic:
by
  let := hL _ φ.hs
  simp [map]

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
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ L.map φ.s ≫ φ.map L hL = L.map φ.f

Tactic:
by
  let := hL _ φ.hs
  simp [map]

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

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b, ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b_1)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b_1)
hb₀ : Small.{w, w'} ↑(Set.Iio b)
c : ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑c) P)

Tactic:
have := H c.2.le

Goal state after:
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b, ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b_1)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b_1)
hb₀ : Small.{w, w'} ↑(Set.Iio b)
c : ↑(Set.Iio b)
this : Small.{w, w'} ↑(Set.Iio ↑c)
⊢ ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑c) P)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop ≤ P.colimitsClosure J

Tactic:
rw [← op_monotone_iff, op_unop]
    apply limitsClosure_le
    rw [op_monotone_iff]
    apply le_colimitsClosure

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁶ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝⁵ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (Q.limitsClosure J)

Tactic:
← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁶ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝⁵ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (Q.strictLimitsClosureIter J κ.ord).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P ≤ ⨆ x, P.shift x

Tactic:
conv_lhs => rw [← P.shift_zero G]

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P.shift 0 ≤ ⨆ x, P.shift x