mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : D ⥤ E
inst✝ : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ 𝟙 ((shiftFunctor E (m + n)).obj (G.obj ((F.functor a'').obj X))) ≫
      (commShiftIso G (m + n)).inv.app ((F.functor a'').obj X) ≫
        𝟙 (G.obj ((shiftFunctor D (m + n)).obj ((F.functor a'').obj X))) ≫
          G.map ((F.shiftIso (m + n) a a'' ⋯).hom.app X) =
    (shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫
      𝟙 ((shiftFunctor E n).obj ((shiftFunctor E m).obj (G.obj ((F.functor a'').obj X)))) ≫
        (shiftFunctor E n).map
            (𝟙 ((shiftFunctor E m).obj (G.obj ((F.functor a'').obj X))) ≫
              (commShiftIso G m).inv.app ((F.functor a'').obj X) ≫
                𝟙 (G.obj ((shiftFunctor D m).obj ((F.functor a'').obj X))) ≫
                  G.map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
          𝟙 ((shiftFunctor E n).obj (G.obj ((F.functor a').obj X))) ≫
            (commShiftIso G n).inv.app ((F.functor a').obj X) ≫
              𝟙 (G.obj ((shiftFunctor D n).obj ((F.functor a').obj X))) ≫ G.map ((F.shiftIso n a a' ha').hom.app X)

Tactic:
simp only [F.shiftIso_add_hom_app n m a a' a'' ha' ha'', Functor.commShiftIso_add,
      Functor.CommShift.isoAdd_inv_app, Functor.map_comp, id_comp, assoc,
      Functor.commShiftIso_inv_naturality_assoc]

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
G : D ⥤ E
inst✝ : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫
      (shiftFunctor E n).map ((commShiftIso G m).inv.app ((F.functor a'').obj X)) ≫
        (commShiftIso G n).inv.app ((shiftFunctor D m).obj ((F.functor a'').obj X)) ≫
          G.map ((shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)) ≫
            G.map ((shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X)) ≫
              G.map ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
                G.map ((F.shiftIso n a a' ha').hom.app X) =
    (shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫
      (shiftFunctor E n).map ((commShiftIso G m).inv.app ((F.functor a'').obj X)) ≫
        (commShiftIso G n).inv.app ((shiftFunctor D m).obj ((F.functor a'').obj X)) ≫
          G.map ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
            G.map ((F.shiftIso n a a' ha').hom.app X)
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
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.limitsOfShape (Discrete WalkingPair) ≤ P

Tactic:
rintro X ⟨p⟩
    refine P.prop_of_iso ?_ (P.ext_of_isTriangulatedClosed₂ _
      (binaryProductTriangle_distinguished _ _)
      (p.prop_diag_obj (.mk .left)) (p.prop_diag_obj (.mk .right)))
    exact IsLimit.conePointUniqueUpToIso (prodIsProd _ _)
      ((IsLimit.postcomposeHomEquiv (diagramIsoPair p.diag) _).2 p.isLimit)

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₁
c : (P.ι.mapTriangle.obj T₁).obj₃ ⟶ (P.ι.mapTriangle.obj T₂).obj₃
hc₁ : (P.ι.mapTriangle.obj T₁).mor₂ ≫ c = P.ι.map b ≫ (P.ι.mapTriangle.obj T₂).mor₂
hc₂ : (P.ι.mapTriangle.obj T₁).mor₃ ≫ (shiftFunctor C 1).map (P.ι.map a) = c ≫ (P.ι.mapTriangle.obj T₂).mor₃
this :
  P.ι.map ((shiftFunctor P.FullSubcategory 1).map a) ≫ (Functor.commShiftIso P.ι 1).hom.app T₂.obj₁ =
    (Functor.commShiftIso P.ι 1).hom.app T₁.obj₁ ≫ (shiftFunctor C 1).map (P.ι.map a)
⊢ (T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a).hom = (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom

Tactic:
← cancel_mono ((Functor.commShiftIso P.ι (1 : ℤ)).hom.app T₂.obj₁)

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
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₁
c : (P.ι.mapTriangle.obj T₁).obj₃ ⟶ (P.ι.mapTriangle.obj T₂).obj₃
hc₁ : (P.ι.mapTriangle.obj T₁).mor₂ ≫ c = P.ι.map b ≫ (P.ι.mapTriangle.obj T₂).mor₂
hc₂ : (P.ι.mapTriangle.obj T₁).mor₃ ≫ (shiftFunctor C 1).map (P.ι.map a) = c ≫ (P.ι.mapTriangle.obj T₂).mor₃
this :
  P.ι.map ((shiftFunctor P.FullSubcategory 1).map a) ≫ (Functor.commShiftIso P.ι 1).hom.app T₂.obj₁ =
    (Functor.commShiftIso P.ι 1).hom.app T₁.obj₁ ≫ (shiftFunctor C 1).map (P.ι.map a)
⊢ (T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a).hom ≫ (Functor.commShiftIso P.ι 1).hom.app T₂.obj₁ =
    (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom ≫ (Functor.commShiftIso P.ι 1).hom.app T₂.obj₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁)

Tactic:
rw [← cancel_mono (HomotopyCategory.isoOfHomotopyEquiv
      (mappingConeCompHomotopyEquiv f g)).inv, assoc]
  dsimp [mappingConeCompTriangleh]
  rw [← Functor.map_comp, ← Functor.map_comp, ← Functor.map_comp,
    mappingConeCompHomotopyEquiv_hom_inv_id, comp_id,
    mappingConeCompHomotopyEquiv_comm₁ f g,
    mappingConeCompTriangle_mor₂]

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

Goal state before:
pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

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

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

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 : ι
i' j' : ι'
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.restriction e).d i j = (K.restrictionXIso e hi).hom ≫ K.d i' j' ≫ (K.restrictionXIso e hj).inv

Tactic:
subst hi hj
  simp [restrictionXIso]

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

Goal state before:
pp: case neg
ι : 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
hjk' : ¬c.Rel j k
⊢ c'.next (e.f j) = e.f k

Tactic:
obtain rfl : j = k := by
      simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hjk : c.next j = j
hjk' : ¬c.Rel j j
⊢ c'.next (e.f j) = e.f j
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
⊢ f φ i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv

Tactic:
have hi' : ∃ k, e.f k = i' := ⟨i, hi⟩
  have : hi'.choose = i := e.injective_f (by rw [hi'.choose_spec, hi])
  grind [f]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
hk : ¬∃ k, e.f k = k'
⊢ ∀ (i : ι), e.f i ≠ k'

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ¬∃ j, e.f j = j'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
i : ι
hi : e.f i = i'
⊢ (K.restrictionXIso e hi).symm.hom ≫ (Arrow.mk (φ.f i)).hom =
    (Arrow.mk ((e.liftExtend φ hφ).f i')).hom ≫ (L.extendXIso e hi).hom

Tactic:
simp [e.liftExtend_f φ hφ hi]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
hj : ¬∃ j, e.f j = j'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : (e.extendFunctor C).obj K ⟶ (e.extendFunctor C).obj L
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto

Goal state after:
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'

Tactic:
dsimp [restrictionHomologyIso, homologyIsoSc']

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.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.restriction e).homologyπ j ≫
      ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e)) ≫
        ShortComplex.homologyMap (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫
          ShortComplex.homologyMap ((natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'
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 M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : ∀ (j : ι), K.HasHomology j
j' : ι'
h : ¬∃ j, e.f j = j'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
tauto

Goal state after:
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv ≫ (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
dsimp [restrictionHomologyIso, homologyIsoSc']

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.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
⊢ ((ShortComplex.homologyMap ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K) ≫
          ShortComplex.homologyMap (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv) ≫
        ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).inv.app (K.restriction e))) ≫
      (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case mp
ι : 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'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
⊢ (∀ (i : ι'), QuasiIsoAt (extendMap φ e) i) → ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)

Tactic:
tauto

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 : 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:
let φ := (shortComplexFunctor C c' j').map (K.πTruncGE e)
    have : Epi φ.τ₁ := by
      by_cases hi : ∃ i, e.f i = c'.prev j'
      · obtain ⟨i, hi⟩ := hi
        dsimp [φ, πTruncGE]
        rw [e.epi_liftExtend_f_iff _ _ hi]
        infer_instance
      · apply IsZero.epi (isZero_extend_X _ _ _ (by simpa using hi))
    have : IsIso φ.τ₂ := by
      dsimp [φ, πTruncGE]
      rw [e.isIso_liftExtend_f_iff _ _ hj']
      exact K.isIso_restrictionToTruncGE' e j hj
    have : IsIso φ.τ₃ := by
      dsimp [φ, πTruncGE]
      have : c'.next j' = e.f (c.next j) := by simpa only [← hj'] using e.next_f rfl
      rw [e.isIso_liftExtend_f_iff _ _ this.symm]
      exact K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)
    exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_5
i j k : ι
hij : i = j
hjk : j = k
x : X i
⊢ (aux X j k hjk) ((aux X i j hij) x) = (aux X i k ⋯) x

Tactic:
by
  subst hij hjk
  rfl

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'
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
this : e = e' ≪≫ L₁.isoWhiskerLeft α
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
simp [this]

Goal state after:
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 ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
⊢ QuasiIso (CochainComplex.truncGEMap s n)

Tactic:
CochainComplex.quasiIso_truncGEMap_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i
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.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)
hs : QuasiIso s
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
⊢ QuasiIso (CochainComplex.truncGEMap s a)

Tactic:
CochainComplex.quasiIso_truncGEMap_iff

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.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)
hs : QuasiIso s
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
⊢ ∀ (i : ℤ), a ≤ i → QuasiIsoAt s i
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 : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
this : ∀ (f : Q.obj X ⟶ Q.obj Y), f = 0
⊢ ∀ (a b : Q.obj X ⟶ Q.obj Y), a = b

Tactic:
simp [this]

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C M
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (equiv W W.Q) ((α.comp β h₁₂).comp γ ⋯) = (equiv W W.Q) (α.comp (β.comp γ h₂₃) ⋯)

Tactic:
simp only [equiv_comp, ShiftedHom.comp_assoc _ _ _ h₁₂ h₂₃ h]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ IsZero (S.X₁.homology j)

Tactic:
· have := hS.mono_f
    have := HomologicalComplex.mono_homologyMap_of_mono_of_not_rel S.f j hj
    rw [IsZero.iff_id_eq_zero,
      ← cancel_mono (HomologicalComplex.homologyMap S.f j),
      ← cancel_mono (HomologicalComplex.homologyMap S.g j)]
    simp [← HomologicalComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
⊢ S.X₃.ExactAt i

Tactic:
rw [exactAt_iff_isZero_homology]
  by_cases! hi : ∃ j, c.Rel i j
  · obtain ⟨j, hij⟩ := hi
    have := h₂ j hij
    apply (hS.homology_exact₃ i j hij).isZero_X₂
    · simp [← cancel_epi (HomologicalComplex.homologyMap S.f i),
        ← HomologicalComplex.homologyMap_comp]
    · simp [← cancel_mono (HomologicalComplex.homologyMap S.f j)]
  · have := hS.epi_g
    have := HomologicalComplex.epi_homologyMap_of_epi_of_not_rel S.g i hi
    rw [IsZero.iff_id_eq_zero,
      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]
    simp [← HomologicalComplex.homologyMap_comp]

Goal state after: