mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
suffices IsIso φ'.hom₃ by
    have : IsIso φ' := by
      apply Triangle.isIso_of_isIsos
      all_goals infer_instance
    exact isomorphic_distinguished _ hT' _ (asIso φ').symm

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₁)
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₂
⊢ IsIso φ'.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 : ℤ
⊢ lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n) ((snd φ).shift n)
        ⋯ ≫
      desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯ =
    𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))

Tactic:
ext p
    dsimp
    simp only [Int.reduceNeg, lift_desc_f _ _ _ _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X',
      Cocycle.coe_units_smul, Cocycle.shift_coe, Cochain.units_smul_v, Cochain.shift_v',
      Linear.comp_units_smul, Linear.units_smul_comp, smul_smul, Int.units_mul_self, one_smul,
      shiftFunctor_map_f', id_X]

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
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T₁ ≅ CochainComplex.mappingCone.triangleh f
⊢ T₂ ∈ distinguishedTriangles C

Tactic:
exact ⟨X, Y, f, ⟨e ≪≫ e'⟩⟩

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
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:
by dsimp [φ]; infer_instance

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
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:
by dsimp [φ]; infer_instance

Goal state after:
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
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
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₂ ≫ 𝟙 X₃ = u₁₂ ≫ (Triangle.mk v₂₃ u₂₃ w₂₃).mor₂

Tactic:
dsimp
    rw [comp_id, comm]

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

Goal state before:
pp: case mpr.cons
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (p.cons g))

Tactic:
show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl,

Goal state after:
case mpr.cons
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (p' ≫ g.toPath))
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (X Y : W.FunctorsInverting D) (f : X ⟶ Y),
    (inverse W D ⋙ functor W D).map f = eqToHom ⋯ ≫ (𝟭 (W.FunctorsInverting D)).map f ≫ eqToHom ⋯

Tactic:
· rintro ⟨G₁, hG₁⟩ ⟨G₂, hG₂⟩ f
        ext
        dsimp
        -- Why does `rw` work but not `simp`?
        rw [NatTransExtension.app_eq, InducedCategory.eqToHom_hom,
          InducedCategory.eqToHom_hom]
        simp

Goal state after:
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ AreEqualizedByLocalization W f g ↔ L.map f = L.map g

Tactic:
dsimp [AreEqualizedByLocalization]

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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ W.Q.map f = W.Q.map g ↔ L.map f = L.map g
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.inverseImage Φ.functor.asEquivalence.symm.functor

Tactic:
erw [W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor.asEquivalence.functor
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ add' W f (L.map 0) = f

Tactic:
obtain ⟨α, hα⟩ := exists_leftFraction L W f

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✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ add' W f (L.map 0) = f
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ L.map 0 = { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.snd.map L ⋯

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.add.map L ⋯ = α.map L ⋯

Tactic:
· rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp,
      LeftFraction.map_comp_map_s]

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✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.add.map L ⋯ = α.map L ⋯
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
    F'.map (L.map ((shiftFunctorAdd C a b).inv.app X)) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C (a + b)).obj X) ≫
        F.map ((shiftFunctorAdd C a b).hom.app X) ≫
          (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
            (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctorAdd E a b).inv.app (F.obj X) ≫
                (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)

Tactic:
erw [← NatTrans.naturality_assoc]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
    F'.map (L.map ((shiftFunctorAdd C a b).inv.app X)) ≫
      (L ⋙ F').map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
          (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
            (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctorAdd E a b).inv.app (F.obj X) ≫
                (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
obtain ⟨α, hα⟩ := exists_leftFraction L W f

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✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map ((shiftFunctor D b).map ((commShiftIso L a).hom.app X)) ≫
    (commShiftOfLocalization.iso L W F F' b).hom.app ((shiftFunctor D a).obj (L.obj X)) ≫
      (shiftFunctor E b).map (F'.map ((commShiftIso L a).inv.app X)) ≫
        (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
          (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
            (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
              (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))

Tactic:
erw [← NatTrans.naturality_assoc]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map ((shiftFunctor D b).map ((commShiftIso L a).hom.app X)) ≫
    (shiftFunctor D b ⋙ F').map ((commShiftIso L a).inv.app X) ≫
      (commShiftOfLocalization.iso L W F F' b).hom.app (L.obj ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
          (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
            (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
              (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f'' = ψ.thd.map L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), hβ]
    nth_rw 1 [L.map_comp]
    rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]

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

Goal state before:
pp: case refine_2.refine_3.refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
Z : C
u : w₂.Y' ⟶ Z
hu : W u
fac₄ : z₂.f ≫ w₂.s ≫ u = t₂ ≫ w₂.f ≫ u
⊢ p₂.s ≫ u = (a₂.comp₀ b z₂).s ≫ w₂.s ≫ u

Tactic:
dsimp [p₁, p₂]
        simp only [assoc]

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map ((Q W).map f.s ≫ Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
Qiso_hom_inv_id,

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (𝟙 ((Q W).obj Y)) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
      f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (inv_rot_of_distTriang _ hT) n₁)

Goal state after:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
      X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
      g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ } ≅
    { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
      f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ }
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁶ : Category.{v_3, u_3} E
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
inst✝² : HasShift E M
X Y : C
a : M
f : ShiftedHom X Y a
F : C ⥤ D
inst✝¹ : F.CommShift M
G : D ⥤ E
inst✝ : G.CommShift M
⊢ f.map (F ⋙ G) = (f.map F).map G

Tactic:
simp [map, Functor.commShiftIso_comp_hom_app]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
⊢ (Triangle.mk f₁ f₂ f₃).mor₃ ≫ (shiftFunctor C 1).map a₁ =
    a₃ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₃

Tactic:
by dsimp; grind

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ = a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁
ha₂₃ : (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ = a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂
⊢ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₃ ≫ (shiftFunctor C 1).map b₁ =
    b₃ ≫ (Triangle.mk f₁ f₂ f₃).mor₃

Tactic:
by dsimp; grind

Goal state after: