mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_2
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 : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom =
    (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom =
    (shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃

Tactic:
· ext p
    dsimp
    simp only [Units.smul_def, shiftIso, Int.reduceNeg, Linear.smul_comp, id_comp,
      ext_to_iff _ _ (p + 1) rfl, shiftFunctor_obj_X', assoc, lift_f_fst_v, Cocycle.coe_smul,
      Cocycle.shift_coe, Cochain.smul_v, Cochain.shift_v', Linear.comp_smul, inr_f_fst_v,
      smul_zero, lift_f_snd_v, inr_f_snd_v, and_true]

Goal state after:
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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom =
    (shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_2
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
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₂ ≫
      (mapHomologicalComplexIso φ G).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₂

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
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) 1).map
        (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Tactic:
· dsimp
    rw [map_inr, id_comp]

Goal state after:
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
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) 1).map
        (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: case mp
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₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₁.IsTriangulated → F₂.IsTriangulated

pp: case mpr
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₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₂.IsTriangulated → F₁.IsTriangulated

Tactic:
· intro
    exact isTriangulated_of_iso e

Goal state after:
case mpr
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₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₂.IsTriangulated → F₁.IsTriangulated
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
inst✝ : HasBinaryBiproducts C
n : ℤ
h : S.f.f (n + 1) ≫ (σ (n + 1)).r = 𝟙 (S.X₁.X (n + 1))
⊢ S.f.f (n + 1) ≫
      (S.g.f (n + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (n + 1) n ⋯ -
        (σ (n + 1)).r ≫ 𝟙 (S.X₁.X (n + 1)) ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f n) =
    -(mappingCone.inr (homOfDegreewiseSplit S σ)).f n

Tactic:
rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]

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.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
⊢ S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0

Tactic:
← p_opcyclesMap_assoc,

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.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
⊢ S.X₁.pOpcycles i ≫ opcyclesMap S.f i ≫ k = 0
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ (𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X

Tactic:
cases X

Goal state after:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (𝟭 (Quotient (pathsHomRel C))).obj { as := as✝ } ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj { as := as✝ }
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ (quotientPathsTo C).map
        ((NatIso.ofComponents
                (fun X ↦
                  Quotient.casesOn (motive := fun t ↦
                    X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
                    (fun as h ↦ ⋯ ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as })) ⋯)
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj x)) ⋯).hom.app
        ((quotientPathsTo C).obj X) =
    𝟙 ((quotientPathsTo C).obj X)

Tactic:
cases X

Goal state after:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (quotientPathsTo C).map
        ((NatIso.ofComponents
                (fun X ↦
                  Quotient.casesOn (motive := fun t ↦
                    X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
                    (fun as h ↦ ⋯ ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as })) ⋯)
                ⋯).hom.app
          { as := as✝ }) ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj x)) ⋯).hom.app
        ((quotientPathsTo C).obj { as := as✝ }) =
    𝟙 ((quotientPathsTo C).obj { as := as✝ })
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
by
  rw [← Prefunctor.comp_map]
  exact (Prefunctor.congr_hom e.inv_hom_id.symm f).symm

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

Goal state before:
pp: case refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X : Paths (LocQuiver W)
⊢ (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X

Tactic:
cases X

Goal state after:
case refine_1.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
obj✝ : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj { obj := obj✝ } = (Quotient.functor (relations W) ⋙ G₂).obj { obj := obj✝ }
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
X : C
⊢ (commShiftOfLocalization.iso L W F F' 0).hom.app (L.obj X) = (CommShift.isoZero F' A).hom.app (L.obj X)

Tactic:
simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_zero,
      CommShift.isoZero_inv_app, map_comp, CommShift.isoZero_hom_app, Category.assoc,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality]

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
X : C
⊢ F'.map ((shiftFunctorZero D A).hom.app (L.obj X)) ≫
      F'.map (L.map ((shiftFunctorZero C A).inv.app X)) ≫
        (L ⋙ F').map ((shiftFunctorZero C A).hom.app X) ≫
          (Lifting.iso L W F F').hom.app X ≫
            (𝟭 E).map ((Lifting.iso L W F F').inv.app X) ≫ (shiftFunctorZero E A).inv.app (F'.obj (L.obj X)) =
    F'.map ((shiftFunctorZero D A).hom.app (L.obj X)) ≫ (shiftFunctorZero E A).inv.app (F'.obj (L.obj X))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case 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 : W.LeftFraction X Y) (b₁ b₂ : W.LeftFraction Y Z), LeftFractionRel b₁ b₂ → a.comp b₁ = a.comp b₂

pp: case refine_2
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), LeftFractionRel a₁ a₂ → a₁.comp b = a₂.comp b

