mathlib-initiative/mathlib-tactics huggingface dataset:
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 i : ℤ
hi : (ComplexShape.up ℤ).Rel i n
⊢ ((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n) = 0

Tactic:
by
    simp only [ComplexShape.up_Rel] at hi
    exact (isZero_of_isStrictlyGE _ n _).eq_of_src _ _

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

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 C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasRightResolutions
X₂ : C₂
ρ : B.RightResolution (R.functor.obj X₂) := Classical.arbitrary (B.RightResolution (R.functor.obj X₂))
⊢ Nonempty (T.RightResolution X₂)

Tactic:
obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁

Goal state after:
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 C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasRightResolutions
X₂ : C₂
ρ : B.RightResolution (R.functor.obj X₂) := Classical.arbitrary (B.RightResolution (R.functor.obj X₂))
X₁ : C₁
e : L.functor.obj X₁ ≅ ρ.X₁
⊢ Nonempty (T.RightResolution X₂)
Module: Mathlib.CategoryTheory.Localization.Resolution

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 C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
⊢ Nonempty (T.LeftResolution X₂)

Tactic:
obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁

Goal state after:
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 C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
X₁ : C₁
e : L.functor.obj X₁ ≅ ρ.X₁
⊢ Nonempty (T.LeftResolution X₂)
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
inst✝¹ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝ : w.GuitartExact
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
⊢ ∀ (g : B.op.obj X₃ ⟶ R.op.obj X₂), IsConnected (w.op.StructuredArrowRightwards g)

Tactic:
g

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
inst✝¹ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝ : w.GuitartExact
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
g : B.op.obj X₃ ⟶ R.op.obj X₂
⊢ IsConnected (w.op.StructuredArrowRightwards g)
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ IsConnected ((localizerMorphism C).RightResolution X)

Tactic:
let R₀ : (localizerMorphism C).RightResolution X :=
    { X₁ := mk (HoCat.resolutionObj X)
      w := HoCat.iResolutionObj X
      hw := by simpa using mem_weakEquivalences (HoCat.iResolutionObj X) }

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).RightResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.iResolutionObj X, hw := ⋯ }
⊢ IsConnected ((localizerMorphism C).RightResolution X)
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
⊢ ∀ (g : R.obj Y₀ ⟶ B.obj X), IsConnected (CostructuredArrowDownwards e.hom g)

Tactic:
g

Goal state after:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
⊢ IsConnected (CostructuredArrowDownwards e.hom g)
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X : C⦄ ⦃Y₀ : C₀⦄ (f₀ f₁ : X ⟶ L.obj Y₀),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.p₀ = T.map P.p₁ ∧ Nonempty ((P.map L).RightHomotopy f₀ f₁)
e' : T.op ⋙ R.op ≅ L.op ⋙ B.op := NatIso.op e.symm
X₀ : C₀ᵒᵖ
Y : Cᵒᵖ
f₀ f₁ : L.op.obj X₀ ⟶ Y
h✝ : B.op.map f₀ = B.op.map f₁
P : PrepathObject (unop X₀)
hP : T.map P.p₀ = T.map P.p₁
h : (P.map L).RightHomotopy f₀.unop f₁.unop
⊢ ∃ P, T.op.map P.i₀ = T.op.map P.i₁ ∧ Nonempty ((P.map L.op).LeftHomotopy f₀ f₁)

Tactic:
exact ⟨P.op, Quiver.Hom.unop_inj hP, ⟨h.op⟩⟩

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_2} D
inst✝² : Category.{v_5, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
this : RF.IsLeftKanExtension α
⊢ F.HasRightDerivedFunctor W

Tactic:
simpa only [hasRightDerivedFunctor_iff F L W] using HasLeftKanExtension.mk RF α

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
D₂ : Type u₄
inst✝³ : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝² : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst✝ : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (Φ.functor ⋙ F) h W₁.Q
⊢ IsIso (α.app (Φ.functor.obj X₁))

Tactic:
let eG := Localization.Lifting.iso W₁.Q W₁ (Φ.functor ⋙ F) G

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝³ : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝² : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst✝ : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (Φ.functor ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor ⋙ F := Localization.Lifting.iso W₁.Q W₁ (Φ.functor ⋙ F) G
⊢ IsIso (α.app (Φ.functor.obj X₁))
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

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₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← guitartExact_op_iff, ← guitartExact_op_iff w,
    ← vComp_iff_of_equivalences _ _ _ w'', this]

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₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
⊢ (w.op ≫ᵥ w''.hom).GuitartExact ↔ (w.op ≫ᵥ w''.hom).GuitartExact
Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ IsIso ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f)

Tactic:
refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f ≫ g) =
    Qh.map (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K))

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ Qh.map (g ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f) =
    Qh.map (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L))
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₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ ∃ P,
    (L C).functor.map P.p₀ = (L C).functor.map P.p₁ ∧
      Nonempty
        ((P.map (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy (ObjectProperty.homMk f₀)
          (ObjectProperty.homMk f₁))

Tactic:
refine ⟨Plus.prepathObject _, ?_, ⟨?_⟩⟩

Goal state after:
case refine_1
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₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₀ =
    (L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₁

case refine_2
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₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ ((Plus.prepathObject { obj := K₂, property := ⋯ }).map
        (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy
    (ObjectProperty.homMk f₀) (ObjectProperty.homMk f₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus

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✝⁵ : Abelian C
inst✝⁴ : Abelian D
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : EnoughInjectives C
⊢ F.rightDerivedFunctorPlus.IsRightDerivedFunctor F.rightDerivedFunctorPlusUnit (HomotopyCategory.Plus.quasiIso C)

Tactic:
dsimp only [rightDerivedFunctorPlus, rightDerivedFunctorPlusUnit]
  infer_instance

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
grind +splitIndPred

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
grind +splitIndPred

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsZero (K.stupidTrunc e) ↔ K.IsStrictlySupportedOutside e

Tactic:
by
  constructor
  · exact fun h ↦ ⟨fun i ↦
      ((eval _ _ (e.f i)).map_isZero h).of_iso (K.stupidTruncXIso e rfl).symm⟩
  · intro h
    rw [isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside _ e]
    constructor
    · infer_instance
    · exact ⟨fun i ↦ (h.isZero i).of_iso (K.stupidTruncXIso e rfl)⟩

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 : K ⟶ L
⊢ ∀ (g : K ⟶ L),
    (∀ (G : HomologicalComplex C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g) →
      f = g

Tactic:
g

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
⊢ (∀ (G : HomologicalComplex C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g) → f = g
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain ((singleFunctor C p).obj X) K n
⊢ (fun f ↦ fromSingleMk f h) ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α) =
    α

Tactic:
ext p' q' hpq'
    by_cases hp : p' = p
    · aesop
    · exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hp).eq_of_src _ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
have hα := ((n + 1).negOnePow • α).δ_eq_zero (n + 1)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : δ n (n + 1) ↑((n + 1).negOnePow • α) = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

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
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ 𝟙 (F.obj ((toKaroubi C).obj X)) ≫
      τ.app X ≫ G.map (𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }) =
    τ.app X

Tactic:
Category.id_comp

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
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ τ.app X ≫ G.map (𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }) = τ.app X
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ {
      X₁ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1 + 1)).X₃,
      X₂ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1)).X₃,
      X₃ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) 0).X₃,
      f :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1)).g,
      g :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) 0).g,
      zero := ⋯ }.Exact

Tactic:
| =>

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ {
      X₁ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1 + 1)).X₃,
      X₂ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1)).X₃,
      X₃ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) 0).X₃,
      f :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1)).g,
      g :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) 0).g,
      zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ n : ℕ
⊢ {
      X₁ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1 + 1)).X₃,
      X₂ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1)).X₃,
      X₃ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).X₃,
      f :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1)).g,
      g :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).g,
      zero := ⋯ }.Exact

Tactic:
| =>

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ n : ℕ
⊢ {
      X₁ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1 + 1)).X₃,
      X₂ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1)).X₃,
      X₃ :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).X₃,
      f :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1)).g,
      g :=
        (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
            (d (d (Projective.π Z))) ⋯ (fun S ↦ ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).g,
      zero := ⋯ }.Exact