mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ P X

Tactic:
obtain ⟨Z, hZ, hZ₂⟩ := P.exists_prop_of_containsZero

Goal state after:
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
⊢ P X
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.ColimitOfShape (Discrete PEmpty.{1}) X
⊢ P X

Tactic:
obtain ⟨Z, hZ, hZ₂⟩ := P.exists_prop_of_containsZero

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ P X
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
⊢ { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }.f ≫
      { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ }.s =
    z₁.s ≫ { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ }.f

Tactic:
by dsimp; rw [assoc, ← reassoc_of% fac₁₂, fac]

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 Y : C
s : X ⟶ Y
hs : W s
⊢ Qinv s hs ≫ (Q W).map s = 𝟙 ((Q W).obj Y)

Tactic:
dsimp only [Qinv, Q_map]
    rw [homMk_comp_homMk (ofInv s hs) (ofHom W s) (ofHom W (𝟙 Y)) (by simp)]
    apply homMk_eq_of_leftFractionRel
    exact ⟨_, 𝟙 Y, 𝟙 Y, by simp, by simp, by simpa using W.id_mem Y⟩

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ → ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

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:
· intro h
    rw [← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
      ← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
      RightFraction.map_eq_iff] at h
    obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
    dsimp at t₁ t₂ hst hft ht
    grind

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
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₂
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
f : K ⟶ L
inst✝² : IsIso f
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff]

Goal state after:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
f : K ⟶ L
inst✝² : IsIso f
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.sc' i j k).HasHomology
inst✝ : (L.sc' i j k).HasHomology
⊢ QuasiIsoAt f j ↔ ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)

Tactic:
rw [quasiIsoAt_iff]

Goal state after:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.sc' i j k).HasHomology
inst✝ : (L.sc' i j k).HasHomology
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map f) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
⊢ subcategoryAcyclic C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
rw [mem_subcategoryAcyclic_iff]
  refine forall_congr' (fun n => ?_)
  simp only [HomologicalComplex.exactAt_iff_isZero_homology]
  exact ((homologyFunctorFactors C (ComplexShape.up ℤ) n).app K).isZero_iff

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ

Tactic:
by
  rw [quasiIso_eq_trW_subcategoryAcyclic]
  infer_instance

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

Goal state before:
pp: case refine_5
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
      (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
        (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂)) ∈
    distinguishedTriangles

Tactic:
refine isomorphic_distinguished _ (mappingConeCompTriangleh_distinguished u₁₂ u₂₃) _ ?_

Goal state after:
case refine_5
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
      (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
        (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂)) ≅
    mappingConeCompTriangleh u₁₂ u₂₃
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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 M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ K.X (e.f i) = K.X i'

Tactic:
subst hi'; rfl

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

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 M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ K.opcycles (e.f i) = K.opcycles i'

Tactic:
subst hi'; rfl

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

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
⊢ (K.truncGE' e).d i j = (K.truncGE'XIsoOpcycles e hi' hi).hom ≫ K.fromOpcycles i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv

Tactic:
by
  dsimp [truncGE', truncGE'.d]
  rw [dif_pos hij, dif_pos hi]
  subst hi' hj'
  simp [truncGE'XIso, truncGE'XIsoOpcycles]

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

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
⊢ QuasiIsoAt (K.restrictionToTruncGE' e) j

Tactic:
rw [quasiIsoAt_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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ QuasiIsoAt (K.πTruncGE e) j'

Tactic:
rw [quasiIsoAt_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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom ≫ K.homologyι j' =
    (K.restriction e).homologyι j ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom

Tactic:
rw [← cancel_epi (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv,
    Iso.inv_hom_id_assoc, restrictionHomologyIso_inv_homologyι_assoc,
      Iso.inv_hom_id, comp_id]

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

Goal state before:
pp: case inl
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₁ : ι₁
⊢ φ.f (e₁.f i₁) = HomologicalComplex.Hom.f 0 (e₁.f i₁)

pp: case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₂ : ι₂
⊢ φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (e₂.f i₂)

Tactic:
· apply (hL.isZero i₁).eq_of_tgt

Goal state after:
case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₂ : ι₂
⊢ φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (e₂.f i₂)
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
G : D₁ ⥤ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₁ L₂) f = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
    Iso.symm_hom, Iso.symm_inv]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ ∃ Y', ∃ (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b), ∃ g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
refine ⟨Y'.truncLE b, inferInstance, inferInstance,
    inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b,
    inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z T : C
inst✝⁵ : HasSmallLocalizedHom W X Y
inst✝⁴ : HasSmallLocalizedHom W X Z
inst✝³ : HasSmallLocalizedHom W X T
inst✝² : HasSmallLocalizedHom W Y Z
inst✝¹ : HasSmallLocalizedHom W Y T
inst✝ : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ (α.comp β).comp γ = α.comp (β.comp γ)

Tactic:
apply (equiv W W.Q).injective
  simp only [equiv_comp, assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ comp 0 β h = 0

Tactic:
let := HasDerivedCategory.standard C; ext; simp [this, zero_hom']

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
⊢ α.comp 0 h = 0

Tactic:
let := HasDerivedCategory.standard C; ext; simp [this, zero_hom']

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
          𝟙
            ((shiftFunctor (DerivedCategory C) 1).obj
              (Q.obj ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)))

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
⊢ (NatIso.op (commShiftIso F 0)).symm = CommShift.isoZero (OppositeShift.functor A F) A

Tactic:
rw [commShiftIso_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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
⊢ (NatIso.op (CommShift.isoZero F A)).symm = CommShift.isoZero (OppositeShift.functor A F) A
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
⊢ NatIso.removeOp (commShiftIso (OppositeShift.functor A F) 0).symm = CommShift.isoZero F A

Tactic:
rw [commShiftIso_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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
⊢ NatIso.removeOp (CommShift.isoZero (OppositeShift.functor A F) A).symm = CommShift.isoZero F A
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).Exact

Tactic:
rw [ShortComplex.ab_exact_iff]
    intro (x₂ : T.obj₂.unop ⟶ B) (hx₂ : T.mor₂.unop ≫ x₂ = 0)
    obtain ⟨x₃, hx₃⟩ := Triangle.yoneda_exact₂ _ (unop_distinguished T hT) x₂ hx₂
    exact ⟨x₃, hx₃.symm⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ (↑z • e.hom) ≫ (↑z⁻¹ • e.inv) = 𝟙 X

Tactic:
rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.hom ≫ (↑z * ↑z⁻¹).app Y ≫ e.inv = 𝟙 X
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ (↑z⁻¹ • e.inv) ≫ (↑z • e.hom) = 𝟙 Y

Tactic:
rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.inv ≫ (↑z⁻¹ * ↑z).app X ≫ e.hom = 𝟙 Y
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
⊢ inv (Q.map π) ≫ Q.map g = 0

Tactic:
have hπ : IsSplitEpi π := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
⊢ inv (Q.map π) ≫ Q.map g = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
⊢ inv (Q.map π) = Q.map (section_ π)

Tactic:
← cancel_mono (Q.map π),

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
⊢ inv (Q.map π) ≫ Q.map π = Q.map (section_ π) ≫ Q.map π