Tactic:
· rintro a b₁ b₂ ⟨U, t₁, t₂, hst, hft, ht⟩
    obtain ⟨z₁, fac₁⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₁.f)
    obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₂.f)
    obtain ⟨w₁, fac₁'⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs t₁)
    obtain ⟨w₂, fac₂'⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs t₂)
    obtain ⟨u, fac₃⟩ := exists_leftFraction (RightFraction.mk w₁.s w₁.hs w₂.s)
    dsimp at fac₁ fac₂ fac₁' fac₂' fac₃ ⊢
    have eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s := by
      rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
    obtain ⟨Z, p, hp, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a.hs eq
    simp only [assoc] at fac₄
    rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]
    apply Quot.sound
    refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ p, ?_, ?_, ?_⟩
    · dsimp
      simp only [assoc, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hst, reassoc_of% fac₃]
    · dsimp
      simp only [assoc, fac₄]
    · dsimp
      simp only [assoc]
      rw [← reassoc_of% fac₁', ← reassoc_of% fac₃, ← assoc]
      exact W.comp_mem _ _ ht (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ u.hs hp))

Goal state after:
case refine_2
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), LeftFractionRel a₁ a₂ → a₁.comp b = a₂.comp b
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2
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₁ : { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.f ≫ z₁.s = { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.s ≫ z₁.f
⊢ a₁.comp b = a₂.comp b

Tactic:
obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a₂.s a₂.hs b.f)

Goal state after:
case refine_2
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₁ : { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.f ≫ z₁.s = { X' := Y, s := a₁.s, hs := ⋯, f := b.f }.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.f ≫ z₂.s = { X' := Y, s := a₂.s, hs := ⋯, f := b.f }.s ≫ z₂.f
⊢ a₁.comp b = a₂.comp b
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
C₁ : Type u_1
C₂ : Type u_2
inst✝¹² : Category.{v_1, u_1} C₁
inst✝¹¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C₁ M
inst✝⁸ : HasShift C₂ M
inst✝⁷ : Φ.functor.CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{v_3, u_4} D₁
inst✝⁵ : Category.{v_4, u_5} D₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : HasShift D₁ M
inst✝² : HasShift D₂ M
inst✝¹ : L₁.CommShift M
inst✝ : L₂.CommShift M
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
⊢ G.CommShift M

Tactic:
letI : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := ⟨e.symm⟩

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
C₁ : Type u_1
C₂ : Type u_2
inst✝¹² : Category.{v_1, u_1} C₁
inst✝¹¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C₁ M
inst✝⁸ : HasShift C₂ M
inst✝⁷ : Φ.functor.CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{v_3, u_4} D₁
inst✝⁵ : Category.{v_4, u_5} D₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : HasShift D₁ M
inst✝² : HasShift D₂ M
inst✝¹ : L₁.CommShift M
inst✝ : L₂.CommShift M
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
this : Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso := e.symm }
⊢ G.CommShift M
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case mpr
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.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ (∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂

Tactic:
· rintro ⟨Z, s, hs, fac⟩
    simp only [← cancel_epi (Localization.isoOfHom L W s hs).hom,
      Localization.isoOfHom_hom, ← L.map_comp, fac]

Goal state after:
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
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α ≫ (-(shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z) =
    -α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
Preadditive.comp_neg

Goal state after:
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
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ -α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    -α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: case mpr
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ L.essImageDistTriang → T ∈ distinguishedTriangles

Tactic:
rintro ⟨T₀, e, hT₀⟩

Goal state after:
case mpr
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
T₀ : Triangle C
e : T ≅ L.mapTriangle.obj T₀
hT₀ : T₀ ∈ distinguishedTriangles
⊢ T ∈ distinguishedTriangles
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 : ObjectProperty C
inst✝ : IsTriangulated C
n : ℕ
⊢ P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P

Tactic:
induction n with
  | zero => rfl
  | succ n h =>
    rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← h]

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

Goal state before:
pp: case succ
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 : ObjectProperty C
n : ℕ
H : P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
⊢ P.retractClosure.extensionProduct (P.retractClosure.extensionProductIter n) ≤
    (P.extensionProduct (P.extensionProductIter n)).retractClosure

Tactic:
monotone_extensionProduct_right _ H,

Goal state after:
case succ
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 : ObjectProperty C
n : ℕ
H : P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
⊢ P.retractClosure.extensionProduct (P.extensionProductIter n).retractClosure ≤
    (P.extensionProduct (P.extensionProductIter n)).retractClosure
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ HomologicalComplex.quasiIso C c f

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff, quasiIso_iff]

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ ∀ (i : ι), QuasiIsoAt f i