mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

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

Tactic:
let : Q.IsClosedUnderIsomorphisms := IsClosedUnderBinaryProducts.closedUnderIsomorphisms Q

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
this : Q.IsClosedUnderIsomorphisms := IsClosedUnderBinaryProducts.closedUnderIsomorphisms 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
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Fan f
hF : IsLimit F
h : ∀ (j : J), P (f j)
⊢ ∀ (j : Discrete J), P ((Discrete.functor f).obj j)

Tactic:
intro ⟨j⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Fan f
hF : IsLimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P ((Discrete.functor f).obj { as := j })
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Cofan f
hF : IsColimit F
h : ∀ (j : J), P (f j)
⊢ ∀ (j : Discrete J), P ((Discrete.functor f).obj j)

Tactic:
intro ⟨j⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Cofan f
hF : IsColimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P ((Discrete.functor f).obj { as := j })
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯

Tactic:
rw [F₁.map_id, comp_id]

Goal state after:
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
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
⊢ F.IsHomological

Tactic:
by
  have : F.PreservesZeroMorphisms := preservesZeroMorphisms_of_map_zero_object
    (F.mapIso L.mapZeroObject.symm ≪≫ e.app _ ≪≫ G.mapZeroObject)
  have : (L ⋙ F).IsHomological := IsHomological.of_iso e.symm
  refine IsHomological.mk' _ (fun T hT => ?_)
  rw [L.distTriang_iff] at hT
  obtain ⟨T₀, e, hT₀⟩ := hT
  exact ⟨L.mapTriangle.obj T₀, e, (L ⋙ F).map_distinguished_exact _ hT₀⟩

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✝
W : MorphismProperty Cᵒᵖ
h : W.HasRightCalculusOfFractions
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ Y' t, ∃ (_ : W.unop t), f₁ ≫ t = f₂ ≫ t

Tactic:
obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)
    exact ⟨Opposite.unop Y', t.unop, ht, Quiver.Hom.op_inj fac⟩

Goal state after:
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
f : X ⟶ Y
g : Y ⟶ Z
a : M
ha : a = 0
d : M
h : ShiftedHom Z T d
⊢ d + a = d

Tactic:
rw [ha, add_zero]

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

Goal state before:
pp: case zero
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)

Tactic:
rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']

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 : ObjectProperty C
n✝ : P.ContainsZero
n m✝ m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter m ≤ P.extensionProduct (P.extensionProductIter m)

Tactic:
exact le_extensionProduct_right P

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✝ : 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:
simpa using P.ι.congr_map comm

Goal state after:
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:
dsimp [embeddingUp'Add]

Goal state after:
ι : 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
⊢ (Embedding.mk' (up' a) (up' a) (fun x ↦ x + b) ⋯ ⋯).IsRelIff
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝² : (K.restriction e).HasHomology j
this✝¹ : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e k (e.not_boundaryGE_next' hj hk)

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝³ : (K.restriction e).HasHomology j
this✝² : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ((K.truncGE' e).sc' i j k).HasHomology
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.homologyπ j' ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ≫ (K.restriction e).homologyπ j

Tactic:
rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_assoc]

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 φ.τ₁
⊢ IsIso ((K.restrictionToTruncGE' e).f j)

Tactic:
exact K.isIso_restrictionToTruncGE' e j hj

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i j : ι
hij : i = j
⊢ X i ≃ X j

Tactic:
by
  subst hij
  rfl

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

Goal state before:
pp: ι : 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₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
i₂ : ι₂
hi₂ : c.next (e₁.f i₁) = e₂.f i₂
⊢ ∃ i₂, ac.Boundary i₁ i₂

Tactic:
exact ⟨i₂, by simpa only [hi₂] using! h₁⟩

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₂
⊢ Φ.homMap L₁ L₂ f = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
let e' := CatCommSq.iso Φ.functor L₁ L₂ G'

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'
⊢ Φ.homMap L₁ L₂ f = 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 : C
this : IsIso (((single C c j).obj A).iCycles j)
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j ≫ (singleObjOpcyclesSelfIso c j A).inv =
    ((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom

Tactic:
← HomologicalComplex.homology_π_ι_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 : C
this : IsIso (((single C c j).obj A).iCycles j)
⊢ ((single C c j).obj A).homologyπ j ≫ ((single C c j).obj A).homologyι j ≫ (singleObjOpcyclesSelfIso c j A).inv =
    ((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

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

Tactic:
have : IsIso (Q.map (CochainComplex.truncLEMap s b)) := by
    rw [isIso_Q_map_iff_quasiIso] at hs
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
    infer_instance

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)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ ∃ Y', ∃ (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b), ∃ g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
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₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁵ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝⁴ : L₂.IsLocalization W₂
X Y : C₁
inst✝³ : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst✝² : HasSmallLocalizedHom W₂ X' X'
inst✝¹ : HasSmallLocalizedHom W₂ X' Y'
inst✝ : HasSmallLocalizedHom W₂ Y' Y'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
⊢ (SmallHom.equiv W₂ L₂) (Φ.smallHomMap' eX eY f) =
    L₂.map eX.inv ≫ e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) f) ≫ e.inv.app Y ≫ L₂.map eY.hom

Tactic:
by
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Y')
  simp [smallHomMap', SmallHom.equiv_comp, Φ.equiv_smallHomMap L₁ L₂ G e]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
← cancel_mono (app' φ 3 _),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ (f₂ ≫ R₁.map' 2 3 ⋯ ⋯) ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
    0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
⊢ hom 0 = 0

Tactic:
have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
this : 0 = comp 0 β ⋯
⊢ hom 0 = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp α'.hom ⋯ = α.hom

Tactic:
dsimp [α']

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp ((mk₀ biprod.fst).comp α ⋯).hom ⋯ = α.hom
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
← cancel_mono (app' φ 3 _),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ (f₂ ≫ R₁.map' 2 3 ⋯ ⋯) ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
    0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
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
a b : A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝))).op ≫
      ((commShiftIso F b).inv.app ((shiftFunctor C a).obj (Opposite.unop x✝))).op ≫
        ((shiftFunctor D b).map ((commShiftIso F a).inv.app (Opposite.unop x✝))).op ≫
          ((shiftFunctorAdd D a b).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorAdd (OppositeShift C A) a b).hom.app x✝) ≫
      ((commShiftIso F b).inv.app (Opposite.unop ((shiftFunctor (OppositeShift C A) a).obj x✝))).op ≫
        (shiftFunctor (OppositeShift D A) b).map ((commShiftIso F a).inv.app (Opposite.unop x✝)).op ≫
          ((shiftFunctorAdd D a b).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op

Tactic:
oppositeShiftFunctorAdd_hom_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
a b : A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝))).op ≫
      ((commShiftIso F b).inv.app ((shiftFunctor C a).obj (Opposite.unop x✝))).op ≫
        ((shiftFunctor D b).map ((commShiftIso F a).inv.app (Opposite.unop x✝))).op ≫
          ((shiftFunctorAdd D a b).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝)).op ≫
      ((commShiftIso F b).inv.app (Opposite.unop ((shiftFunctor (OppositeShift C A) a).obj x✝))).op ≫
        (shiftFunctor (OppositeShift D A) b).map ((commShiftIso F a).inv.app (Opposite.unop x✝)).op ≫
          ((shiftFunctorAdd D a b).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op