mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ -(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ) =
    (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map ((rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃) ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L

Tactic:
rotateHomotopyEquiv_comm₃,

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
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ -(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ) =
    (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
          (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ) ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i j : ι
inst✝³ : K.HasHomology i
inst✝² : K.HasHomology j
inst✝¹ : L.HasHomology i
inst✝ : L.HasHomology j
⊢ opcyclesMap φ i ≫ L.opcyclesToCycles i j = K.opcyclesToCycles i j ≫ cyclesMap φ j

Tactic:
simp only [← cancel_mono (L.iCycles j), ← cancel_epi (K.pOpcycles i),
    assoc, p_opcyclesMap_assoc, pOpcycles_opcyclesToCycles_iCycles, Hom.comm, cyclesMap_i,
    pOpcycles_opcyclesToCycles_iCycles_assoc]

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✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.cycles j, f := K.homologyι i, g := K.opcyclesToCycles i j,
    zero := ⋯ }
S' : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.X j, f := K.homologyι i, g := K.fromOpcycles i j, zero := ⋯ }
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C :=
  { X₁ := K.opcycles i, X₂ := K.cycles j, X₃ := K.homology j, f := K.opcyclesToCycles i j, g := K.homologyπ j,
    zero := ⋯ }
T' : ShortComplex C :=
  { X₁ := K.X i, X₂ := K.cycles j, X₃ := K.homology j, f := K.toCycles i j, g := K.homologyπ j, zero := ⋯ }
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (composableArrows₃ K i j).Exact

Tactic:
have hT : T.Exact := by
    rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]
    exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))

Goal state after:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.cycles j, f := K.homologyι i, g := K.opcyclesToCycles i j,
    zero := ⋯ }
S' : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.X j, f := K.homologyι i, g := K.fromOpcycles i j, zero := ⋯ }
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C :=
  { X₁ := K.opcycles i, X₂ := K.cycles j, X₃ := K.homology j, f := K.opcyclesToCycles i j, g := K.homologyπ j,
    zero := ⋯ }
T' : ShortComplex C :=
  { X₁ := K.X i, X₂ := K.cycles j, X₃ := K.homology j, f := K.toCycles i j, g := K.homologyπ j, zero := ⋯ }
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (composableArrows₃ K i j).Exact
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
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ { l // opcyclesMap S.g i ≫ l = k }

Tactic:
refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩

Goal state after:
case refine_1
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
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ S.X₃.d (c.prev i) i ≫ ↑H = 0

case refine_2
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
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ opcyclesMap S.g i ≫ S.X₃.descOpcycles (↑H) (c.prev i) ⋯ ?refine_1 = k
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: 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
τ : X✝ ⟶ Y✝
⊢ W.Q ⋙ lift X✝.obj ⋯ = X✝.obj

Tactic:
rw [fac]

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

Goal state before:
pp: 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
τ : X✝ ⟶ Y✝
⊢ Y✝.obj = W.Q ⋙ lift Y✝.obj ⋯

Tactic:
rw [fac]

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
h :
  ∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'),
    ∃ X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ u₁₂ u₂₃ e₁ e₂ e₃,
      ∃ (_ : u₁₂' ≫ e₂.hom = e₁.hom ≫ u₁₂) (_ : u₂₃' ≫ e₃.hom = e₂.hom ≫ u₂₃),
        ∃ v₁₂ w₁₂,
          ∃ (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles),
            ∃ v₂₃ w₂₃,
              ∃ (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles),
                ∃ v₁₃ w₁₃,
                  ∃ (h₁₃ : Triangle.mk (u₁₂ ≫ u₂₃) v₁₃ w₁₃ ∈ distinguishedTriangles),
                    Nonempty (Octahedron ⋯ h₁₂ h₂₃ h₁₃)
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
⊢ Nonempty (Octahedron comm' h₁₂' h₂₃' h₁₃')

Tactic:
obtain ⟨X₁, X₂, X₃, Z₁₂, Z₂₃, Z₁₃, u₁₂, u₂₃, e₁, e₂, e₃, comm₁₂, comm₂₃,
      v₁₂, w₁₂, h₁₂, v₂₃, w₂₃, h₂₃, v₁₃, w₁₃, h₁₃, H⟩ := h u₁₂' u₂₃'
    exact ⟨Octahedron.ofIso u₁₂' u₂₃' u₁₃' comm' h₁₂' h₂₃' h₁₃'
      u₁₂ u₂₃ _ rfl e₁ e₂ e₃ comm₁₂ comm₂₃ v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃ v₁₃ w₁₃ h₁₃ H.some⟩

Goal state after:
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:
add'_zero

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
⊢ f = 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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
h₂ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
⊢ add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂

Tactic:
rw [h₁, h₂]

Goal state after:
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✝² : Preadditive D
inst✝¹ : L.Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
T : Triangle D
⊢ T.rotate ∈ L.essImageDistTriang → T ∈ L.essImageDistTriang

Tactic:
· rintro ⟨T', e', hT'⟩
    exact ⟨T'.invRotate, (triangleRotation D).unitIso.app T ≪≫ (invRotate D).mapIso e' ≪≫
      L.mapTriangleInvRotateIso.app T', inv_rot_of_distTriang T' hT'⟩

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isSuccLimit.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
a✝ : ∀ b < k', k ≤ b → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) b
hkj✝ : k ≤ k'
hkj : k < k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'

Tactic:
dsimp
      rw [transfiniteIterate_limit _ _ _ hk']
      exact le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩

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)
Q : ObjectProperty C
h : P ≤ Q
⊢ P.strictLimitsClosureStep J ≤ Q.strictLimitsClosureStep J

Tactic:
dsimp [strictLimitsClosureStep]
  simp only [sup_le_iff, iSup_le_iff]
  exact ⟨h.trans le_sup_left, fun a ↦
    (strictLimitsOfShape_monotone (J a) h).trans <|
      le_iSup (fun a ↦ Q.strictLimitsOfShape (J a)) a |>.trans le_sup_right⟩

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) κ
a : α
⊢ ((P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a)).isoClosure ≤
    (P.strictLimitsClosureIter J κ.ord ⊔ ⨆ a, (P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a)).isoClosure

Tactic:
exact monotone_isoClosure ((le_trans (by rfl) (le_iSup _ a)).trans le_sup_right)

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} (P.limitsClosure J)

Tactic:
have : ObjectProperty.EssentiallySmall.{w} (Q.isoClosure.limitsClosure J) := by
    rw [limitsClosure_isoClosure,
      ← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]
    infer_instance

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
this : ObjectProperty.EssentiallySmall.{w, v, u} (Q.isoClosure.limitsClosure J)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)
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₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ :
  { X' := T₂.obj₁, s := α.s, hs := ⋯, f := T₂.mor₁ }.f ≫ β.s =
    { X' := T₂.obj₁, s := α.s, hs := ⋯, f := T₂.mor₁ }.s ≫ β.f
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
obtain ⟨γ, hγ⟩ := exists_leftFraction L W (b ≫ L.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
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₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ :
  { X' := T₂.obj₁, s := α.s, hs := ⋯, f := T₂.mor₁ }.f ≫ β.s =
    { X' := T₂.obj₁, s := α.s, hs := ⋯, f := T₂.mor₁ }.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
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✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap (T.mor₃ ≫ (shiftFunctor C 1).map φ.hom₁) n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁

Tactic:
shiftMap_comp

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✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel z₁ z₂
⊢ LeftFractionRel z₁.op z₂.op

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.RightFraction X Y
Z : C
t₁ : Z ⟶ z₁.X'
t₂ : Z ⟶ z₂.X'
hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s
hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f
ht : W (t₁ ≫ z₁.s)
⊢ LeftFractionRel z₁.op z₂.op
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel z₁ z₂
⊢ LeftFractionRel z₁.unop z₂.unop

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.RightFraction X Y
Z : Cᵒᵖ
t₁ : Z ⟶ z₁.X'
t₂ : Z ⟶ z₂.X'
hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s
hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f
ht : W (t₁ ≫ z₁.s)
⊢ LeftFractionRel z₁.unop z₂.unop
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ RightFractionRel z₁.op z₂.op

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hs : z₁.s ≫ t₁ = z₂.s ≫ t₂
hf : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ RightFractionRel z₁.op z₂.op
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ RightFractionRel z₁.unop z₂.unop

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.LeftFraction X Y
Z : Cᵒᵖ
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hs : z₁.s ≫ t₁ = z₂.s ≫ t₂
hf : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ RightFractionRel z₁.unop z₂.unop
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case mp
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✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1) →
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
rintro ⟨Z, g, h, H, mem⟩
    exact ⟨_, _, _, inv_rot_of_distTriang _ H, P.le_shift (-1) _ mem⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
obtain rfl : i' = i + n := by lia

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow =
    ((imageSubobjectIso g.unop ≪≫ (imageUnopOp g).unop.symm).hom ≫
        (cokernel.desc f (factorThruImage g) ⋯).unop ≫ (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      (kernelSubobject f.unop).arrow

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelUnopUnop_inv, Category.assoc,
    imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, cokernel.π_desc, Iso.unop_inv,
    ← unop_comp, factorThruImage_comp_imageUnopOp_inv, Quiver.Hom.unop_op, imageSubobject_arrow]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
· exact c'.prev_eq' (by simpa only [e.rel_iff] using hij')

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hjk : k = j
hk : c.Rel j k
⊢ c.Rel j j

Tactic:
simpa only [hjk] using hk

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

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extend e).homologyπ j' ≫ (K.extendHomologyIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ K.homologyπ j

Tactic:
by
  dsimp [extendHomologyIso, homologyπ]
  rw [ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc,
    ← cancel_mono (K.sc j).homologyData.left.homologyIso.hom,
    assoc, assoc, assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom]
  dsimp [extendCyclesIso]
  simp only [assoc, Iso.inv_hom_id_assoc]

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

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'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (truncLE'Map φ e).f i = (K.truncLE'XIsoCycles e h hi).hom ≫ cyclesMap φ i' ≫ (L.truncLE'XIsoCycles e h hi).inv

Tactic:
apply Quiver.Hom.op_inj
  dsimp [truncLE'Map, truncLE'XIsoCycles]
  rw [assoc, assoc, truncGE'Map_f_eq_opcyclesMap _ e.op (by simpa) h,
    opcyclesOpIso_inv_naturality_assoc, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: case pos
n₁ i : ℤ
k : ℕ
h : i + ↑k + 1 = n₁
hi : i ≤ i + ↑k
⊢ (∃ i₁, (embeddingUpIntLE (i + ↑k)).f i₁ = i) ∨ ∃ i₂, (embeddingUpIntGE n₁).f i₂ = i

Tactic:
exact Or.inl ⟨k, by dsimp; lia⟩

Goal state after: