mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ (OfComp.iso e (a + b)).hom.app X = (isoAdd (OfComp.iso e a) (OfComp.iso e b)).hom.app X

Tactic:
apply G.map_injective

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ G.map ((OfComp.iso e (a + b)).hom.app X) = G.map ((isoAdd (OfComp.iso e a) (OfComp.iso e b)).hom.app X)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
h : IsZero T.obj₂
⊢ T ∈ distinguishedTriangles ↔ IsIso T.mor₃

Tactic:
by
  rw [rotate_distinguished_triangle, distinguished_iff_of_isZero₁ _ h]
  simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ (inl φ).v p q hpq ≫ (triangle φ).mor₃.f q = -(K.shiftFunctorObjXIso 1 q p ⋯).inv

Tactic:
dsimp [triangle]
  -- the following list of lemmas was obtained by doing
  -- simp? [Cochain.rightShift_v _ 1 0 (zero_add 1) q q (add_zero q) p (by lia)]
  simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
    Cochain.rightShift_v _ 1 0 (zero_add 1) q q (add_zero q) p (by lia), shiftFunctor_obj_X,
    shiftFunctorObjXIso, Preadditive.comp_neg, inl_v_fst_v_assoc]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁰ : Category.{v_1, u_1} C
inst✝¹⁹ : Category.{v_2, u_2} D
inst✝¹⁸ : Category.{v_3, u_3} E
inst✝¹⁷ : HasShift C ℤ
inst✝¹⁶ : HasShift D ℤ
inst✝¹⁵ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝¹³ : G.CommShift ℤ
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
⊢ (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).mor₁ ≫ prodComparison F X₁ X₃ =
    𝟙 (F.mapTriangle.obj (binaryProductTriangle X₁ X₃)).obj₁ ≫ (binaryProductTriangle (F.obj X₁) (F.obj X₃)).mor₁

Tactic:
dsimp
        ext
        · simp only [assoc, prodComparison_fst, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_left, BinaryFan.mk_fst,
            ← F.map_comp, F.map_id]
        · simp only [assoc, prodComparison_snd, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_right, BinaryFan.mk_snd,
            ← F.map_comp, F.map_zero]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T.rotate ∈ distinguishedTriangles

Tactic:
rotate_distinguished_triangle

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T.rotate.rotate ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = 𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) p ≫ 𝟙 (Φ.obj b✝)
⊢ Φ.map (p.cons f') =
    𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) (p.cons f') ≫ 𝟙 (Φ.obj c✝)

Tactic:
| cons p f' ih =>

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y b✝ c✝ : Paths V
g : Quiver.Path X b✝
e : b✝ ⟶ c✝
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ F.map g ≫ F.map e.toPath = eqToHom ⋯ ≫ G.map (g.cons e) ≫ eqToHom ⋯

Tactic:
G.map_comp g (Quiver.Hom.toPath e),

Goal state after:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y b✝ c✝ : Paths V
g : Quiver.Path X b✝
e : b✝ ⟶ c✝
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ F.map g ≫ F.map e.toPath = eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W (z₁.s ≫ t₁ ≫ v₄ ≫ w)

Tactic:
rw [← reassoc_of% fac, ← reassoc_of% hsu, ← Category.assoc]

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s ≫ u₂) ≫ v₅ ≫ w)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
x✝⁵ x✝⁴ x✝³ : D
x✝² x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² + x✝¹) ≫ x✝ = x✝² ≫ x✝ + x✝¹ ≫ x✝

Tactic:
apply Preadditive.add_comp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
this : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ
⊢ HasCardinalLT (Subtype (P₁ ⊔ P₂)) κ

Tactic:
refine this.of_surjective (Sum.elim (fun x ↦ ⟨x.1, Or.inl x.2⟩)
    (fun x ↦ ⟨x.1, Or.inr x.2⟩)) ?_

Goal state after:
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
this : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ
⊢ Function.Surjective (Sum.elim (fun x ↦ ⟨↑x, ⋯⟩) fun x ↦ ⟨↑x, ⋯⟩)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case inr
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (Order.succ m) P (limit F)

Tactic:
transfiniteIterate_succ _ _ _ (by simp)

Goal state after:
case inr
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) m P).strictLimitsClosureStep J (limit F)
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (-(F.shiftIso (-1) n₁ n₀ ⋯).hom.app T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h =
    (F.shift n₁).map (-(shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁) ≫
      𝟙 ((F.shift n₁).obj T.obj₁)

Tactic:
simp only [homologySequenceδ, neg_comp, map_neg, comp_id,
    F.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero T.mor₃ (-1) (neg_add_cancel 1) n₀ n₁
      (by lia)]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ (mk₀ a ha f).comp (mk₀ b hb g) h = mk₀ c ⋯ (f ≫ g)

Tactic:
by
  subst ha hb
  obtain rfl : c = 0 := by rw [← h, zero_add]
  rw [mk₀_comp, mk₀, mk₀, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P.retracts ≤ P

Tactic:
by
  rwa [← isStableUnderRetracts_iff_retracts_le]

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.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ distinguishedTriangles
X₁ : C
h₁ : P X₁
e₁ : T.obj₁ ≅ X₁
X₃ : C
h₃ : P X₃
e₃ : T.obj₃ ≅ X₃
⊢ (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom)).mor₃ ≫
      (shiftFunctor C 1).map e₁.symm.hom =
    e₃.symm.hom ≫ T.mor₃

Tactic:
dsimp
          simp only [assoc, ← Functor.map_comp, e₁.hom_inv_id,
            Functor.map_id, comp_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁶ : Category.{v_1, u_1} C
inst✝¹⁵ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : HasZeroObject C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
inst✝⁹ : HasShift D ℤ
inst✝⁸ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : W.HasLeftCalculusOfFractions
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.IsTriangulated
inst✝ : IsTriangulated C
⊢ IsTriangulated D

Tactic:
have := essSurj_mapComposableArrows L W 2

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
L : C ⥤ D
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : HasZeroObject C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
inst✝⁹ : HasShift D ℤ
inst✝⁸ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : W.HasLeftCalculusOfFractions
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.IsTriangulated
inst✝ : IsTriangulated C
this : (L.mapComposableArrows 2).EssSurj
⊢ IsTriangulated D
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ ((single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj X).X i =
    ((single C (ComplexShape.up ℤ) a).obj X).X i

Tactic:
dsimp [single]

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ (if i + n = a + n then X else 0) = if i = a then X else 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n : ℤ
⊢ (singleFunctor C n).Additive

Tactic:
by
  dsimp only [singleFunctor, singleFunctors, SingleFunctors.postcomp]
  infer_instance

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✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
obtain ⟨Z, f, g, H, mem⟩ := φ.hs
    obtain ⟨X', f', h', mem'⟩ := distinguished_cocone_triangle₁ (φ.f ≫ f)
    obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ _
      mem' H φ.f (𝟙 Z) (by simp)
    exact ⟨MorphismProperty.RightFraction.mk f' ⟨_, _, _, mem', mem⟩ a, ha₁⟩

Goal state after:
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:
rotate_distinguished_triangle

Goal state after:
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 φ)).rotate ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X✝ Y✝ : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.symm.Rel i j
⊢ (f.unop.f i).unop ≫ (unop Y✝).unop.d i j = (unop X✝).unop.d i j ≫ (f.unop.f j).unop

Tactic:
by simp only [unop_d, ← unop_comp, f.unop.comm]

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

Goal state before:
pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)

Tactic:
· intro k hk
    apply hk' k
    rw [← c'.next_eq' hj, c'.next_eq' hk]

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 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
⊢ e.f k = k'

Tactic:
rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]

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

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
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
⊢ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

Tactic:
rw [K.extend_d_from_eq_zero e j' k' j hj', comp_zero, comp_zero]

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
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
⊢ ¬c.Rel j (c.next 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 : 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
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
by_cases hij : c.Rel i j
  · have hi'' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
    have : (K.extendXIso e hi'').hom ≫ f' = f'' := by
      apply Fork.IsLimit.hom_ext hcone
      rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
    rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, assoc]
  · have h₁ : f' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      simp only [zero_comp, hf', K.shape _ _ hij]
    have h₂ : f'' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']
      rw [hi]
      exact hij
    simp [h₁, h₂]

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'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
⊢ e.f k = k'

Tactic:
rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]

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'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
hk'' : e.f k = k'
⊢ Cofork.π cocone ≫ f' ≫ (K.extendXIso e hk'').inv = Cofork.π cocone ≫ f''

Tactic:
rw [reassoc_of% hf', ← cancel_epi (extendXIso K e hj').hom, hf'',
        K.extend_d_eq e hj' hk'']

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

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
rw [f_eq_iso_hom_pOpcycles_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq_fromOpcycles e hij rfl rfl hi]

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv) ≫
      (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case mpr
ι : 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
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ (∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i') → ∀ (i : ι'), QuasiIsoAt (truncGEMap φ e) i

Tactic:
· intro h i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi'
      simpa only [this i i' hi] using h i i' hi
    · rw [quasiIsoAt_iff_exactAt]
      all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
⊢ (K.shortComplexTruncLE e).X₃.ExactAt (e.f i)

Tactic:
exactAt_iff_isZero_homology

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))