mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (Hom.mk (z₁.comp₀ z₂ z₁₂)).comp (Hom.mk z₃) = (Hom.mk z₁).comp (Hom.mk (z₂.comp₀ z₃ z₂₃))

Tactic:
comp₀,

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ (Hom.mk { Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }).comp (Hom.mk z₃) =
    (Hom.mk z₁).comp (Hom.mk (z₂.comp₀ z₃ z₂₃))
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
⊢ (Hom.mk { Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }).comp (Hom.mk z₃) =
    (Hom.mk z₁).comp (Hom.mk (z₂.comp₀ z₃ z₂₃))

Tactic:
comp₀,

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ (Hom.mk { Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }).comp (Hom.mk z₃) =
    (Hom.mk z₁).comp (Hom.mk { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ })
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 Q R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X Y C : C✝
f : Y ⟶ X
g : X ⟶ C
h : C ⟶ (shiftFunctor C✝ 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
A B : C✝
f' : A ⟶ Y
g' : Y ⟶ B
h' : B ⟶ (shiftFunctor C✝ 1).obj A
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hP : P A
hQ : Q B
hR : R C
⊢ P.extensionProduct (Q.extensionProduct R) X

Tactic:
obtain ⟨Y, g'', h'', hT''⟩ := distinguished_cocone_triangle (f' ≫ f)

Goal state after:
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 Q R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X Y✝ C : C✝
f : Y✝ ⟶ X
g : X ⟶ C
h : C ⟶ (shiftFunctor C✝ 1).obj Y✝
hT : Triangle.mk f g h ∈ distinguishedTriangles
A B : C✝
f' : A ⟶ Y✝
g' : Y✝ ⟶ B
h' : B ⟶ (shiftFunctor C✝ 1).obj A
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hP : P A
hQ : Q B
hR : R C
Y : C✝
g'' : X ⟶ Y
h'' : Y ⟶ (shiftFunctor C✝ 1).obj A
hT'' : Triangle.mk (f' ≫ f) g'' h'' ∈ distinguishedTriangles
⊢ P.extensionProduct (Q.extensionProduct R) X
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
f g : Arrow (HomotopyCategory C c)
e : f ≅ g
hf : quasiIso C c f.hom
i : ι
⊢ IsIso ((homologyFunctor C c i).map g.hom)

Tactic:
exact ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    ((homologyFunctor C c i).mapArrow.mapIso e)).1 (hf i)

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
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : HasShift E ℤ
P : ObjectProperty C
X' X Y : C
e : X' ⟶ X
he : IsIso e
⊢ ∀ (f : X ⟶ Y), P.trW f → P.trW (e ≫ f)

Tactic:
by
    rintro f ⟨Z, g, h, mem, mem'⟩
    refine ⟨Z, g, h ≫ inv e⟦(1 : ℤ)⟧', isomorphic_distinguished _ mem _ ?_, mem'⟩
    refine Triangle.isoMk _ _ (asIso e) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_
    dsimp
    simp only [Functor.map_inv, assoc, IsIso.inv_hom_id, comp_id, id_comp]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ i
i : ℤ
⊢ QuasiIsoAt φ (n + i)

Tactic:
exact h (n + i)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₃ _ hT n₀ n₁ h)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      X₂ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      f := (DerivedCategory.homologyFunctor C n₀).map (DerivedCategory.Q.mapTriangle.obj T).mor₂,
      g := DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h, zero := ⋯ } ≅
    { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i : Option ι
⊢ d K i none = 0

Tactic:
cases i <;> rfl

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

Goal state before:
pp: case pos
ι : 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 j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ (if hi : e.BoundaryGE i then
        (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ opcyclesMap φ (e.f i) ≫ (L.truncGE'XIsoOpcycles e ⋯ hi).inv
      else (K.truncGE'XIso e ⋯ hi).hom ≫ φ.f (e.f i) ≫ (L.truncGE'XIso e ⋯ hi).inv) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ (K.truncGE'XIso e ⋯ ⋯).hom ≫ φ.f (e.f j) ≫ (L.truncGE'XIso e ⋯ ⋯).inv

Tactic:
rw [dif_pos hi]
      simp [truncGE'_d_eq_fromOpcycles _ e hij rfl rfl hi,
        ← cancel_epi (K.pOpcycles (e.f i))]

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'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
⊢ IsIso (K.πTruncGE e)

Tactic:
suffices ∀ (i' : ι'), IsIso ((K.πTruncGE e).f i') by
    apply Hom.isIso_of_components
  intro i'
  by_cases! hn : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hn
    dsimp [πTruncGE]
    rw [e.isIso_liftExtend_f_iff _ _ hi]
    infer_instance
  · refine ⟨0, ?_, ?_⟩
    all_goals
      apply (isZero_X_of_isStrictlySupported _ e i' hn).eq_of_src

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
⊢ ⋯.δ i' j' hij' = 0

Tactic:
by_cases hj : ∃ j, e.f j = j'
  · obtain ⟨j, rfl⟩ := hj
    rw [← cancel_mono (homologyMap (K.ιTruncLE e) (e.f j)), zero_comp]
    exact (K.shortComplexTruncLE_shortExact e).δ_comp i' _ hij'
  · apply ((K.truncLE e).exactAt_of_isSupported e j'
      (by simpa using hj)).isZero_homology.eq_of_tgt

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)) → K.IsStrictlyGE n

Tactic:
intro h
    refine IsStrictlySupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntGE_iff] at hi
    exact h i hi

Goal state after:
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
f : X ⟶ Y
⊢ (homEquiv W L₁ L₂) (L₁.map f) = L₂.map f

Tactic:
simp [homEquiv_apply]

Goal state after:
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 : C
⊢ (homEquiv W L₁ L₂) (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X)

Tactic:
simp [homEquiv_apply]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')

Tactic:
exact small_congr (Iso.homCongr (Iso.refl _) (Localization.isoOfHom W.Q W f hf))

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
L : C ⥤ D
inst✝² : L.IsLocalization W
inst✝¹ : L.CommShift M
X Y : C
inst✝ : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ (L.map f ≫ L.map ((shiftFunctorZero' C 0 ⋯).inv.app Y)) ≫ (Functor.commShiftIso L 0).hom.app Y =
    ShiftedHom.mk₀ 0 ⋯ (L.map f)

Tactic:
dsimp [equiv, mk₀, ShiftedHom.mk₀, shiftFunctorZero']

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
L : C ⥤ D
inst✝² : L.IsLocalization W
inst✝¹ : L.CommShift M
X Y : C
inst✝ : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ (L.map f ≫ L.map ((shiftFunctorZero C M).inv.app Y ≫ 𝟙 ((shiftFunctor C 0).obj Y))) ≫
      (Functor.commShiftIso L 0).hom.app Y =
    L.map f ≫ (shiftFunctorZero D M).inv.app (L.obj Y) ≫ 𝟙 ((shiftFunctor D 0).obj (L.obj Y))
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
inst✝ : HasDerivedCategory C
f : X ⟶ Y
⊢ (mk₀ f).hom = ShiftedHom.mk₀ (↑0) mk₀._proof_1 ((singleFunctor C 0).map f)

Tactic:
by
  apply SmallShiftedHom.equiv_mk₀

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    (((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
          inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁

Tactic:
← Iso.app_hom,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      ((Functor.commShiftIso Q 1).app S₂.X₁).hom =
    (((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
          inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      ((Functor.commShiftIso Q 1).app S₂.X₁).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃

Tactic:
· dsimp
    simp only [← Q.map_comp, CochainComplex.mappingCone.inr_descShortComplex, id_comp]

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
X : C
⊢ (iso adj a).hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))) ≫
        F.map ((shiftFunctor C a).map ((Functor.commShiftIso G b).hom.app ((shiftFunctor D a).obj (F.obj X)))) ≫
          F.map ((shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : G.CommShift A
X : C
h : a + -a = 0
⊢ (iso adj a).hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) h).inv.app (F.obj X)))) ≫
        F.map ((shiftFunctor C a).map ((Functor.commShiftIso G (-a)).hom.app ((shiftFunctor D a).obj (F.obj X)))) ≫
          F.map ((shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            adj.counit.app ((shiftFunctor D a).obj (F.obj X))
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
Y : C
⊢ (iso adj a).inv.app Y =
    (shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y)) ≫
      (shiftFunctor D a).map (F.map ((shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj Y)))) ≫
        (shiftFunctor D a).map (F.map ((Functor.commShiftIso G b).inv.app (F.obj ((shiftFunctor C a).obj Y)))) ≫
          (shiftFunctor D a).map (adj.counit.app ((shiftFunctor D b).obj (F.obj ((shiftFunctor C a).obj Y)))) ≫
            (shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))

Tactic:
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : G.CommShift A
Y : C
h : a + -a = 0
⊢ (iso adj a).inv.app Y =
    (shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a (-a) h).inv.app Y)) ≫
      (shiftFunctor D a).map (F.map ((shiftFunctor C (-a)).map (adj.unit.app ((shiftFunctor C a).obj Y)))) ≫
        (shiftFunctor D a).map (F.map ((Functor.commShiftIso G (-a)).inv.app (F.obj ((shiftFunctor C a).obj Y)))) ≫
          (shiftFunctor D a).map (adj.counit.app ((shiftFunctor D (-a)).obj (F.obj ((shiftFunctor C a).obj Y)))) ≫
            (shiftFunctorCompIsoId D (-a) a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))
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
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := T.coyoneda_exact₂ hT x₂ hx₂

Goal state after:
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
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
x₁ : unop A ⟶ T.obj₁
hx₁ : x₂ = x₁ ≫ T.mor₁
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
h : ↑(AddCommGrpCat.of (Ext N M n))
this : r • 𝟙 N = 0
⊢ r • h = (mk₀ (r • 𝟙 N)).comp h ⋯

Tactic:
simp [Ext.mk₀_smul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
i : ℕ
x✝¹ x✝ : Ext N M i
⊢ (ConcreteCategory.hom (AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯))) x✝ = r • x✝

Tactic:
simp [Ext.mk₀_smul]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ∀ (i_1 : ℤ), (ComplexShape.up ℤ).Rel i_1 i → L.d i_1 i ≫ Injective.factorThru (𝟙 I) α = 0

Tactic:
rintro j rfl
      apply (L.isZero_of_isStrictlyGE (j + 1) j (by simp)).eq_of_src

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
this : π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)
⊢ (Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) (relations.relation r) = 0

Tactic:
rw [← this]

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
this : π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)
⊢ π (relations.relation r) = 0
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ solution.π.ker
⊢ relations.toQuotient x ∈ ⊥

Tactic:
rw [h, ← range_map] at hx

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ relations.map.range
⊢ relations.toQuotient x ∈ ⊥
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Mᵀ.SeparatingRight ↔ M.SeparatingLeft

Tactic:
have := Fintype.ofFinite m
  have := Fintype.ofFinite n
  simp_rw [separatingRight_def, separatingLeft_def, dotProduct_transpose_mulVec]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
⊢ Subsingleton ↥(rootsOfUnity 1 M)

Tactic:
by simp [subsingleton_iff]

Goal state after: