mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ homMk z₁ ≫ homMk z₂ = homMk (z₁.comp₀ z₂ z₃)

Tactic:
by
  change Hom.comp _ _ = _
  rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]

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
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) ≫ e.hom.app Y =
    (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯

Tactic:
← cancel_mono (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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ ((Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) ≫ e.hom.app Y) ≫ L₂.map φ.s =
    ((Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯) ≫ L₂.map φ.s
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
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.compUniqFunctor L₂ L₁ W).hom.app X ≫ φ₁.map L₁ ⋯ ≫ (Localization.compUniqFunctor L₂ L₁ W).inv.app Y =
    (Localization.compUniqFunctor L₂ L₁ W).hom.app X ≫ φ₂.map L₁ ⋯ ≫ (Localization.compUniqFunctor L₂ L₁ W).inv.app Y

Tactic:
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
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.compUniqFunctor L₂ L₁ W).hom.app X ≫ φ₂.map L₁ ⋯ ≫ (Localization.compUniqFunctor L₂ L₁ W).inv.app Y =
    (Localization.compUniqFunctor L₂ L₁ W).hom.app X ≫ φ₂.map L₁ ⋯ ≫ (Localization.compUniqFunctor L₂ L₁ W).inv.app Y
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝ : F.ShiftSequence ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ n₀ + 1 = n₁

Tactic:
h

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝ : F.ShiftSequence ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ n₁ = n₁
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₂ + a₁ = a

Tactic:
h

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a = a
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
⊢ a✝ ≤ b✝ → a✝.retracts ≤ b✝.retracts

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
⊢ a✝.retracts ≤ b✝.retracts
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P Y
Z' : C
hQ : Q Z'
i : Z ≅ Z'
⊢ Triangle.mk f (g ≫ i.hom) (i.inv ≫ h) ∈ distinguishedTriangles

Tactic:
exact isomorphic_distinguished _ hT _ <| Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) i.symm

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
P Q : ObjectProperty C
inst✝ : Q.ContainsZero
X : C
hX : P X
⊢ P.extensionProduct Q X

Tactic:
rw [← extensionProduct_isoClosure_right]

Goal state after:
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 : ObjectProperty C
inst✝ : Q.ContainsZero
X : C
hX : P X
⊢ P.extensionProduct Q.isoClosure X
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 : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i ↔ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
by
  constructor
  · intro h
    exact h.quasiIso
  · intro h
    exact ⟨h⟩

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

Goal state before:
pp: case a
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 : ObjectProperty C
⊢ P.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure

Tactic:
monotone_extensionProduct_right _ (le_retractClosure Q),

Goal state after:
case a
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 : ObjectProperty C
⊢ P.extensionProduct Q.retractClosure ≤ P.retractClosure.extensionProduct Q.retractClosure
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
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hf : QuasiIsoAt f i
⊢ IsIso (homologyMap f i)

Tactic:
simpa only [quasiIsoAt_iff, ShortComplex.quasiIso_iff] using! hf

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 L : CochainComplex C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]
  exact (NatIso.isIso_map_iff
    ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i j h) φ)

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

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : i = a
⊢ ((single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj X).X i =
    ((single C (ComplexShape.up ℤ) a).obj X).X i

Tactic:
subst h
          simp only [Functor.comp_obj, shiftFunctor_obj_X', single_obj_X_self]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n : ℤ
⊢ ((singleFunctors C).functor n).Additive

Tactic:
dsimp only [singleFunctors]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n : ℤ
⊢ (single C (ComplexShape.up ℤ) n).Additive
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✝ : P.IsTriangulated
T₁ T₂ : Triangle P.FullSubcategory
hT₁ : T₁ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
hT₂ : T₂ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ (P.ι.mapTriangle.obj T₁).mor₁ ≫ P.ι.map b = P.ι.map a ≫ (P.ι.mapTriangle.obj T₂).mor₁

Tactic:
by simpa using P.ι.congr_map comm

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 (DerivedCategory C)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ n₀ + 1 = n₁

Tactic:
h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ n₁ = n₁
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ (embeddingUp'Add a b).IsRelIff

Tactic:
by dsimp [embeddingUp'Add]; infer_instance

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 := homologyδOfTriangle T n₀ n₁ h,
      g := homologyMap T.mor₁ n₁, zero := ⋯ }.Exact

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

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

Goal state before:
pp: case inr.inr
ι : 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'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
obtain hk' | ⟨k, hk⟩ := (e.r k').eq_none_or_eq_some
        · rw [extend.d_none_eq_zero' K _ _ hk', comp_zero]
        · rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]

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.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

Tactic:
obtain ⟨k', hk'⟩ := e.mem_next hj

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
k' : ι
hk' : e.f k' = c'.next (e.f j)
⊢ c'.next (e.f j) = e.f k
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
⊢ extendMap 0 e = 0

Tactic:
ext i'
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]
  · apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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

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✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
⊢ extendMap (φ + φ') e = extendMap φ e + extendMap φ' e

Tactic:
ext i'
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]
  · apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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

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✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = e.f i

Tactic:
h

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✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = i'
Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
h : (singleFunctor C n).map f₁ = (singleFunctor C n).map f₂
eq₁ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₁
eq₂ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₂
⊢ (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝

Tactic:
h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
h : (singleFunctor C n).map f₁ = (singleFunctor C n).map f₂
eq₁ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₁
eq₂ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₂
⊢ (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
let G' := Ψ.localizedFunctor L₂ L₃

Goal state after:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L')
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) ((homEquiv W L W.Q) f))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
Equiv.symm_apply_apply,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L') ((homEquiv W L W.Q) f) = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
inst✝² : Injective (K.X n₀)
inst✝¹ : Injective (K.X n₁)
inst✝ : K.IsStrictlyGE n₀
hK : ExactAt K n₀
h : n₀ + 1 = n₁
S : ShortComplex C :=
  { X₁ := K.X n₀, X₂ := K.X n₁, X₃ := opcycles K n₁, f := K.d n₀ n₁, g := pOpcycles K n₁, zero := ⋯ }
this : Mono S.f
⊢ (up ℤ).prev n₁ = n₀

Tactic:
by simp [← h]

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 Y X
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f)
⊢ (equiv W L) (mk₀Inv m₀ hm₀ f hf) = ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv

Tactic:
refine (SmallHom.equiv_mkInv L _ hf' =≫ _).trans ?_

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 Y X
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f)
⊢ (isoOfHom L W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) hf').inv ≫ ((Functor.commShiftIso L m₀).app X).hom =
    ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv
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
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₂ + a₁ = a

Tactic:
h

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
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a = a
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:
mem_distinguishedTriangles_iff

Goal state after:
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ᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))