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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
h₁₂ : LeftFractionRel z₁ z₂
h₂₃ : LeftFractionRel z₂ z₃
⊢ LeftFractionRel z₁ z₃

Tactic:
obtain ⟨Z₄, t₁, t₂, hst, hft, ht⟩ := h₁₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
h₂₃ : LeftFractionRel z₂ z₃
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁ z₃
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f₁ f₂ : X' ⟶ Y'
g : Y' ⟶ Z'
⊢ add W eX eY f₁ f₂ ≫ g = add W eX eZ (f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨g, rfl⟩ := (homEquiv eY eZ).symm.surjective g
  simp [add]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
E : Type u_3
inst✝² : Category.{v_2, u_3} E
inst✝¹ : HasShift E A
a : A
inst✝ : P.IsStableUnderShiftBy a
⊢ P.isoClosure ≤ P.isoClosure.shift a

Tactic:
rintro X ⟨Y, hY, ⟨e⟩⟩
    exact ⟨Y⟦a⟧, P.le_shift a _ hY, ⟨(shiftFunctor C a).mapIso e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasTerminal C
P Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderBinaryProducts
inst✝ : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryProductsClosure ≤ Q ↔ P ≤ Q

Tactic:
refine ⟨fun h ↦ (P.le_limitsClosure _).trans h, fun h ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasTerminal C
P Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderBinaryProducts
inst✝ : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
h : P ≤ Q
⊢ P.binaryProductsClosure ≤ Q
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderLimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, 0} J))

Tactic:
exact H _

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderColimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete (Shrink.{w, 0} J))

Tactic:
exact H _

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

