mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
rw [d₂_eq _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]

Goal state after:
case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, c₂.next i₂, i₃) ≠ j'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
⊢ coboundaries K L n ≤
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapAddHom.comp Cocycle.equivHomShift.symm.toAddMonoidHom).ker

Tactic:
rintro ⟨x, _⟩ ⟨m, hm, β, rfl⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property✝ : δ m n β ∈ cocycle K L n
⊢ ⟨δ m n β, property✝⟩ ∈
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapAddHom.comp Cocycle.equivHomShift.symm.toAddMonoidHom).ker
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.trW.isColocal X
Y : C
f : X ⟶ Y
hY : P Y
⊢ f = 0

Tactic:
exact (hX _ (trW.mk P (contractible_distinguished₂ Y) (P.le_shift _ _ hY))).injective (by simp)

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
this : ∀ (a : ℕ), H a
⊢ Monotone t.le

Tactic:
intro n₀ n₁ h

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
⊢ t.le n₀ ≤ t.le n₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
n : ℤ
X : C
hX : t.le n X
⊢ t.le (n + ↑1) X

Tactic:
rw [← t.shift_le n 1 (n + (1 : ℕ)) rfl, ObjectProperty.prop_shift_iff]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
n : ℤ
X : C
hX : t.le n X
⊢ t.le 1 ((shiftFunctor C n).obj X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
this : ∀ (a : ℕ), H a
⊢ Antitone t.ge

Tactic:
intro n₀ n₁ h

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
⊢ t.ge n₁ ≤ t.ge n₀
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : t.ge n X✝
⊢ t.ge n Y✝

Tactic:
simp only [ge_iff_isGE] at h ⊢

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : t.IsGE X✝ n
⊢ t.IsGE Y✝ n
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)) → X.IsLE n

Tactic:
intro hX
    have : (Q.objPreimage X).IsLE n := by
      rw [CochainComplex.isLE_iff]
      intro i hi
      rw [HomologicalComplex.exactAt_iff_isZero_homology]
      apply (hX i hi).of_iso
      exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)
    exact ⟨(Q.objPreimage X).truncLE n, (Q.objObjPreimageIso X).symm ≪≫
      (asIso (Q.map ((Q.objPreimage X).ιTruncLE n))).symm, inferInstance⟩

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration P.i₀

Tactic:
rw [← P.inl_i]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝³ : HasBinaryCoproducts C
inst✝² : CategoryWithCofibrations C
inst✝¹ : P.IsGood
inst✝ : (cofibrations C).RespectsIso
⊢ Cofibration P.symm.i

Tactic:
by
    have hi : cofibrations C P.i := by rw [← cofibration_iff]; infer_instance
    rw [P.symm_i, cofibration_iff]
    refine ((cofibrations C).arrow_mk_iso_iff ?_).2 hi
    exact Arrow.isoMk (coprod.braiding A A) (Iso.refl _)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : Cylinder A
inst✝¹ : IsCofibrant A
P P' : Cylinder A
inst✝ : P'.IsGood
⊢ WeakEquivalence (P.trans P'.toPrecylinder).π

Tactic:
have : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫
        pushout.desc P.π P'.π (by simp)) := by
      simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]
      infer_instance
    dsimp
    apply weakEquivalence_of_precomp (P.i₀ ≫ pushout.inl _ _)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
a : A
X : C
⊢ G.map ((lift.shiftIso hΦ 0 a a ⋯).hom.app X) = G.map (((Φ a).isoWhiskerLeft (shiftFunctorZero D A)).hom.app X)

Tactic:
simp [lift.map_shiftIso_hom_app, Functor.commShiftIso_zero]

Goal state after:
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
n : ℤ
K : HomotopyCategory C (ComplexShape.up ℤ)
hK : plus C K
⊢ (plus C).shift n K

Tactic:
by
        obtain ⟨K : CochainComplex _ _, rfl⟩ := K.quotient_obj_surjective
        simp only [plus_quotient_obj_iff] at hK
        obtain ⟨q, _⟩ := hK
        rw [ObjectProperty.prop_shift_iff, shift_quotient_obj,
          plus_quotient_obj_iff]
        exact ⟨q - n, K.isStrictlyGE_shift q n (q - n) (by lia)⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
x✝ : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
hs : B.trW s
⊢ ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
rw [ObjectProperty.trW_iff'] at hs
    obtain ⟨W, a, b, hT, hW⟩ := hs
    obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac a hW hX
    obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX
    obtain ⟨g, hg, _⟩ := Pretriangulated.complete_distinguished_triangle_morphism _ _ hT hT'
      c (𝟙 _) (by cat_disch)
    refine ⟨U, e, g, hU, ?_, by cat_disch⟩
    rw [ObjectProperty.trW_iff']
    exact ⟨_, _, _, hT', h₁, h₂⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left✝ : Epi f
hf : Injective (kernel f)
this : Epi f'
⊢ kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯ ≫
      kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯ =
    𝟙 (kernel f')

Tactic:
by ext; simp

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
n : ℤ
⊢ biprod.inl.f n ≫ (p K L).f n = 0

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
n : ℤ
⊢ { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
          g := (p K L).f n, zero := ⋯ }.f ≫
      biprod.fst.f n =
    𝟙
      { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
          g := (p K L).f n, zero := ⋯ }.X₁

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

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

Goal state before:
pp: case refine_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
n : ℤ
⊢ biprod.inr.f n ≫
      { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
          g := (p K L).f n, zero := ⋯ }.g =
    𝟙
      { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
          g := (p K L).f n, zero := ⋯ }.X₃

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

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

Goal state before:
pp: case refine_4
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
n : ℤ
⊢ biprod.fst.f n ≫
        { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
            g := (p K L).f n, zero := ⋯ }.f +
      { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
            g := (p K L).f n, zero := ⋯ }.g ≫
        biprod.inr.f n =
    𝟙
      { X₁ := (mappingCone (𝟙 (I K))).X n, X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n, X₃ := L.X n, f := biprod.inl.f n,
          g := (p K L).f n, zero := ⋯ }.X₂

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ModelCategory C
X Y : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ ∃ g, LeftHomotopyRel (f ≫ g) (𝟙 X) ∧ LeftHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
by
  simp only [leftHomotopyRel_iff_rightHomotopyRel]
  apply RightHomotopyClass.whitehead

Goal state after:
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 : ℤ
⊢ Mono ((p f n).f n)

Tactic:
simp only [p, mkHomToSingle_f, mono_comp_iff_of_mono]

Goal state after:
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 : ℤ
⊢ Mono (Injective.ι (((cokernel f).truncGE n).X n))
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (homRel C).FactorsThroughLocalization (weakEquivalences (FibrantObject C))

Tactic:
by
  rintro X Y f g h
  obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_cylinder
  let L := (weakEquivalences (FibrantObject C)).Q
  rw [areEqualizedByLocalization_iff L]
  suffices L.map (homMk P.i₀) = L.map (homMk P.i₁) by
    simp only [show f = homMk P.i₀ ≫ homMk h.h by cat_disch,
      show g = homMk P.i₁ ≫ homMk h.h by cat_disch, Functor.map_comp, this]
  have := Localization.inverts L (weakEquivalences _) (homMk P.π) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)
  simp [← cancel_mono (L.map (homMk P.π)), ← L.map_comp]

Goal state after:
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
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
G : H ⥤ Hfib := (HoCat.localizerMorphismResolution C).localizedFunctor L Lfibπ
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
    CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lfibπ G

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
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
G : H ⥤ Hfib := (HoCat.localizerMorphismResolution C).localizedFunctor L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lfibπ G
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C₃
inst✝⁵ : Category.{v_4, u_4} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
inst✝³ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst✝² : R₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ᵥ w').GuitartExact
Y₂ : D₂
⊢ (w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂))).Initial

Tactic:
have := Functor.initial_of_natIso (structuredArrowDownwardsComp w w' (R₁.objPreimage Y₂)).symm

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} C₃
inst✝⁵ : Category.{v_4, u_4} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
inst✝³ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst✝² : R₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ᵥ w').GuitartExact
Y₂ : D₂
this :
  (w.structuredArrowDownwards (R₁.objPreimage Y₂) ⋙ w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂))).Initial
⊢ (w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂))).Initial
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr.succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
k : ℕ
h : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + k = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + ↑q₁
hk : q₁ + (k + 1) = q₂
⊢ IsIso (((functor f n₀).map (homOfLE ⋯ ≫ homOfLE ⋯).op).hom.h.f i)

Tactic:
op_comp,

Goal state after:
case inr.succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
k : ℕ
h : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + k = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + ↑q₁
hk : q₁ + (k + 1) = q₂
⊢ IsIso (((functor f n₀).map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op)).hom.h.f i)
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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q₁ : ℕ
hi : i ≤ n₀ + ↑q₁
hq : q₁ ≤ q₁ + 1
⊢ IsIso ((CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q₁).op.unop.hom.h.f i)

Tactic:
exact CofFibFactorizationQuasiIsoLE.isIso_fromNext_hom_h_f _ _ _ _ hi

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

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✝ : e.IsRelIff
i : ι
i' : ι'
hi' : e.f i = i'
⊢ (K.restriction e).X i = K.X i'

Tactic:
subst hi'

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.restriction e).X i = K.X (e.f i)