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
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 Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
n : ℕ
H : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ

Tactic:
extensionProductIter_succ

Goal state after:
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
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 Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
n : ℕ
H : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ
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 K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ : HomologicalComplex C c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : quasiIso C c f
hfg : quasiIso C c (f ≫ g)
⊢ quasiIso C c g

Tactic:
by
    rw [mem_quasiIso_iff] at hf hfg ⊢
    rwa [← quasiIso_iff_comp_left f g]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i i' : ℤ
hi : n + i = i'
⊢ n + (up ℤ).prev i = (up ℤ).prev i'

Tactic:
by simp only [prev]; lia

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
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle s

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
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
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
G' : E ⥤ E'
inst✝¹ : G.CommShift A
inst✝ : G'.CommShift A
n a a' : A
ha' : n + a = a'
⊢ (((F.postcomp G).postcomp G').shiftIso n a a' ha').hom ≫ ((F.functor a).associator G G').hom =
    whiskerRight ((F.functor a').associator G G').hom (shiftFunctor E' n) ≫
      ((F.postcomp (G ⋙ G')).shiftIso n a a' ha').hom

Tactic:
by
    ext X
    simp [Functor.commShiftIso_comp_inv_app]

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₃
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a = c ≫ T₂.mor₃

Tactic:
refine ⟨P.fullyFaithfulι.preimage c, ⟨by cat_disch, ?_⟩⟩

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₃
⊢ T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a = P.fullyFaithfulι.preimage c ≫ T₂.mor₃
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ (homologyFunctor C 0).shiftMap (ShiftedHom.map f Q) a a' h =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L

Tactic:
rw [← ShiftedHom.map_naturality_1 f (quotientCompQhIso C),
    ShiftedHom.mk₀_comp, ShiftedHom.comp_mk₀,
    Functor.shiftMap_comp', Functor.shiftMap_comp,
    ShiftedHom.comp_map, shiftMap_homologyFunctor_map_Qh ..,
    homologyFunctorFactorsh_hom_app_quotient_obj,
    homologyFunctorFactorsh_inv_app_quotient_obj,
    HomotopyCategory.homologyFunctor_shiftMap]
  simp [shift_homologyFunctor, ← Functor.map_comp, ← Functor.map_comp_assoc]

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
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b

Tactic:
simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]

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
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b

Tactic:
simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i : Option ι
hi : i = none
⊢ IsZero (X K i)

Tactic:
subst hi
  exact Limits.isZero_zero _

Goal state after:
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.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁) ≫
      (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv

Tactic:
assoc

Goal state after:
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.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁) ≫
      (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv
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 : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ extend.mapX φ (e.r i') = 0

Tactic:
rw [extend.mapX_none φ (e.r_eq_none i' hi')]

Goal state after:
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'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'✝ : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ (φ ≫ K.d j k) ≫ (K.extendXIso e hk').inv = 0 ↔ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0

Tactic:
assoc

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'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'✝ : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0 ↔ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : 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
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ f φ (e.f j)

Tactic:
f_eq φ rfl

Goal state after:
case pos
ι : 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
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).inv ≫ φ.f j ≫ (L.extendXIso e ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : 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
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi'
      rw [f_eq φ hi]
      by_cases hj' : ∃ j, e.f j = j'
      · obtain ⟨j, hj⟩ := hj'
        rw [f_eq φ hj, L.extend_d_eq e hi hj]
        subst hi hj
        simp [HomologicalComplex.restrictionXIso]
      · apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt
    · have : (L.extend e).d i' j' = 0 := by
        apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_src
      rw [this, comp_zero]
      by_cases hj' : ∃ j, e.f j = j'
      · obtain ⟨j, rfl⟩ := hj'
        rw [f_eq φ rfl]
        dsimp [restrictionXIso]
        rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]
      · have : f φ j' = 0 := by
          apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt
        rw [this, comp_zero]

Goal state after:
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 ↔ ((K.extendXIso e hi'').hom ≫ f') ≫ φ = 0

Tactic:
assoc

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.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'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : ((K.extendXIso e hj').hom ≫ h.p) ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv

Tactic:
assoc

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'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv
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 ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) ≫
        (K.sc j').homologyι =
    ((K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j') ≫ (K.sc j').homologyι

Tactic:
assoc

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

Tactic:
exact h j

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₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ ↑((fun x ↦
          match x with
          | ⟨i₁, h⟩ => ⟨indexOfBoundaryLE ac h, ⋯⟩)
        ((fun x ↦
            match x with
            | ⟨i₂, h⟩ => ⟨indexOfBoundaryGE ac h, ⋯⟩)
          ⟨i₂, h⟩)) =
    ↑⟨i₂, h⟩

Tactic:
have h' := of_boundaryGE ac h

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₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
h' : ac.Boundary (indexOfBoundaryGE ac h) i₂
⊢ ↑((fun x ↦
          match x with
          | ⟨i₁, h⟩ => ⟨indexOfBoundaryLE ac h, ⋯⟩)
        ((fun x ↦
            match x with
            | ⟨i₂, h⟩ => ⟨indexOfBoundaryGE ac h, ⋯⟩)
          ⟨i₂, h⟩)) =
    ↑⟨i₂, h⟩
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)
⊢ ∃ Y'_1,
    ∃ (_ : Y'_1.IsStrictlyGE n),
      ∃ g_1 s_1, ∃ (x : IsIso (Q.map s_1)), Q.map g ≫ inv (Q.map s) = Q.map g_1 ≫ inv (Q.map s_1)

Tactic:
have : IsIso (Q.map (CochainComplex.truncGEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    infer_instance

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)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ ∃ Y'_1,
    ∃ (_ : Y'_1.IsStrictlyGE n),
      ∃ g_1 s_1, ∃ (x : IsIso (Q.map s_1)), Q.map g ≫ inv (Q.map s) = Q.map g_1 ≫ inv (Q.map s_1)
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j = (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
← singleObjCyclesSelfIso_hom_naturality_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j =
    cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom ≫ (singleObjCyclesSelfIso c j B).inv
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ ((single C c j).obj A).iCycles j ≫
      (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv ≫ ((single C c j).obj B).pOpcycles j =
    (((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom) ≫
      f ≫ (singleObjXSelf c j B).inv ≫ ((single C c j).obj B).pOpcycles j

Tactic:
assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ ((single C c j).obj A).iCycles j ≫
      (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv ≫ ((single C c j).obj B).pOpcycles j =
    ((single C c j).obj A).iCycles j ≫
      (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv ≫ ((single C c j).obj B).pOpcycles j