mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: case hR₂'
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Mono (((preadditiveCoyonedaObj G).op ⋙ preadditiveYoneda.obj ((preadditiveCoyonedaObj G).obj Y)).map cm.op.f)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (∐ fun X ↦ ∐ fun x ↦ projectiveSeparator C)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ ∀ (J : Type ?u.34) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape J (preadditiveCoyonedaObj (generator F))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ c ^ i * (1 - c⁻¹) ≤ ↑⌊c ^ i⌋₊

Tactic:
mul_comm

Goal state after:
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A

Tactic:
have h₂ : Functor.Final (inclusion (fromFinalModel (CostructuredArrow yoneda A))) :=
    Functor.final_of_comp_full_faithful' (factoring _) (inclusion _)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
have := essentiallySmallSelf (CostructuredArrow yoneda A)

Goal state after:
case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
this : EssentiallySmall.{max ?u.32 u, u, u} (CostructuredArrow yoneda A)
⊢ FinallySmall (CostructuredArrow yoneda A)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (b : B), IsConnected (CostructuredArrow L (R.obj b))
b : B
this : (costructuredArrowSndInclusion L R b).Final
⊢ IsConnected (CostructuredArrow L (R.obj b))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom iR.hom))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ AsSmall.equiv.functor.Faithful

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Faithful
⊢ Ind.yoneda.rightOp.Faithful

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝¹ : (F C).Faithful
this✝ : (G C).Faithful
this : (H C).Faithful
⊢ (F C ⋙ G C ⋙ H C).Faithful

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ AsSmall.equiv.functor.Full

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Full
⊢ Ind.yoneda.rightOp.Full

Tactic:
infer_instance

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

Goal state before:
pp: C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w✝¹ : SmallCategory I
w✝ : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map ϕ)
i' : Arrow.mk (coimageImageComparison f) ≅ Arrow.mk (coimageImageComparison ((Ind.lim I).map ϕ)) :=
  coimageImageComparisonFunctor.mapIso i
this : IsIso i'.hom
⊢ IsIso ((Ind.lim I).map (coimageImageComparison ϕ))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝¹ : (F C).Full
this✝ : (G C).Full
this : (G C ⋙ H C).Full
⊢ (F C ⋙ G C ⋙ H C).Full

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteLimits AsSmall.equiv.functor

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝¹ : PreservesFiniteLimits (F C)
this✝ : PreservesFiniteLimits (G C)
this : PreservesFiniteLimits (H C)
⊢ PreservesFiniteLimits (F C ⋙ G C ⋙ H C)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteColimits AsSmall.equiv.functor

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝¹ : PreservesFiniteColimits (F C)
this✝ : PreservesFiniteColimits (G C)
this : PreservesFiniteColimits (H C)
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Tactic:
intro

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYoneda.obj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Tactic:
intro

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYonedaObj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Abelian.Injective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
this : (preadditiveYonedaObj J).PreservesHomology
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ CochainComplex.IsStrictlyGE (HomologicalComplex.extend R.cocomplex ComplexShape.embeddingUpNat) 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
⊢ QuasiIso
    ((HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1).inv ≫
      HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
⊢ HomologicalComplex.IsSupported ((CochainComplex.singleFunctor C 0).obj X) (ComplexShape.embeddingUpIntLE 0)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt I.ι (n + 1)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono 0

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
x✝³ x✝² x✝¹ : C
f : x✝³ ⟶ x✝¹
g : x✝³ ⟶ x✝²
x✝ : Limits.HasPushout f g
hf : Mono f
⊢ Mono (Limits.pushout.inr f g)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
x✝³ x✝² x✝¹ : C
f : x✝³ ⟶ x✝¹
g : x✝² ⟶ x✝¹
x✝ : Limits.HasPullback f g
hf : Epi g
⊢ Epi (Limits.pullback.fst f g)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
inst✝ : Φ.IsIdempotent
X : C
⊢ IsIso (Φ.ι.app (Φ.r.obj X))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ ∀ (k : D), Mono ((F.whiskerLeft Φ.ι).app k)

Tactic:
intro

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
k✝ : D
⊢ Mono ((F.whiskerLeft Φ.ι).app k✝)
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
k✝ : D
⊢ Mono (Φ.ι.app (F.obj k✝))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Radical C
⊢ IsIso (Φ.obj.toColon Φ.obj)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ CochainComplex.IsStrictlyLE (HomologicalComplex.extend R.complex ComplexShape.embeddingDownNat) 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ QuasiIso
    (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat ≫
      (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1).hom)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ HomologicalComplex.IsSupported ((CochainComplex.singleFunctor C 0).obj X) (ComplexShape.embeddingUpIntGE 0)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Mono Φ.ι

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Epi Φ.π

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ Mono (Φ.ι.app X)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ Epi (Φ.π.app X)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Epi (pullback.snd Φ.π (Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ QuasiIso R.ι'

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Mono (Injective.ι Z)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
p : Over P
hpbar : pseudoApply f ⟦p⟧ = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
hp : ⟦p⟧ = pbar
⊢ ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧

Tactic:
exact hpbar

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
⊢ QuasiIso R.π'

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsMultiplicative

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderRetracts

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderBaseChange

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderCobaseChange

Tactic:
infer_instance

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

Goal state before:
pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯))

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt

Tactic:
· exact (IsLimit.postcomposeInvEquiv _ _).symm (kernelIsKernel f.hom)

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso
    ((InjectiveResolution.self X).toRightDerivedZero' F ≫
      (CochainComplex.isoHomologyπ₀
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex)).hom ≫
        ((InjectiveResolution.self X).isoRightDerivedObj F 0).inv)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteLimits F
X : C
⊢ IsIso
    ((injectiveResolution X).toRightDerivedZero' F ≫
      (CochainComplex.isoHomologyπ₀
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ Function.LeftInverse (fun f ↦ ⇑(ConcreteCategory.hom f)) fun f ↦ ↾f

Tactic:
intro

Goal state after:
X : Type u
x✝ : Function.End X
⊢ (fun f ↦ ⇑(ConcreteCategory.hom f)) ((fun f ↦ ↾f) x✝) = x✝
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ Function.RightInverse (fun f ↦ ⇑(ConcreteCategory.hom f)) fun f ↦ ↾f

Tactic:
intro

Goal state after:
X : Type u
x✝ : End X
⊢ (fun f ↦ ↾f) ((fun f ↦ ⇑(ConcreteCategory.hom f)) x✝) = x✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
J : Type u_3
inst✝¹ : Category.{v_2, u_3} J
K : J ⥤ Action V G
inst✝ : HasLimit (K ⋙ forget V G)
this : ∀ (k : SingleObj G), HasLimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k)
⊢ PreservesLimit K ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
J : Type u_3
inst✝¹ : Category.{v_2, u_3} J
K : J ⥤ Action V G
inst✝ : HasColimit (K ⋙ forget V G)
this : ∀ (k : SingleObj G), HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k)
⊢ PreservesColimit K ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : HasFiniteLimits V
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : HasFiniteColimits V
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesColimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
H : D ⥤ E
inst✝² : HasColimitsOfSize.{v, u, v₁, u₁} C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
x✝¹ : PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
J : Type u
x✝ : Category.{v, u} J
⊢ PreservesColimitsOfShape J (F ⋙ H)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : RightRigidCategory V
⊢ RightRigidCategory (SingleObj H ⥤ V)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : LeftRigidCategory V
⊢ LeftRigidCategory (SingleObj H ⥤ V)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : RigidCategory V
⊢ RigidCategory (SingleObj H ⥤ V)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
h : F.FullyFaithful
this✝ : F.Full
this : F.Faithful
⊢ IsIso t.adj₁.unit

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
h : H.FullyFaithful
this✝ : H.Full
this : H.Faithful
⊢ IsIso t.adj₂.counit

Tactic:
infer_instance

Goal state after: