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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
⊢ (mappingCone (𝟙 (I K)) ⊞ L).IsStrictlyGE n

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero ((mappingCone (𝟙 (I K)) ⊞ L).X i)
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 : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : (shiftFunctor C 1).obj ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
hg' : g = 0
⊢ f = 0

Tactic:
hg,

Goal state after:
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 : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : (shiftFunctor C 1).obj ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
hg' : g = 0
⊢ ((t.triangleLTGE n).obj X).mor₃ ≫ g = 0
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 : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
hg' : g = 0
⊢ f = 0

Tactic:
hg,

Goal state after:
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 : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
hg' : g = 0
⊢ g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁ = 0
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
n m : ℤ
hnm : n + 1 = m
⊢ i.f n ≫ (↑(cocycle₁' sq hsq)).v n m hnm = 0

Tactic:
have fac_left (k : ℤ) := (hsq k).fac_left

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
n m : ℤ
hnm : n + 1 = m
fac_left :
  ∀ (k : ℤ),
    (HomologicalComplex.eval C (ComplexShape.up ℤ) k).map i ≫ (hsq k).l =
      (HomologicalComplex.eval C (ComplexShape.up ℤ) k).map t
⊢ i.f n ≫ (↑(cocycle₁' sq hsq)).v n m hnm = 0
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
inst✝ : IsTriangulated C
a b : ℤ
h : a ≤ b
X : C
⊢ (t.triangleLTLTGELT a b h).obj X ∈ distinguishedTriangles

Tactic:
have := t.isIso_truncLT_map_truncLTι_app a b h X

Goal state after:
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
inst✝ : IsTriangulated C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ (t.triangleLTLTGELT a b h).obj X ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
hip✝ : QuasiIso i ∨ QuasiIso p
sq✝ : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq✝ (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i)
    (kernelIsKernel p)
this : ∀ (n : ℤ), Injective ((kernel p).X n)
d : ℤ
hd : X.IsStrictlyGE d
inst✝ : Fibration (ObjectProperty.homMk p)
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
⊢ (kernel p).IsStrictlyGE d

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
hip✝ : QuasiIso i ∨ QuasiIso p
sq✝ : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq✝ (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i)
    (kernelIsKernel p)
this : ∀ (n : ℤ), Injective ((kernel p).X n)
d : ℤ
hd : X.IsStrictlyGE d
inst✝ : Fibration (ObjectProperty.homMk p)
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
⊢ ∀ (i : ℤ), autoParam (i < d) isStrictlyGE_iff._auto_1 → IsZero ((kernel p).X i)
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g

Tactic:
have := coprod.inr ≫= sq.fac_left

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this : coprod.inr ≫ Q.i ≫ sq.lift = coprod.inr ≫ coprod.desc (f ≫ P.ι) h.h
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
⊢ P.i₀ ≫ sq.lift = f₀

Tactic:
have := coprod.inl ≫= sq.fac_left
          rwa [P.inl_i_assoc, coprod.inl_desc] at this

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 Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
⊢ P.i₁ ≫ sq.lift = f₁

Tactic:
have := coprod.inr ≫= sq.fac_left

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
this : coprod.inr ≫ P.i ≫ sq.lift = coprod.inr ≫ coprod.desc f₀ f₁
⊢ P.i₁ ≫ sq.lift = f₁
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case right
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ Function.Surjective fun g ↦ g.precomp f

Tactic:
· intro φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    have sq : CommSq φ f (terminal.from _) (terminal.from _) := { }
    exact ⟨mk sq.lift, by simp⟩

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
X Y : C
inst✝ : IsFibrant Y
f g : resolutionObj X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ RightHomotopyRel (homMk f).hom (homMk g).hom

Tactic:
rw [← RightHomotopyClass.mk_eq_mk_iff] at h ⊢

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : C
inst✝ : IsFibrant Y
f g : resolutionObj X ⟶ Y
h : RightHomotopyClass.mk (iResolutionObj X ≫ f) = RightHomotopyClass.mk (iResolutionObj X ≫ g)
⊢ RightHomotopyClass.mk (homMk f).hom = RightHomotopyClass.mk (homMk g).hom
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)

Tactic:
apply Constructor.isConnected

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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
⊢ (mid f n₀).IsStrictlyGE (n₀ + 1)

Tactic:
isStrictlyGE_iff

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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
⊢ ∀ (i : ℤ), autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1 → IsZero ((mid f n₀).X 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)
⊢ degreewiseEpiWithInjectiveKernel (π f n₀)

Tactic:
by
  intro i
  obtain ⟨q, hq⟩ : ∃ (q : ℕ), i ≤ n₀ + q := ⟨(i - n₀).natAbs, by lia⟩
  rw [← midπ_π_f f n₀ q]
  have := isIso_midπ_f f n₀ q i
  exact MorphismProperty.comp_mem _ _ _
    (epiWithInjectiveKernel_of_iso _)
    ((CofFibFactorizationQuasiIsoLE.sequence f n₀ q).obj.property.2 i)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝ : Φ.IsRightDerivabilityStructure
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
exact Functor.hasPointwiseRightDerivedFunctor_of_inverts _ h

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) = s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) = s.ι.app (CostructuredArrow.mk φ)
⊢ e.hom.app X₁ ≫
      (L ⋙ G).map w ≫
        G.map (Localization.isoOfHom L W w hw).inv ≫
          G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
comp_map,

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) = s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) = s.ι.app (CostructuredArrow.mk φ)
⊢ e.hom.app X₁ ≫
      G.map (L.map w) ≫
        G.map (Localization.isoOfHom L W w hw).inv ≫
          G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
⊢ T.IsLeftDerivabilityStructure

Tactic:
by
    let e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
      (leftUnitor _).symm ≪≫
        isoWhiskerRight L.functor.asEquivalence.counitIso.symm _ ≪≫
        associator _ _ _ ≪≫ isoWhiskerLeft _ (associator _ _ _).symm ≪≫
        isoWhiskerLeft _ (isoWhiskerRight iso.symm R.inv.functor) ≪≫
        isoWhiskerLeft _ (associator _ _ _) ≪≫
        isoWhiskerLeft _ (isoWhiskerLeft _ R.functor.asEquivalence.unitIso.symm) ≪≫
        (associator _ _ _).symm ≪≫ rightUnitor _
    have : W₁.RespectsIso := by rw [← L.inverseImage_eq]; infer_instance
    have : W₂.RespectsIso := by rw [← R.inverseImage_eq]; infer_instance
    exact isLeftDerivabilityStructure_of_equivalences e

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K L : Plus (InjectiveObject C)
f : K ⟶ L
hf : IsIso f
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((ι C).map ((InjectiveObject.ι C).mapHomotopyCategoryPlus.map f))

Tactic:
rw [HomotopyCategory.mem_quasiIso_iff]

Goal state after:
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K L : Plus (InjectiveObject C)
f : K ⟶ L
hf : IsIso f
⊢ ∀ (n : ℤ),
    IsIso
      ((homologyFunctor C (ComplexShape.up ℤ) n).map ((ι C).map ((InjectiveObject.ι C).mapHomotopyCategoryPlus.map f)))
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
⊢ L.IsStrictlyGE (-d)

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
⊢ ∀ (i : ℤ), autoParam (i < -d) isStrictlyGE_iff._auto_1 → IsZero (L.X i)
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
by
        have := C.d_comp_d i j k
        rw [NatTrans.ext_iff, funext_iff] at this
        exact this t

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ (G : HomologicalComplex C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ p ≫ f.f j = p ≫ g.f j

Tactic:
apply H.homEquiv.symm.injective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ (G : HomologicalComplex C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ H.homEquiv.symm (p ≫ f.f j) = H.homEquiv.symm (p ≫ g.f j)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi (P.π.f (n✝ + 1))

Tactic:
π_f_succ

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi 0
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : ¬c.π c c (c.next i₁, i₂) = j
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0

Tactic:
· rw [mapBifunctor.d₁_eq_zero' _ _ _ _ h₁ _ _ h₂]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ IsLimit (KernelFork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)) ⋯)

Tactic:
by
      refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (kernelIsKernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂))
      · exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
      · exact Fork.ext (Iso.refl _)

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
⊢ ∀ (r r' : ℤ) (pq : ℕ × ℕ),
    (∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq pq') →
      ∀ (n : ℤ),
        n = coreE₂HomologicalNat.deg pq + 1 →
          ∀ (hrr' : autoParam (r + 1 = r') HasSpectralSequence._auto_1)
            (hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3), IsZero ((Y.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
    apply isZero₂_of_isThirdQuadrant
    simp only [coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_deg, WithBotTop.coe_le_coe]
    by_contra!
    obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p - r by lia)
    obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + r - 1 by lia)
    exact hpq ⟨p', q'⟩ (by constructor <;> lia)

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : ¬(c r).Rel pq pq'
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0

Tactic:
dsimp only [pageD]
    rw [dif_neg hpq, zero_comp]

Goal state after:
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
rw [eventuallyConst_atTop]

Goal state after:
α : Type u_1
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m