mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ g.f = h.f

Tactic:
rw [← cancel_epi f]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ f ≫ g.f = f ≫ h.f
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ

Tactic:
rwa [isIdempotentComplete_iff_opposite]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom (δ i.castSucc ≫ σ j.succ)) k = (Hom.toOrderHom (σ j ≫ δ i)) k

Tactic:
dsimp [σ, δ]

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
j : ℕ
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((alternatingFaceMapComplex C).obj X)).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ ((alternatingFaceMapComplex D).obj (((SimplicialObject.whiskering C D).obj F).obj X)).d (j + 1) j

Tactic:
simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d,
        eqToHom_refl, id_comp, comp_id, AlternatingFaceMapComplex.objD, Functor.map_sum,
        Functor.map_zsmul]

Goal state after:
case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
j : ℕ
⊢ ∑ x, (-1) ^ ↑x • F.map (X.δ x) = ∑ i, (-1) ^ ↑i • (((SimplicialObject.whiskering C D).obj F).obj X).δ i
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
j : Fin (i + 1)
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑j.succ • X.δ j.succ) = 0

Tactic:
NormalizedMooreComplex.objX_add_one,

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
j : Fin (i + 1)
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ ((-1) ^ ↑j.succ • X.δ j.succ) = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.δ (i.castLT ⋯) ≫ X.δ j.succ = X.δ j ≫ X.δ i

Tactic:
by
  dsimp [δ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_δ'' H]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ)) x

Tactic:
simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    Function.comp_apply, Fin.predAboveOrderHom_coe]

Goal state after:
case h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
x✝ : ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex
h₁ : s.dim = t.dim
h₂ : (s.cast h₁).simplex = t.simplex
⊢ s = t

Tactic:
obtain ⟨_, _, rfl⟩ := s.mk_surjective