Goal state before:
pp: case refine_2
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 ℤ
H :
  ∀ (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
T₁ T₂ : Triangle D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle C
e₁ : T₁ ≅ L.mapTriangle.obj T₁'
hT₁' : T₁' ∈ distinguishedTriangles
T₂' : Triangle C
e₂ : T₂ ≅ L.mapTriangle.obj T₂'
hT₂' : T₂' ∈ distinguishedTriangles
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ (commShiftIso L 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  L.map T₁'.mor₃ ≫ (commShiftIso L 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map φ.hom₁ =
    φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁
⊢ T₁.mor₃ ≫ (shiftFunctor D 1).map a = (e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃) ≫ T₂.mor₃

Tactic:
rw [assoc, assoc, ← cancel_epi e₁.inv.hom₃, ← reassoc_of% comm₃,
      Iso.inv_hom_id_triangle_hom₃_assoc, ← cancel_mono (e₂.hom.hom₁⟦(1 : ℤ)⟧'),
      assoc, assoc, assoc, assoc, assoc, ← Functor.map_comp, ← Functor.map_comp, ← hφ₁,
      h₃, comm₃', Iso.inv_hom_id_triangle_hom₃_assoc]

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.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → LeftFractionRel φ ψ

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
φ ψ : W.LeftFraction X Y
⊢ LeftFractionRel φ ψ → φ.map L ⋯ = ψ.map L ⋯

Tactic:
· intro h
    rw [← MorphismProperty.LeftFraction.Localization.map_eq_iff]
    apply map_eq_of_map_eq _ _ _ _ h

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.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ LeftFractionRel φ ψ → φ.map L ⋯ = ψ.map L ⋯
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
⊢ F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
by
  obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
  apply (F.homologicalKernel.trW_iff_of_distinguished _ hT).trans
  have h₁ := fun n => (F.homologySequence_exact₃ _ hT n _ rfl).isZero_X₂_iff
  have h₂ := fun n => F.homologySequence_mono_shift_map_mor₁_iff _ hT n _ rfl
  have h₃ := fun n => F.homologySequence_epi_shift_map_mor₁_iff _ hT n
  dsimp at h₁ h₂ h₃ ⊢
  simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]
  constructor
  · intro h n
    obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩
    have := (h (m + 1)).1
    have := (h m).2
    apply isIso_of_mono_of_epi
  · intros
    constructor <;> infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderRetracts ↔ P.retracts ≤ P

Tactic:
rw [isStableUnderRetracts_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f) ↔ P.retracts ≤ P
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
functor : A → C ⥤ D
shiftIso : (n a a' : A) → n + a = a' → (functor a' ⋙ shiftFunctor D n ≅ functor a)
shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (shiftFunctorZero D A)
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + (n + a) = a''

Tactic:
ha',

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
functor : A → C ⥤ D
shiftIso : (n a a' : A) → n + a = a' → (functor a' ⋙ shiftFunctor D n ≅ functor a)
shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (shiftFunctorZero D A)
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + a' = a''
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + (n + a) = a''

Tactic:
ha',

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + a' = a''
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ Q.mapTriangle.obj (mappingCone.triangle φ) ∈ distinguishedTriangles

Tactic:
mem_distTriang_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ ∃ X Y f, Nonempty (Q.mapTriangle.obj (mappingCone.triangle φ) ≅ Q.mapTriangle.obj (mappingCone.triangle f))
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
T₁ T₃ : Triangle C
mem₁ : T₁ ∈ distinguishedTriangles
mem₃ : T₃ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₃.obj₁
b : T₁.obj₂ ⟶ T₃.obj₂
Z₅ : C
g₅ : T₃.obj₁ ⟶ Z₅
h₅ : Z₅ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₅ : Triangle.mk a g₅ h₅ ∈ distinguishedTriangles
mem₅' : P Z₅
Z₄ : C
g₄ : T₃.obj₂ ⟶ Z₄
h₄ : Z₄ ⟶ (shiftFunctor C 1).obj T₁.obj₂
mem₄ : Triangle.mk b g₄ h₄ ∈ distinguishedTriangles
mem₄' : P Z₄
comm : T₁.mor₁ ≫ b = a ≫ T₃.mor₁
Z₂ : C
g₂ : T₃.obj₂ ⟶ Z₂
h₂ : Z₂ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₂ : Triangle.mk (T₁.mor₁ ≫ b) g₂ h₂ ∈ distinguishedTriangles
H : Octahedron ⋯ mem₁ mem₄ mem₂
H' : Octahedron ⋯ mem₅ mem₃ mem₂
φ : T₁ ⟶ T₃ := H.triangleMorphism₁ ≫ H'.triangleMorphism₂
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map a = φ.hom₃ ≫ T₃.mor₃

Tactic:
simpa [φ] using φ.comm₃

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
i : ℤ
j : ℕ
h : (up ℤ).Rel i (embeddingDownNat.f j)
⊢ embeddingDownNat.f (j + 1) = i

Tactic:
dsimp at h ⊢

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
i : ℤ
j : ℕ
h : i + 1 = -↑j
⊢ -(↑j + 1) = i
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
j : ℕ
x✝ : ℤ
h : (up ℤ).Rel ((embeddingUpIntGE p).f j) x✝
⊢ (embeddingUpIntGE p).f (j + 1) = x✝

Tactic:
dsimp at h ⊢

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
j : ℕ
x✝ : ℤ
h : p + ↑j + 1 = x✝
⊢ p + (↑j + 1) = x✝
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p x✝ : ℤ
k : ℕ
h : (up ℤ).Rel x✝ ((embeddingUpIntLE p).f k)
⊢ (embeddingUpIntLE p).f (k + 1) = x✝

Tactic:
dsimp at h ⊢

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p x✝ : ℤ
k : ℕ
h : x✝ + 1 = p - ↑k
⊢ p - (↑k + 1) = x✝
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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 : 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
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))

Tactic:
rw [(truncGE.rightHomologyMapData K e hj' rfl rfl hj).quasiIso_iff]
    dsimp
    infer_instance

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

Goal state before:
pp: case inl
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : i < n
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i

Tactic:
apply (K.isZero_of_isStrictlyGE n i (by lia)).eq_of_src

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

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
⊢ Φ.homMap L₁ L₂ f = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
change e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = _

Goal state after:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y
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 B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
Iso.hom_inv_id_assoc,

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 B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j = (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv
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', ∃ (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b), ∃ g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
obtain ⟨Y', hY', g, s, hs, fac⟩ := left_fac_of_isStrictlyGE f a

Goal state after:
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)
⊢ ∃ Y', ∃ (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b), ∃ g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case h₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ Epi (homologyMap φ.τ₁ i)

pp: case h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ IsIso (homologyMap φ.τ₂ i)

pp: case h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)

pp: case h₄
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)

Tactic:
all_goals infer_instance

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

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ x = y

Tactic:
rw [← cancel_mono ((Q.commShiftIso b).inv.app _),
        ← cancel_epi ((Q.commShiftIso a).hom.app _)]

Goal state after:
case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      x ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y) =
    (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      y ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y)
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 : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ triangleOfSES hS ∈ distinguishedTriangles

Tactic:
mem_distTriang_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ ∃ X Y f, Nonempty (triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))
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 ≫
        (SmallHom.equiv W Q)
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃)) ≫
      (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    hS.singleδ

Tactic:
SmallHom.equiv_mk

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₁) =
    hS.singleδ
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₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
this : HasDerivedCategory C := ⋯
⊢ (h₁.extClass.comp (Ext.mk₀ f.τ₁) ⋯).hom = ((Ext.mk₀ f.τ₃).comp h₂.extClass ⋯).hom

Tactic:
simpa [ShiftedHom.comp_mk₀, ShiftedHom.mk₀_comp] using! (singleTriangle.map h₁ h₂ f).comm₃

Goal state after: