mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case succ
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
⊢ P.extensionProductIter (n + 1) ≤ Q.isoClosure

Tactic:
rw [extensionProductIter_succ]
    exact extensionProduct_le_of_isTriangulatedClosed₂ (h.trans Q.le_isoClosure) H

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

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)

Tactic:
have eq₁ := (P.inverseImage F).trW_iff_of_distinguished _ hT

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
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
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW (Triangle.mk s g h).mor₁ ↔ P.inverseImage F (Triangle.mk s g h).obj₃
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

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

Tactic:
simp [Functor.shiftMap, homologyFunctor_shift, homologyδOfTriangle]

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)

Goal state after:
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₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      X₂ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      f := DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h,
      g := (DerivedCategory.homologyFunctor C n₁).map (DerivedCategory.Q.mapTriangle.obj T).mor₁, zero := ⋯ } ≅
    { 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 := ⋯ }
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 M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
⊢ extendMap (φ ≫ φ') e = extendMap φ e ≫ extendMap φ' e

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

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
⊢ c'.next (e.f j) = e.f k

Tactic:
by_cases hjk' : c.Rel j k
  · exact c'.next_eq' (by simpa only [e.rel_iff] using hjk')
  · obtain rfl : j = k := by
      simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk
    apply c'.next_eq_self
    intro hj'
    simp only [BoundaryLE, not_and, not_forall, not_not] at hj
    obtain ⟨k, hk⟩ := hj hj'
    rw [e.rel_iff] at hk
    rw [c.next_eq' hk] at hjk
    exact hjk' (by simpa only [hjk] using hk)

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
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
by
  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
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'

Tactic:
← this,

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
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j'
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
this : (K.extendXIso e hi'').hom ≫ f' = f''
⊢ (K.extendXIso e hi'').hom ≫ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
← this,

Goal state after:
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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
this : (K.extendXIso e hi'').hom ≫ f' = f''
⊢ (K.extendXIso e hi'').hom ≫ f' ≫ φ = 0 ↔ ((K.extendXIso e hi'').hom ≫ f') ≫ φ = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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

Tactic:
shape _ _ _ hjk,

Goal state after:
case neg
ι : 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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: case e_a
ι : 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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ K.homologyπ j' ≫ (K.sc j').homologyι = K.iCycles j' ≫ (K.sc j').pOpcycles

Tactic:
apply ShortComplex.homology_π_ι

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ k = j

Tactic:
rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : 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'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d k k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
shape _ _ _ hjk,

Goal state after:
case neg
ι : 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'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ 0 ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv
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.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv = (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j'

Tactic:
rw [← cancel_mono (K.extendOpcyclesIso e hj').hom, assoc, assoc, Iso.inv_hom_id, comp_id]

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.pOpcycles j = (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom
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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ IsIso (homologyMap (extendMap φ e) j') ↔ IsIso (homologyMap φ j)

Tactic:
exact (MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.extendHomologyIso e hj') (L.extendHomologyIso e 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₂
K L : HomologicalComplex C c
x✝ : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
⊢ ↑((fun x ↦
          match x with
          | ⟨i₂, h⟩ => ⟨indexOfBoundaryGE ac h, ⋯⟩)
        ((fun x ↦
            match x with
            | ⟨i₁, h⟩ => ⟨indexOfBoundaryLE ac h, ⋯⟩)
          ⟨i₁, h⟩)) =
    ↑⟨i₁, h⟩

Tactic:
have h'' := of_boundaryGE ac h'.snd

Goal state after:
ι : 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₂
K L : HomologicalComplex C c
x✝ : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
h'' : ac.Boundary (indexOfBoundaryGE ac ⋯) (indexOfBoundaryLE ac h)
⊢ ↑((fun x ↦
          match x with
          | ⟨i₂, h⟩ => ⟨indexOfBoundaryGE ac h, ⋯⟩)
        ((fun x ↦
            match x with
            | ⟨i₁, h⟩ => ⟨indexOfBoundaryLE ac h, ⋯⟩)
          ⟨i₁, h⟩)) =
    ↑⟨i₁, h⟩
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
⊢ (∃ i₁, (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ i₂, (embeddingUpIntGE n₁).f i₂ = i

Tactic:
by
    by_cases hi : i ≤ n₀
    · obtain ⟨k, rfl⟩ := Int.exists_add_of_le hi
      exact Or.inl ⟨k, by dsimp; lia⟩
    · obtain ⟨k, rfl⟩ := Int.exists_add_of_le (show n₁ ≤ i by lia)
      exact Or.inr ⟨k, rfl⟩

Goal state after:
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.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ f =
    inv (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a))) ≫
      Q.map (CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a))

Tactic:
simp only [Functor.map_comp, Functor.map_inv, IsIso.inv_comp, IsIso.inv_inv, assoc, fac,
      ← cancel_epi (Q.map s), IsIso.hom_inv_id_assoc]

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.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ Q.map g =
    Q.map s ≫
      Q.map (X.πTruncGE a) ≫
        inv (Q.map (CochainComplex.truncGEMap s a)) ≫ Q.map (CochainComplex.truncGEMap g a) ≫ inv (Q.map (Y.πTruncGE a))
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₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))) ≫
      G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
← this,

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
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₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    ((shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y))) ≫
      G.map ((shiftFunctor D a).map (adj.counit.app Y))
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ ((opEquiv a).symm f).comp z h = (opEquiv a).symm (Quiver.Hom.op z ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
ShiftedHom.opEquiv_symm_apply,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ comp
      (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f))
      z h =
    (opEquiv a).symm (Quiver.Hom.op z ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ comp
      (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f))
      z h =
    (opEquiv a).symm (Quiver.Hom.op z ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
ShiftedHom.opEquiv_symm_apply,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ comp
      (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f))
      z h =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatIso.ofComponents
      (fun A ↦
        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm;
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
      ⋯ =
    Functor.isoWhiskerRight (shiftFunctorAdd Cᵒᵖ m n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
      (shiftFunctor Cᵒᵖ m).associator (shiftFunctor Cᵒᵖ n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
        (shiftFunctor Cᵒᵖ m).isoWhiskerLeft
            (NatIso.ofComponents
              (fun A ↦
                (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' ha').symm;
                  { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
              ⋯) ≪≫
          NatIso.ofComponents
            (fun A ↦
              (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' m a' a'' ha'').symm;
                { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
            ⋯

Tactic:
ext _ x

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x✝ : Cᵒᵖ
x : ↑((shiftFunctor Cᵒᵖ (m + n) ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x✝)
⊢ (AddCommGrpCat.Hom.hom
        ((NatIso.ofComponents
                (fun A ↦
                  (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm;
                    { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                ⋯).hom.app
          x✝))
      x =
    (AddCommGrpCat.Hom.hom
        ((Functor.isoWhiskerRight (shiftFunctorAdd Cᵒᵖ m n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                (shiftFunctor Cᵒᵖ m).associator (shiftFunctor Cᵒᵖ n)
                    (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                  (shiftFunctor Cᵒᵖ m).isoWhiskerLeft
                      (NatIso.ofComponents
                        (fun A ↦
                          (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' ha').symm;
                            { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                        ⋯) ≪≫
                    NatIso.ofComponents
                      (fun A ↦
                        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' m a' a'' ha'').symm;
                          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                      ⋯).hom.app
          x✝))
      x
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π = 𝟙 ((singleFunctor C i).obj P)

Tactic:
by
      apply HomologicalComplex.from_single_hom_ext
      rw [comp_f, mkHomFromSingle_f, assoc, id_f, this, Projective.factorThru_comp_assoc,
        id_comp, Iso.hom_inv_id]
      rfl

Goal state after: