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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} E
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : C₁ ⥤ E
hF : W₃.IsInvertedBy F
⊢ W₂.IsInvertedBy (h₁.lift F ⋯)

Tactic:
refine MorphismProperty.IsInvertedBy.of_le _ _ _ ?_ hW₂₃

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} E
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : C₁ ⥤ E
hF : W₃.IsInvertedBy F
⊢ (W₃.map L₁).IsInvertedBy (h₁.lift F ⋯)
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.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure

Tactic:
rw [retractClosure_le_iff]

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.retractClosure.extensionProduct Q.retractClosure ≤ (P.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 : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : L.ExactAt i
⊢ QuasiIsoAt f i ↔ K.ExactAt i

Tactic:
by
  simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff,
    ShortComplex.exact_iff_isZero_homology] at hL ⊢
  constructor
  · intro h
    exact IsZero.of_iso hL (@asIso _ _ _ _ _ h)
  · intro hK
    exact ⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩

Goal state after:
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 : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_iff_comp_right φ φ']

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 Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P.extensionProductIter 0 ≤ Q.isoClosure

Tactic:
rw [extensionProductIter_zero]
    exact h.trans Q.le_isoClosure

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 : ObjectProperty C
n : ℕ
⊢ (P.retractClosure.extensionProductIter n).retractClosure ≤ (P.extensionProductIter n).retractClosure

Tactic:
rw [retractClosure_le_iff]

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 : ObjectProperty C
n : ℕ
⊢ P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : quasiIso C c ((quotient C c).map f)
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
quotient_map_mem_quasiIso_iff

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : HomologicalComplex.quasiIso C c f
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)
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 (mappingCocone.triangle φ) ∈ distinguishedTriangles

Tactic:
by
  rw [rotate_distinguished_triangle]
  exact isomorphic_distinguished _ (mappingCone_triangle_distinguished φ) _
    (DerivedCategory.Q.mapTriangleRotateIso.app _ ≪≫
    DerivedCategory.Q.mapTriangle.mapIso (mappingCocone.rotateTriangleIso φ))

Goal state after:
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' : ι'
h : ¬c'.Rel i' j'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') = 0

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

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

Goal state before:
pp: case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Tactic:
rintro rfl

Goal state after:
case mpr
p : ℤ
⊢ (embeddingUpIntGE p).BoundaryGE 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Tactic:
· intro i hi
      dsimp at hi
      lia

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

Goal state before:
pp: case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntLE p).BoundaryLE n

Tactic:
rintro rfl

Goal state after:
case mpr
p : ℤ
⊢ (embeddingUpIntLE p).BoundaryLE 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
⊢ ∀ (k : ℕ), ¬(up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f k)

Tactic:
· intro i hi
      dsimp at hi
      lia

Goal state after:
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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i✝ j k : ι
hi✝ : c.prev j = i✝
hk : c.next j = k
i : ι
hi : e.BoundaryGE i
⊢ (K.truncGE' e).HasHomology i

Tactic:
exact ShortComplex.HasHomology.mk' (homologyData K e _ _ _ rfl rfl hi)

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

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.iCycles j = (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' ≫ (K.extendXIso e hj').hom

Tactic:
dsimp [extendCyclesIso, iCycles]

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).iCycles =
    ((K.sc j).homologyData.left.cyclesIso.hom ≫
        (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.inv) ≫
      ((K.extend e).sc j').iCycles ≫ (K.extendXIso e hj').hom
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ restrictionToTruncGE'.f K e j = 0

Tactic:
rw [restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv K e rfl hj]

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'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f j) ≫ (K.truncGE'XIsoOpcycles e ⋯ hj).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case inl
ι : 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✝² : Abelian C
K : HomologicalComplex C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst✝¹ : e₁.IsTruncLE
inst✝ : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₁ : ι₁
⊢ QuasiIsoAt (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)

Tactic:
have h₁ := ((ac.isSupportedOutside₁_iff (K.truncGE e₂)).2 inferInstance).exactAt i₁
      have h₂ := (K.shortComplexTruncLE_X₃_isSupportedOutside e₁).exactAt i₁
      simpa only [quasiIsoAt_iff_exactAt _ _ h₂] using h₁

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
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j =
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom

Tactic:
singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_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
⊢ ((single C c j).obj A).homologyπ j ≫ ((single C c j).obj A).homologyι j =
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom
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'
this : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso := e.symm }
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
let α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) _ _ e'.symm

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'
this : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso := e.symm }
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) G' G e'.symm
⊢ 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.DerivedCategory.Fractions

Goal state before:
pp: case refine_2
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))
⊢ Q.map g = inv (Q.map (X.ιTruncLE b)) ≫ Q.map (CochainComplex.truncLEMap g b ≫ Y'.ιTruncLE b)

Tactic:
CochainComplex.ιTruncLE_naturality g b,

Goal state after:
case refine_2
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))
⊢ Q.map g = inv (Q.map (X.ιTruncLE b)) ≫ Q.map (X.ιTruncLE b ≫ g)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (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 : ℤ),
      Small.{w, w'}
        ((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)))

Tactic:
· intro h X Y a b
    obtain hab | hab := le_or_gt a b
    · refine (small_congr ?_).1 (h X Y (b - a) (by simpa))
      exact (Functor.FullyFaithful.ofFullyFaithful
        (shiftFunctor _ a)).homEquiv.trans
        ((shiftFunctorAdd' _ _ _ _ (Int.sub_add_cancel b a)).symm.app _).homToEquiv
    · suffices Subsingleton ((Q.obj ((CochainComplex.singleFunctor C 0).obj X))⟦a⟧ ⟶
          (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))⟦b⟧) from inferInstance
      constructor
      intro x y
      rw [← cancel_mono ((Q.commShiftIso b).inv.app _),
        ← cancel_epi ((Q.commShiftIso a).hom.app _)]
      have : (((CochainComplex.singleFunctor C 0).obj X)⟦a⟧).IsStrictlyLE (-a) :=
        CochainComplex.isStrictlyLE_shift _ 0 _ _ (by lia)
      have : (((CochainComplex.singleFunctor C 0).obj Y)⟦b⟧).IsStrictlyGE (-b) :=
        CochainComplex.isStrictlyGE_shift _ 0 _ _ (by lia)
      apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE _ _ (-a) (-b) (by
        lia)).elim

Goal state after:
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
⊢ Ext S.X₃ S.X₁ 1

Tactic:
have := hS.hasSmallLocalizedHom_S'_X₃_K

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Ext S.X₃ S.X₁ 1
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 G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝¹ : A
x✝ : OppositeShift C A
⊢ (shiftFunctor (OppositeShift D A) x✝¹).map ((OppositeShift.natTrans A τ).app x✝) ≫
      (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).inv.app x✝ =
    (Functor.commShiftIso (OppositeShift.functor A G) x✝¹).inv.app x✝ ≫
      (OppositeShift.natTrans A τ).app ((shiftFunctor (OppositeShift C A) x✝¹).obj x✝)

Tactic:
exact (op_inj_iff _ _).mpr (NatTrans.shift_app_comm τ _ (unop _))

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0

Tactic:
by simpa only [map'_comp R₂ 0 1 2] using hR₂.toIsComplex.zero 0

Goal state after:
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
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x✝¹).hom ≫
          Functor.whiskerRight (OppositeShift.natIsoComp A F G).hom (shiftFunctor (OppositeShift E A) x✝¹)).app
      x✝ =
    ((shiftFunctor (OppositeShift C A) x✝¹).whiskerLeft (OppositeShift.natIsoComp A F G).hom ≫
          (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝¹).hom).app
      x✝

Tactic:
dsimp [OppositeShift.natIsoComp, Functor.commShiftOp_iso_eq]

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
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (F ⋙ G) x✝¹).inv.app (Opposite.unop x✝)).op ≫
      (shiftFunctor (OppositeShift E A) x✝¹).map (𝟙 ((OppositeShift.functor A (F ⋙ G)).obj x✝)) =
    𝟙 ((OppositeShift.functor A (F ⋙ G)).obj ((shiftFunctor (OppositeShift C A) x✝¹).obj x✝)) ≫
      (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝¹).hom.app x✝
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₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
⊢ isoWhiskerRight (pullbackShiftIso C φ 0 (φ 0) ⋯) F ≪≫
      commShiftIso F (φ 0) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ 0 (φ 0) ⋯).symm =
    CommShift.isoZero (PullbackShift.functor φ F) A

Tactic:
by
    ext
    dsimp
    simp only [F.commShiftIso_zero' (A := B) (φ 0) (by rw [map_zero]), CommShift.isoZero'_hom_app,
      assoc, CommShift.isoZero_hom_app, pullbackShiftFunctorZero'_hom_app, map_comp,
      pullbackShiftFunctorZero'_inv_app]
    rfl

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
⊢ e₁ = e₁'

Tactic:
ext
  rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]

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

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
refine exact₂_mk _ (by simp) ?_

Goal state after:
case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ {
      X₁ :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact