mathlib-initiative/mathlib-tactics huggingface dataset:
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),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
intro T₁

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₁ : Triangle C
⊢ ∀ (T₂' : Triangle C),
    T₁ ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
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.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ (∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s) → L.map f₁ = L.map f₂

Tactic:
rintro ⟨Z, s, hs, fac⟩
    simp only [← cancel_mono (Localization.isoOfHom L W s hs).hom,
      Localization.isoOfHom_hom, ← L.map_comp, 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
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
h : W.HasRightCalculusOfFractions
X Y : Cᵒᵖ
φ : W.op.RightFraction X Y
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f

Tactic:
by
    obtain ⟨ψ, eq⟩ := h.exists_rightFraction φ.unop
    exact ⟨ψ.op, Quiver.Hom.unop_inj eq⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone retracts

Tactic:
intro _ _ h _ _ _ ⟨_, _, _, hg, hg'⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝² w✝¹ : C
w✝ : w✝² ⟶ w✝¹
hg : RetractArrow f✝ w✝
hg' : a✝ w✝
⊢ b✝.retracts f✝
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case base
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.ContainsZero
n m : ℕ
⊢ P.extensionProductIter n ≤ P.extensionProductIter n

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
inst✝ : P.ContainsZero
n m n✝ : ℕ
hmn✝ : n ≤ n✝
a✝ : P.extensionProductIter n ≤ P.extensionProductIter n✝
⊢ P.extensionProductIter n ≤ P.extensionProductIter (n✝ + 1)

Tactic:
case base => rfl

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
inst✝ : P.ContainsZero
n m n✝ : ℕ
hmn✝ : n ≤ n✝
a✝ : P.extensionProductIter n ≤ P.extensionProductIter n✝
⊢ P.extensionProductIter n ≤ P.extensionProductIter (n✝ + 1)
Module: Mathlib.CategoryTheory.Localization.Composition

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ L₂.IsLocalization W₂

Tactic:
have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
      comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _
        (by simpa only [hW₂₃] using W₃.map_mem_map _ _ hf)) hW₁₃
        (by rw [hW₂₃])

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
this : (L₁ ⋙ W₂.Q).IsLocalization W₃
⊢ L₂.IsLocalization W₂
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ quasiIso C c e.hom

Tactic:
simp only [HomologicalComplex.mem_quasiIso_iff]

Goal state after:
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ QuasiIso e.hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (subcategoryAcyclic C).IsTriangulated

Tactic:
dsimp [subcategoryAcyclic]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (subcategoryAcyclic C).IsClosedUnderIsomorphisms

Tactic:
dsimp [subcategoryAcyclic]
  infer_instance

Goal state after:
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
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
⊢ ∀ (x y : HomologicalComplex C c) (f₁ f₂ : x ⟶ y), homotopic C c f₁ f₂ → Q.map f₁ = Q.map f₂

Tactic:
by
    intro K L f g ⟨h⟩
    exact Q_map_eq_of_homotopy h

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
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk φ.s f g ∈ distinguishedTriangles
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ (shiftFunctor C 1).obj X'
mem' : Triangle.mk f' (φ.f ≫ f) h' ∈ distinguishedTriangles
a : (Triangle.mk f' (φ.f ≫ f) h').obj₁ ⟶ (Triangle.mk φ.s f g).obj₁
ha₁ : (Triangle.mk f' (φ.f ≫ f) h').mor₁ ≫ φ.f = a ≫ (Triangle.mk φ.s f g).mor₁
right✝ : (Triangle.mk f' (φ.f ≫ f) h').mor₃ ≫ (shiftFunctor C 1).map a = 𝟙 Z ≫ (Triangle.mk φ.s f g).mor₃
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
exact ⟨MorphismProperty.RightFraction.mk f' ⟨_, _, _, mem', mem⟩ a, ha₁⟩

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 ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h =
    (DerivedCategory.homologyFunctor C 0).shiftMap
        (DerivedCategory.Q.map T.mor₃ ≫ (Functor.commShiftIso DerivedCategory.Q 1).hom.app T.obj₁) n₀ n₁ ⋯ ≫
      (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁

Tactic:
rw [dsimp% [ShiftedHom.map]
      DerivedCategory.shiftMap_homologyFunctor_map_Q T.mor₃ n₀ n₁ (by lia)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h =
    ((DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫
        (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫
          (DerivedCategory.homologyFunctorFactors C n₁).inv.app T.obj₁) ≫
      (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
rw [extend.d_none_eq_zero K _ _ hi', zero_comp]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : (e.extendFunctor C).obj K ⟶ (e.extendFunctor C).obj L
i : ι
⊢ ((e.extendFunctor C).map { f := fun i ↦ (K.extendXIso e ⋯).inv ≫ φ.f (e.f i) ≫ (L.extendXIso e ⋯).hom, comm' := ⋯ }).f
      (e.f i) =
    φ.f (e.f i)

Tactic:
simp [HomologicalComplex.extendMap_f _ _ rfl]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
⊢ { f := fun i ↦ (K.extendXIso e ⋯).inv ≫ ((e.extendFunctor C).map f).f (e.f i) ≫ (L.extendXIso e ⋯).hom, comm' := ⋯ }.f
      i =
    f.f i

Tactic:
simp [HomologicalComplex.extendMap_f _ _ rfl]

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'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
⊢ IsIso ((K.restrictionToTruncGE' e).f (c.next j))

Tactic:
exact K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)

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

Goal state before:
pp: case left.inr.inl
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Sum.inr i₂ = Sum.inl j₁

Tactic:
exact (ac.disjoint _ _ h.symm).elim

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

Goal state before:
pp: case neg
ι : 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 : ι
hi : ¬∃ j', c'.Rel (e.f i) j'
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance
      rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]

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

Goal state before:
pp: case neg
ι : 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 : ι
hi : ¬∃ j', c'.Rel (e.f i) j'
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
· have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance
      rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n ↔ ∀ i < n, ExactAt K i

Tactic:
constructor
  · intro _ i hi
    exact K.exactAt_of_isGE n i hi
  · intro h
    refine IsSupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntGE_iff] at hi
    exact h i hi

Goal state after:
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).pOpcycles j ≫ (singleObjOpcyclesSelfIso c j A).inv = (singleObjXSelf c j A).hom

Tactic:
have := ((single C c j).obj A).isIso_iCycles j _ rfl (by simp)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
this : IsIso (((single C c j).obj A).iCycles j)
⊢ ((single C c j).obj A).pOpcycles j ≫ (singleObjOpcyclesSelfIso c j A).inv = (singleObjXSelf c j A).hom
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 : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ ((α₁ + α₂).comp β h).hom = (α₁.comp β h + α₂.comp β h).hom

Tactic:
simp [this, add_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 Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ (α.comp (β₁ + β₂) h).hom = (α.comp β₁ h + α.comp β₂ h).hom

Tactic:
simp [this, add_hom']

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) =
    ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op ≫ (shiftFunctorZero (OppositeShift C A) A).inv.app X

Tactic:
oppositeShiftFunctorZero_inv_app,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) =
    ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op ≫ ((shiftFunctorZero C A).hom.app (Opposite.unop X)).op
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
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝))).op ≫
      ((shiftFunctorZero D A).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorZero (OppositeShift C A) A).hom.app x✝) ≫
      (shiftFunctorZero (OppositeShift D A) A).inv.app ((OppositeShift.functor A F).obj x✝)

Tactic:
oppositeShiftFunctorZero_inv_app,

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
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝))).op ≫
      ((shiftFunctorZero D A).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorZero (OppositeShift C A) A).hom.app x✝) ≫
      ((shiftFunctorZero D A).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) a₁).obj X) ≫
      (shiftFunctor C (φ a₂)).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
          (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Tactic:
erw [Functor.map_id, id_comp, id_comp, shiftFunctorAdd'_eq_shiftFunctorAdd,
    shiftFunctorAdd'_eq_shiftFunctorAdd]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd (PullbackShift C φ) a₁ a₂).inv.app X =
    (shiftFunctorAdd C (φ a₁) (φ a₂)).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
by
  rw [mem_distinguishedTriangles_iff]
  constructor
  · intro hT
    exact ⟨_, hT, ⟨(triangleOpEquivalence C).counitIso.symm.app T⟩⟩
  · rintro ⟨T', hT', ⟨e⟩⟩
    refine isomorphic_distinguished _ hT' _ ?_
    exact Iso.unop ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫
      (triangleOpEquivalence C).inverse.mapIso e.symm)

Goal state after:
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✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x✝ : Cᵒᵖ
x : ↑((shiftFunctor Cᵒᵖ (m + n) ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x✝)
⊢ (AddCommGrpCat.Hom.hom
        ((NatIso.ofComponents
                (fun A ↦
                  (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm;
                    { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                ⋯).hom.app
          x✝))
      x =
    (AddCommGrpCat.Hom.hom
        ((Functor.isoWhiskerRight (shiftFunctorAdd Cᵒᵖ m n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                (shiftFunctor Cᵒᵖ m).associator (shiftFunctor Cᵒᵖ n)
                    (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                  (shiftFunctor Cᵒᵖ m).isoWhiskerLeft
                      (NatIso.ofComponents
                        (fun A ↦
                          (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' ha').symm;
                            { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                        ⋯) ≪≫
                    NatIso.ofComponents
                      (fun A ↦
                        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' m a' a'' ha'').symm;
                          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                      ⋯).hom.app
          x✝))
      x

Tactic:
exact ShiftedHom.opEquiv'_add_symm n m a a' a'' ha' ha'' x.op

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
⊢ Functor.Linear R F ↔ Functor.Linear R G

Tactic:
by
  constructor
  · intro
    have : (L ⋙ G).Linear R := Functor.linear_of_iso _ (Lifting.iso L W F G).symm
    have := Localization.essSurj L W
    rw [Functor.linear_iff]
    intro X r
    have e := L.objObjPreimageIso X
    have : r • 𝟙 X = e.inv ≫ (r • 𝟙 _) ≫ e.hom := by simp
    rw [this, G.map_comp, G.map_comp, ← L.map_id, ← L.map_smul, ← Functor.comp_map,
      (L ⋙ G).map_smul, Functor.map_id, Linear.smul_comp, Linear.comp_smul]
    dsimp
    rw [Category.id_comp, ← G.map_comp, e.inv_hom_id, G.map_id]
  · intro
    exact Functor.linear_of_iso _ (Lifting.iso L W F G)

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
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
⊢ Function.Bijective ⇑(solution.postcomp ↑e).fromQuotient

Tactic:
have : (solution.postcomp e.toLinearMap).fromQuotient =
      e.toLinearMap.comp (solution.fromQuotient) := by aesop
    rw [this, LinearMap.coe_comp, LinearEquiv.coe_coe]
    exact Function.Bijective.comp e.bijective h.bijective

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
this✝ : Function.Injective ⇑(toLin' M)
this : M * toMatrix' ↑(LinearEquiv.ofInjectiveEndo (toLin' M) this✝).symm = 1
⊢ M.det ≠ 0

Tactic:
exact Matrix.det_ne_zero_of_right_inverse this

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
A : GL n R
⊢ ↑((scalar n) u * A) = ↑(A * (scalar n) u)

Tactic:
rw [Units.val_mul, Units.val_mul, coe_scalar, Matrix.scalar_comm _ (Commute.all _)]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ ∀ (j : n), 0 < ∑ i, A j i

Tactic:
exact h2

Goal state after: