mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover f trivial
⊢ QuasiCompactCover (cover f trivial).toPreZeroHypercover

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsOpenImmersion f
⊢ P f

Tactic:
apply IsZariskiLocalAtSource.of_isOpenImmersion

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.toPreZeroHypercover

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
𝒰' : (precoverage P).ZeroHypercover (V.affineCover.X i) :=
  Precoverage.ZeroHypercover.pullback₂ (V.affineCover.f i) (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover)
⊢ QuasiCompactCover
    (PreZeroHypercover.pullback₂ (V.affineCover.f i) (PreZeroHypercover.pullback₂ f 𝒱.cover.toPreZeroHypercover))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i j : V.affineOneHypercover.I₀
k : V.affineOneHypercover.I₁ i j
⊢ QuasiCompactCover
    (PreZeroHypercover.pullback₂ (V.affineOneHypercover.p₁ k ≫ V.affineCover.f i)
      (PreZeroHypercover.pullback₂ f 𝒱.cover.toPreZeroHypercover))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
⊢ IsAffine (∐ 𝒰.X)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this✝ : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
this : Surjective (Sigma.desc 𝒰.f)
⊢ Surjective ((∐ 𝒰.X).isoSpec.inv ≫ Sigma.desc 𝒰.f)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ restriction data G₀ (F.map (p₁ ≫ a)) =
    presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map p₂ ≫ Sieve.ofArrows.h hb)

Tactic:
restriction_eq_of_fac data G₀ (F.map (p₁ ≫ a))
            (F.map p₂ ≫ Sieve.ofArrows.h hb) (by rw [assoc, hb', fac, map_comp])

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map p₂ ≫ Sieve.ofArrows.h hb) =
    presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map p₂ ≫ Sieve.ofArrows.h hb)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
⊢ ValuativeCriterion.Existence (toSpecZero 𝒜)

Tactic:
rintro ⟨O, K, i₁, i₂, w⟩
  obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
  choose d hd hxd using hx'
  have : i₁ (IsLocalRing.closedPoint K) ∈ (⊤ : (Proj 𝒜).Opens) := trivial
  rw [← Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx),
    TopologicalSpace.Opens.mem_iSup] at this
  obtain ⟨i, hi⟩ := this
  have : Set.range i₁ ⊆ (Proj.awayι 𝒜 _ (hxd i i.2) (hd i i.2).bot_lt).opensRange := by
    rw [Proj.opensRange_awayι]
    rintro _ ⟨x, rfl⟩
    obtain rfl := Subsingleton.elim x (IsLocalRing.closedPoint K)
    exact hi
  let φ : Spec (.of <| K) ⟶ _ := IsOpenImmersion.lift _ _ this
  have H : Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
      CommRingCat.ofHom (fromZeroRingHom 𝒜 _) ≫ Spec.preimage φ := by
    apply Spec.map_injective
    simp only [Spec.map_comp, Spec.map_preimage, ← w.w]
    rw [← Proj.awayι_toSpecZero _ _ (hxd i i.2), IsOpenImmersion.lift_fac_assoc]
    exact Nat.zero_lt_of_ne_zero (hd i i.2)
  obtain ⟨i₀, φ', hφ, hφ'⟩ :=
    valuativeCriterion_existence_aux 𝒜 (Spec.preimage i₂).hom x (↑) (by simpa using hx) i
      (O := O) (K := K) (Spec.preimage φ).hom congr(($H).hom)
      (fun i ↦ d _ i.2) (fun i ↦ (hd _ i.2).bot_lt) (fun i ↦ hxd _ i.2)
  let e : O ≃+* (algebraMap O K).range :=
    (AlgEquiv.ofInjective (Algebra.ofId O K) (IsFractionRing.injective _ _)).toRingEquiv
  let φ'' := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (RingHom.rangeRestrict _))
  have hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 (hxd _ i.2) (mul_comm _ _)) := by
    ext x
    exact congr_arg Subtype.val (e.apply_symm_apply _)
  refine ⟨⟨Spec.map (CommRingCat.ofHom φ'') ≫ Proj.awayι 𝒜 _ (hxd _ i₀.2) (hd _ _).bot_lt, ?_, ?_⟩⟩
  · rw [← Spec.map_comp_assoc]
    convert! IsOpenImmersion.lift_fac _ _ this using 1
    change _ = φ ≫ _
    rw [← Spec.map_preimage φ, ← CommRingCat.ofHom_hom (Spec.preimage φ), ← hφ,
      ← CommRingCat.ofHom_comp]
    simp [hφ'', SpecMap_awayMap_awayι, add_comm]
  · simp only [Category.assoc, Proj.awayι_toSpecZero, ← Spec.map_comp]
    conv_rhs => rw [← Spec.map_preimage i₂]
    congr 1
    ext x
    apply IsFractionRing.injective O K
    refine (DFunLike.congr_fun hφ'' (fromZeroRingHom 𝒜 _ _)).trans ?_
    simp only [RingHom.coe_comp, Function.comp_apply]
    rw [awayMap_fromZeroRingHom, ← awayMap_fromZeroRingHom 𝒜 (hxd i₀ i₀.2) rfl,
      ← RingHom.comp_apply, hφ]
    exact congr($(H.symm) x)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ WeaklyEtale f

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type u'
inst✝² : Category.{v', u'} J✝
inst✝¹ : HasFilteredColimitsOfSize.{v', u', v, u} C
inst✝ : AB5OfSize.{v', u', v, u} C
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
⊢ (monomorphisms C).IsStableUnderColimitsOfShape J

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
this : IsIso (f z)
⊢ Epi (f z)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case e
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
⊢ ⦃X : C⦄ → (CategoryTheory.yoneda.obj Y).obj (op X) ≃ (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X)

Tactic:
intro

Goal state after:
case e
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
X✝ : C
⊢ (CategoryTheory.yoneda.obj Y).obj (op X✝) ≃ (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X✝)
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ¬⟨b, hb'⟩ ⋖ m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
not_covBy_iff (by exact hb)

Goal state after:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ∃ c, ⟨b, hb'⟩ < c ∧ c < m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Preorder J
inst✝ : OrderBot J
x✝ : J ⥤ C
⊢ HasLimit x✝

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Preorder J
inst✝ : OrderTop J
x✝ : J ⥤ C
⊢ HasColimit x✝

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ HasColimitsOfShape (↑(Set.Iio j)) (Arrow C)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ HasColimitsOfShape (↑(Set.Iio j)) (K ⥤ C)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
G₁ : C ⥤ D
G₂ : D ⥤ E
inst✝¹ : PreservesWellOrderContinuousOfShape J G₁
inst✝ : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
this✝ : PreservesColimitsOfShape (↑(Set.Iio j)) G₁
this : PreservesColimitsOfShape (↑(Set.Iio j)) G₂
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) (G₁ ⋙ G₂)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
inst✝¹ : HasIterationOfShape J C
K : Type u_1
inst✝ : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) ((evaluation K C).obj X)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.leftFunc

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.rightFunc

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg.succ
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
this : OrderTop α
⊢ HasColimitsOfShape α C

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ (monomorphisms C).IsStableUnderTransfiniteComposition

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u'
inst✝⁷ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁶ : LinearOrder J
inst✝⁵ : SuccOrder J
inst✝⁴ : OrderBot J
inst✝³ : WellFoundedLT J
inst✝² : W.IsMultiplicative
inst✝¹ : W.RespectsIso
inst✝ : IsStableUnderFilteredColimits.{w, w, v, u} W
x✝⁴ : Type w
x✝³ : LinearOrder x✝⁴
x✝² : SuccOrder x✝⁴
x✝¹ : OrderBot x✝⁴
x✝ : WellFoundedLT x✝⁴
⊢ W.IsStableUnderColimitsOfShape x✝⁴

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape (Shrink.{w', w} J)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
φ : FunctorObjIndex f πX →
  (i : Shrink.{t, w} I) × Shrink.{t, v} ((A ((equivShrink I).symm i) ⟶ X) × (B ((equivShrink I).symm i) ⟶ S)) :=
  fun x ↦
    ⟨(equivShrink I) x.i,
      (equivShrink
          ((A ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ X) × (B ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b)⟩
i₁ : I
t₁ : A i₁ ⟶ X
b₁ : B i₁ ⟶ S
w✝¹ : t₁ ≫ πX = f i₁ ≫ b₁
t₂ : A i₁ ⟶ X
b₂ : B i₁ ⟶ S
w✝ : t₂ ≫ πX = f i₁ ≫ b₂
h : φ { i := i₁, t := t₁, b := b₁, w := w✝¹ } = φ { i := i₁, t := t₂, b := b₂, w := w✝ }
⊢ { i := i₁, t := t₁, b := b₁, w := w✝¹ } = { i := i₁, t := t₂, b := b₂, w := w✝ }

Tactic:
simpa [cancel_epi, φ] using h

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
⊢ Small.{t, max v w} (FunctorObjIndex f πX)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
⊢ ∀ (iter₁ iter₂ : Φ.Iteration (Order.succ j)), iter₁.F = iter₂.F

Tactic:
| succ j hj₁ hj₂ =>

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ IsSmall.{w, v, u} W → ∃ ι A B f, W = ofHoms f

Tactic:
intro

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
⊢ ∃ ι A B f, W = ofHoms f
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
w✝³ : Type w
w✝² w✝¹ : w✝³ → C
w✝ : (i : w✝³) → w✝² i ⟶ w✝¹ i
⊢ IsSmall.{w, v, u} (ofHoms w✝)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α✝ : Type t
inst✝¹ : Small.{w, t} α✝
W : α✝ → MorphismProperty C
inst✝ : ∀ (i : α✝), IsSmall.{w, v, u} (W i)
α : α✝ → Type w
A B : (i : α✝) → α i → C
f : (i : α✝) → (i_1 : α i) → A i i_1 ⟶ B i i_1
hf : ∀ (i : α✝), W i = ofHoms (f i)
⊢ IsSmall.{w, v, u} (ofHoms fun j ↦ f j.fst j.snd)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
f✝ : F.obj ⊥ ⟶ X
g✝ : ((Functor.const J).obj c.pt).obj ⊥ ⟶ Y
sq : CommSq f✝ (c.ι.app ⊥) p g✝
j : J
hj : ¬IsMax j
x✝¹ : F.obj j ⟶ X
x✝ : CommSq x✝¹ (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
this : HasLiftingProperty (F.map (homOfLE ⋯)) p
⊢ x✝.HasLift

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: case right
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ IsIso (𝟙 (F.obj f).right)

Tactic:
infer_instance

Goal state after: