mathlib-initiative/mathlib-tactics huggingface dataset:
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 : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ δ n m ↑z = 0

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m ↑z = 0

Tactic:
· rw [← mem_iff n m h]
    exact z.2

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m ↑z = 0
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 φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ (lift φ α β eq).f p = (↑α).v p q hpq ≫ (inl φ).v q p ⋯ + β.v p p ⋯ ≫ (inr φ).f p

Tactic:
by
  simp [ext_to_iff _ _ _ hpq]

Goal state after:
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 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''
i : ℕ
⊢ i + 1 = (ComplexShape.up ℕ).next i

Tactic:
by simp only [CochainComplex.next]

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

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
⊢ (isoAdd' ⋯ (isoZero F A) e).hom.app X = e.hom.app X

Tactic:
have := e.hom.naturality ((shiftFunctorZero C A).inv.app X)

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
this :
  (shiftFunctor C a ⋙ F).map ((shiftFunctorZero C A).inv.app X) ≫ e.hom.app ((shiftFunctor C 0).obj X) =
    e.hom.app ((𝟭 C).obj X) ≫ (F ⋙ shiftFunctor D a).map ((shiftFunctorZero C A).inv.app X)
⊢ (isoAdd' ⋯ (isoZero F A) e).hom.app X = e.hom.app X
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 : ℤ
γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

Tactic:
by
  change (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _
  apply map_add

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁

Tactic:
by rw [← comp_hom₁, e.inv_hom_id, id_hom₁]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f g : T₁ ⟶ T₂
⊢ f - g = f + -g

Tactic:
by ext <;> apply sub_eq_add_neg

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} E
inst✝¹² : Category.{v_4, u_4} J
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : D ⥤ E
τ'' : G ⟶ G'
H : E ⥤ J
A : Type u_5
inst✝¹¹ : AddMonoid A
inst✝¹⁰ : HasShift C A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
inst✝⁷ : HasShift J A
inst✝⁶ : F₁.CommShift A
inst✝⁵ : F₂.CommShift A
inst✝⁴ : F₃.CommShift A
inst✝³ : G.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : H.CommShift A
inst✝ : CommShift τ A
a : A
X : C
⊢ ((Functor.commShiftIso (F₁ ⋙ G) a).hom ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a)).app X =
    ((shiftFunctor C a).whiskerLeft (Functor.whiskerRight τ G) ≫ (Functor.commShiftIso (F₂ ⋙ G) a).hom).app X

Tactic:
simp only [Functor.whiskerRight_twice, comp_app, Functor.commShiftIso_comp_hom_app,
    Functor.associator_hom_app, Functor.whiskerRight_app, Functor.comp_map,
    Functor.associator_inv_app, comp_id, id_comp, assoc, ← Functor.commShiftIso_hom_naturality, ←
    G.map_comp_assoc, shift_app_comm, Functor.whiskerLeft_app]

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 : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
obtain ⟨c, hc⟩ :=
    complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁)
      T.mor₁ rfl

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 : Triangle C
H : T ∈ distinguishedTriangles
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ 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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
refine (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_
  dsimp
  simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]
  tauto

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

Goal state before:
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
⊢ IsIso T.mor₂ → T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
intro
    rw [T.mor₁_eq_zero_iff_mono₂ hT, T.mor₃_eq_zero_iff_epi₂ hT]
    constructor <;> infer_instance

Goal state after:
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
p q : ℤ
hpq : p + -1 = q
⊢ p = q + 1

Tactic:
by rw [← hpq, neg_add_cancel_right]

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₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
⊢ a ≫ (productTriangle T).mor₃ ≫ (shiftFunctor C 1).map (productTriangle.π T j).hom₁ -
      a' ≫ T'.mor₃ ≫ (shiftFunctor C 1).map φ'.hom₁ ≫ (shiftFunctor C 1).map (productTriangle.π T j).hom₁ =
    0

Tactic:
rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_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✝¹⁶ : 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
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁴ : H.CommShift ℤ
inst✝³ : H.IsTriangulated
inst✝² : F.IsTriangulated
inst✝¹ : F.mapArrow.EssSurj
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ G.IsTriangulated

Tactic:
have := (isTriangulated_iff_of_iso e).2 inferInstance

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
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁴ : H.CommShift ℤ
inst✝³ : H.IsTriangulated
inst✝² : F.IsTriangulated
inst✝¹ : F.mapArrow.EssSurj
inst✝ : NatTrans.CommShift e.hom ℤ
this : (F ⋙ G).IsTriangulated
⊢ G.IsTriangulated
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
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₂ = e₂.hom
| h.choose.hom.hom₂ ≫ T₂.mor₂

Tactic:
← TriangleMorphism.comm₂

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
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₂ = e₂.hom
| T₁.mor₂ ≫ h.choose.hom.hom₃
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ o.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
eq₂ :
  o.m₁ ≫ (-(shiftFunctor C 1).map (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) =
    -(shiftFunctor C 1).map (Triangle.mk v₁₂ u₁₂ w₁₂).mor₁
eq₃ : (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃ ≫ o.m₃ = (Triangle.mk v₂₃ u₂₃ w₂₃).mor₃
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃

Tactic:
have eq₄ := o.comm₄

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ o.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
eq₂ :
  o.m₁ ≫ (-(shiftFunctor C 1).map (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) =
    -(shiftFunctor C 1).map (Triangle.mk v₁₂ u₁₂ w₁₂).mor₁
eq₃ : (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃ ≫ o.m₃ = (Triangle.mk v₂₃ u₂₃ w₂₃).mor₃
eq₄ :
  (-(shiftFunctor C 1).map (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) ≫ (shiftFunctor C 1).map u₁₂ =
    o.m₃ ≫ (-(shiftFunctor C 1).map (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁)
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) ≫ (eqToHom ⋯).hom.app x✝ =
    (eqToHom ⋯).hom.app x✝ ≫ ((whiskeringLeftFunctor L W E).map τ).hom.app x✝

Tactic:
rw [ObjectProperty.eqToHom_hom, ObjectProperty.eqToHom_hom, eqToHom_app, eqToHom_app,
          eqToHom_refl, eqToHom_refl]

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) ≫
      𝟙 (((Construction.WhiskeringLeftEquivalence.functor W E).obj (Construction.lift L ⋯ ⋙ Y✝)).obj.obj x✝) =
    𝟙 (((Construction.WhiskeringLeftEquivalence.functor W E).obj (Construction.lift L ⋯ ⋙ X✝)).obj.obj x✝) ≫
      ((whiskeringLeftFunctor L W E).map τ).hom.app x✝
Module: Mathlib.CategoryTheory.Localization.Predicate

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
hW : W ≤ MorphismProperty.isomorphisms C
inst✝ : L.IsEquivalence
⊢ L.IsLocalization W

Tactic:
have : (𝟭 C).IsLocalization W := for_id W hW

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
hW : W ≤ MorphismProperty.isomorphisms C
inst✝ : L.IsEquivalence
this : (𝟭 C).IsLocalization W
⊢ L.IsLocalization W
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedFullyFaithful
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ Nonempty G.FullyFaithful

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

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedFullyFaithful
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful
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)
this : Small.{w, w'} ↑(Set.Iio ↑c)
⊢ ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑c) P)

Tactic:
exact hb' c.1 c.2

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ (Cone.postcompose p.diag.uniqueFromEmpty.hom).obj { pt := X, π := p.π } ≅ asEmptyCone X

Tactic:
exact Cone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩)

Goal state after:
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
⊢ ⨆ x, P.shift x ≤ P.shiftClosure G

Tactic:
intro X hX
    obtain ⟨a, ha⟩ := (prop_iSup_iff _ _).mp hX
    exact ⟨X⟦a⟧, -a, (shiftShiftNeg X a).symm, ha⟩

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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ z₂.f ≫ z₂₃.f ≫ z'.s = z₁.s ≫ z₁₂.f ≫ z'.f

Tactic:
← reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ z₂.f ≫ z₂₃.f ≫ z'.s = z₂.f ≫ z₁₂.s ≫ z'.f
Module: Mathlib.CategoryTheory.Localization.Triangulated

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
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
fac : L.map (T₁.mor₁ ≫ γ.f) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map α.f ≫ L.map β.f ≫ L.map γ.s = α.map L ⋯ ≫ L.map α.s ≫ L.map β.f ≫ L.map γ.s

Tactic:
MorphismProperty.LeftFraction.map_comp_map_s_assoc

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
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
fac : L.map (T₁.mor₁ ≫ γ.f) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map α.f ≫ L.map β.f ≫ L.map γ.s = L.map α.f ≫ L.map β.f ≫ L.map γ.s
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ 0 ⋯ f).comp g ⋯ = f ≫ g

Tactic:
simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).trW

Tactic:
rw [← HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]
  infer_instance

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ¬∃ k, e.f k = i'
⊢ e.f i = i'

Tactic:
· simp [e.r_eq_none i' (by simpa using h)] at hi

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
⊢ K.op.IsStrictlySupported e.op

Tactic:
rw [isStrictlySupported_op_iff]

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
K L : HomologicalComplex C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
⊢ K.IsStrictlySupported e