Goal state after:
X : SSet
t : X.S
w✝¹ : ℕ
w✝ : X _⦋w✝¹⦌
x✝ : ∃ (h : { dim := w✝¹, simplex := w✝ }.dim = t.dim), ({ dim := w✝¹, simplex := w✝ }.cast h).simplex = t.simplex
h₁ : { dim := w✝¹, simplex := w✝ }.dim = t.dim
h₂ : ({ dim := w✝¹, simplex := w✝ }.cast h₁).simplex = t.simplex
⊢ { dim := w✝¹, simplex := w✝ } = t
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
    intro
    rw [isIso_iff_bijective]
    constructor
    · rw [← mono_iff_injective]
      infer_instance
    · rw [← epi_iff_surjective]
      infer_instance

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
cases j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ (ComplexShape.down ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i n✝ : ℕ
⊢ (ComplexShape.down ℕ).Rel i (n✝ + 1) →
    𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i (n✝ + 1) = C.d i (n✝ + 1) ≫ 𝟙 (C.X (n✝ + 1))
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑i + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i ⋯ ≫ ed.s (↑k + 1) ≫ X.left.δ 1 ≫ X.left.σ₀Iter ↑i ⋯

Tactic:
dsimp% ed.s_comp_δ_assoc k.val 0,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑i + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i ⋯ ≫ X.left.δ 0 ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑i ⋯
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case pos
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : i₁ = 0
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂

Tactic:
subst h₁

Goal state after:
case pos
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₂ : Fin (⦋n + 1⦌.len + 1)
hi : 0 ≤ i₂
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) 0 ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
cases j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel i (n✝ + 1) →
    𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i (n✝ + 1) = C.d i (n✝ + 1) ≫ 𝟙 (C.X (n✝ + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i j =
      C.d i j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
by
        rcases j with (_ | _ | j) <;> rcases i with - | i <;> aesop

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ =
    0

Tactic:
rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (t.z (a + b) c • (shiftFunctorAdd C (a + b) c).app X).hom ≫
      (shiftFunctor C c).map (t.z a b • (shiftFunctorAdd C a b).app X).hom =
    eqToHom ⋯ ≫
      (t.z a (b + c) • (shiftFunctorAdd C a (b + c)).app X).hom ≫
        (t.z b c • (shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
simp only [Functor.map_comp, Category.assoc, CatCenter.smul_iso_hom_eq]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ ((shiftFunctorAdd C (a + b) c).app X).hom ≫
      (↑(t.z (a + b) c)).app ((shiftFunctor C c).obj ((shiftFunctor C (a + b)).obj X)) ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    eqToHom ⋯ ≫
      ((shiftFunctorAdd C a (b + c)).app X).hom ≫
        (↑(t.z a (b + c))).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
          ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom ≫
            (↑(t.z b c)).app ((shiftFunctor C c).obj ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)))
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
        (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ (c.prev j)) ≫
      (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₁ c (c.prev j) j

Tactic:
ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ (by rw [← ComplexShape.prev_π₁ c₂ c h₃, h]),

Goal state after:
case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
        (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c (c₁.prev i₁) i₂ (c.prev j) ⋯) ≫
      (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₁ c (c.prev j) j
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
          L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ (c.prev j) ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₂ c (c.prev j) j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ (by rw [← ComplexShape.prev_π₁ c₂ c h₃, h]),

Goal state after:
case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
          L₁.ιMapBifunctor L₂ F c (c₁.prev i₁) i₂ (c.prev j) ⋯ ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₂ c (c.prev j) j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]
    grind [up_Rel]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
i : ℤ
hi : i < n
⊢ HomologicalComplex.homology (Q.objPreimage X) i ≅ (homologyFunctor C i).obj X

Tactic:
exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)
i : ℤ
hi : n < i
⊢ HomologicalComplex.homology (Q.objPreimage X) i ≅ (homologyFunctor C i).obj X

Tactic:
exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ δ m n ((↑z).comp β ⋯) = ↑z

Tactic:
by simp [δ_comp z.1 β _ _ 0 _ hm rfl (by simp), hβ]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : trivialFibrations C p
⊢ HasLiftingProperty i p

Tactic:
mem_trivialFibrations_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : Fibration p ∧ WeakEquivalence p
⊢ HasLiftingProperty i p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

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
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
x✝¹ x✝ : CochainComplex.Plus C
f : x✝¹ ⟶ x✝
hf : (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) f
⊢ IsIso ((quotient C).map f)

Tactic:
by
      simpa [← isIso_iff_of_reflects_iso _ (HomotopyCategory.Plus.ι C),
        ← inverseImage_quotient_isomorphisms] using! hf

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ epiWithInjectiveKernel (f.f n) ↔ Injective (K.X n)

Tactic:
rw [epiWithInjectiveKernel_iff_of_isZero]

Goal state after:
case hY
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ IsZero (L.X n)
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd

Tactic:
simp [reassoc_of% σ₁.s_g, σ₂.f_r]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
⊢ f₁ = f₂

Tactic:
suffices ∀ (f : Y ⟶ (t.truncLT n).obj X) (_ : f ≫ (t.truncLTι n).app X = 0), f = 0 by
    rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
  intro f hf
  obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _
    (t.triangleLTGE_distinguished n X)) f hf
  have hg' := t.zero_of_isLE_of_isGE g (n - 1) (n + 1) (by lia) inferInstance
    (by dsimp; apply (t.isGE_shift _ n (-1) (n + 1) (by lia)))
  rw [hg, hg', zero_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ trivialFibrations C h.p

Tactic:
mem_trivialFibrations_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ Fibration h.p ∧ WeakEquivalence h.p
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let F := (localizerMorphism C).localizedFunctor Lfib L

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this✝ : Mono (homologyMap (π f n) n)
this : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (α f n)).mor₂ n, zero := ⋯ }.f
      ⋯)
⊢ homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom

Tactic:
simp [← cancel_mono (homologyMap (π f n) n),
        dsimp% IsLimit.conePointUniqueUpToIso_hom_comp h₁ h₂ .zero,
        ← homologyMap_comp, mappingCocone.lift_fst]

Goal state after: