mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := ⋯
this✝¹ : IsIso φ.hom₁
this✝ : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ IsIso φ.hom₂

Tactic:
infer_instance

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

Goal state before:
pp: case h₃
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := ⋯
this✝¹ : IsIso φ.hom₁
this✝ : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ IsIso φ.hom₃

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
⊢ T₁ ≅ T₂

Tactic:
have h := exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk e₁ e₂ comm.symm)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
⊢ T₁ ≅ T₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
⊢ (mappingConeHomOfDegreewiseSplitIso S σ).inv ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ =
    -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g

Tactic:
by
  ext n
  dsimp [mappingConeHomOfDegreewiseSplitXIso]
  simp only [Int.reduceNeg, id_comp, sub_comp, assoc, mappingCone.inl_v_triangle_mor₃_f,
    shiftFunctor_obj_X, shiftFunctorObjXIso, XIsoOfEq_rfl, Iso.refl_inv, comp_neg, comp_id,
    mappingCone.inr_f_triangle_mor₃_f, comp_zero, sub_zero]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ Mono (K.homologyι i)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ Epi (K.homologyπ j)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ Epi (S.g.f i)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ Mono (S.f.f i)

Tactic:
infer_instance

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)

Tactic:
refine (W.multiplicativeClosure_le_iff _).2 fun X Y f hf ↦ ?_
    simpa using! W.paths.map_mem_strictMap (pathComposition C) f.toPath (by simpa)

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Epi S.g
⊢ Epi (opcyclesMap S.g i)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Mono S.f
⊢ Mono (cyclesMap S.f j)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
G : V ⥤q C
⊢ Paths.of V ⋙q (Cat.freeMap G ⋙ pathComposition C).toPrefunctor = G

Tactic:
← Functor.toPrefunctor_comp,

Goal state after:
V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
G : V ⥤q C
⊢ Paths.of V ⋙q ((Cat.freeMap G).toPrefunctor ⋙q (pathComposition C).toPrefunctor) = G
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
this : Localization.Construction.lift W.Q ⋯ = 𝟭 W.Localization
⊢ (𝟭 W.Localization).IsEquivalence

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
⊢ P f → ⊤ f

Tactic:
intro

Goal state after:
case mp
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : P f
⊢ ⊤ f
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case mpr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
⊢ ⊤ f → P f

Tactic:
intro

Goal state after:
case mpr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
⊢ P f
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E).Full

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E).Faithful

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L✝ : C ⥤ D
W✝ : MorphismProperty C
inst✝¹ : L✝.IsLocalization W✝
L : Cᵒᵖ ⥤ Dᵒᵖ
W : MorphismProperty Cᵒᵖ
inst✝ : L.IsLocalization W
this✝ : CatCommSq (opOpEquivalence C).functor L.op L.unop (opOpEquivalence D).functor
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
hf : W.unop x✝
this : IsIso (L.map x✝.op)
⊢ IsIso (L.map x✝.op).unop

Tactic:
infer_instance

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F : W.Localization ⥤ D
⊢ (WhiskeringLeftEquivalence.functor W D).map ((WhiskeringLeftEquivalence.unitIso W D).hom.app F) ≫
      (WhiskeringLeftEquivalence.counitIso W D).hom.app ((WhiskeringLeftEquivalence.functor W D).obj F) =
    𝟙 ((WhiskeringLeftEquivalence.functor W D).obj F)

Tactic:
ext
    simp only [WhiskeringLeftEquivalence.unitIso_hom, eqToHom_app, eqToHom_refl,
      WhiskeringLeftEquivalence.counitIso_hom, eqToHom_map, eqToHom_trans]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ P.inverseImage (uniq W.Q L W).functor (Construction.wInv f hf)

Tactic:
refine (P.arrow_mk_iso_iff (Arrow.isoMk (e.app _) (e.app _) ?_)).2 (h₂ f hf)
        dsimp
        rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
⊢ Φ.functor.inv.IsEquivalence

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
⊢ IsIso (L.map φ'.s ≫ L.map α.s)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
⊢ IsIso (L.map β.s ≫ L.map γ.s)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ G.Additive → (L ⋙ G).Additive

Tactic:
intro

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
a✝ : G.Additive
⊢ (L ⋙ G).Additive
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
a✝ : G.Additive
⊢ (L ⋙ G).Additive

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ Finite PUnit.{1}

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isMin
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
hb : IsMin ⊥
hb₀ : Small.{w, w'} ↑(Set.Iio ⊥)
⊢ ObjectProperty.Small.{w, v, u} P

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case succ
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : ¬IsMax b
hb' : ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b)
hb₀ : Small.{w, w'} ↑(Set.Iio (Order.succ b))
this : Small.{w, w'} ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u}
    (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P ⊔
      ⨆ a, (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P).strictLimitsOfShape (J a))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isSuccLimit
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b, ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b_1)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b_1)
hb₀ : Small.{w, w'} ↑(Set.Iio b)
this :
  ∀ (c : ↑(Set.Iio b)), ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑c) P)
⊢ ObjectProperty.Small.{w, v, u} (⨆ x, transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑x) P)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁵ : (a : α) → Category.{v', u'} (J a)
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
this : ∀ (a : α), Small.{w, u'} (J a)ᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
this : ∀ (a : α), (P.strictLimitsClosureIter J κ.ord).isoClosure.IsClosedUnderLimitsOfShape (J a)
⊢ P.limitsClosure J ≤ (P.strictLimitsClosureIter J κ.ord).isoClosure

Tactic:
refine limitsClosure_le
      ((P.le_strictLimitsClosureIter J κ.ord).trans (le_isoClosure _))

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁶ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝⁵ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (Q.strictLimitsClosureIter J κ.ord).isoClosure

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
⊢ P ≤ P.shiftClosure A

Tactic:
by
  intro X hX
  exact ⟨X, 0, (shiftFunctorZero C A).symm.app X, hX⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
h : P.shiftClosure A = P
⊢ (P.shiftClosure A).IsStableUnderShift A

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
by
  have := IsClosedUnderBinaryCoproducts.closedUnderIsomorphisms P
  have := hasFiniteCoproducts_of_has_binary_and_initial (C := P.FullSubcategory)
  have := PreservesFiniteCoproducts.of_preserves_binary_and_initial P.ι
  exact ⟨fun J _ ↦ P.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι _⟩

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

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ (Q W).map s ≫ Qinv s hs = 𝟙 ((Q W).obj X)

Tactic:
rw [Q_map_comp_Qinv]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ homMk { Y' := Y, f := s, s := s, hs := hs } = 𝟙 ((Q W).obj X)
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ X₂ : C
this : HasBinaryBiproduct (F.obj X₁) (F.obj X₂)
Z : A
f : Z ⟶ F.obj (X₁ ⊞ X₂)
hf : f ≫ F.biprodComparison X₁ X₂ = 0
S : ShortComplex A := { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := biprod.inl, g := biprod.snd, zero := ⋯ }.map F
⊢ Mono (F.map biprod.inl)

Tactic:
infer_instance

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

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
L : C ⥤ D
inst✝ : L.IsLocalization W
⊢ IsIso (L.map z₂.s ≫ L.map z₃.s)

Tactic:
infer_instance

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

Goal state before:
pp: case mpr.left
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
a✝ : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n✝ : ℤ
⊢ Epi ((F.shift n✝).map f)

Tactic:
infer_instance

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

Goal state before:
pp: case mpr.right
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
a✝ : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n✝ : ℤ
⊢ Mono ((F.shift (n✝ + 1)).map f)

Tactic:
infer_instance

Goal state after: