mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (Quotient.mk'' y ^ n).val = val (Quotient.mk'' y) ^ n

Tactic:
rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal) =
    (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal)

Tactic:
← Ideal.IsPrime.pow_mem_iff_mem (α := A⁰_ f) inferInstance m hm

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ^ m ∈ q.asIdeal) =
    (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal)
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
⊢ IsIntegral O x ↔ v x ≤ 1

Tactic:
have : Nontrivial O := hv.nontrivial_iff.mpr inferInstance

Goal state after:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
⊢ IsIntegral O x ↔ v x ≤ 1
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
M : Y.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
α : X.presheaf ⟶ (Hom.opensFunctor f).op ⋙ Y.presheaf := { app := fun U ↦ (Hom.appIso f (unop U)).inv, naturality := ⋯ }
hα : IsIso α
φ : X.ringCatSheaf ⟶
  ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
        (Opens.grothendieckTopology ↥Y)).obj
    Y.ringCatSheaf :=
  { hom := Functor.whiskerRight α (forget₂ CommRingCat RingCat) }
this : IsIso φ
⊢ SheafOfModules.IsQuasicoherent ((restrictFunctor f).obj M)

Tactic:
exact SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint.{u}
    f.opensFunctor φ (Scheme.Modules.restrictUnitIso _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
⊢ basicOpen f ⊓ V ≤ ⨆ i, basicOpen (f * g i)

Tactic:
hg,

Goal state after:
case h.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
⊢ basicOpen f ⊓ ⨆ i, basicOpen (g i) ≤ ⨆ i, basicOpen (f * g i)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case h
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
rwa [Cover.toPresieveOver_le_arrows_iff] at hT

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ IsIso g

Tactic:
suffices h : Function.Bijective (g.appTop) by
    refine (HasAffineProperty.iff_of_isAffine (P := MorphismProperty.isomorphisms Scheme)).mpr ?_
    exact ⟨hZ, (ConcreteCategory.isIso_iff_bijective _).mpr h⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ Function.Bijective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp.refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this✝ : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.I₀
fi : (𝒰.X i).asOverProp S ⋯ ⟶ X := Hom.asOverProp (𝒰.f i) S
this :
  Presieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R.arrows
    ((MorphismProperty.Over.forget Q ⊤ S).map fi)
⊢ R.arrows (Hom.asOverProp (𝒰.f i) S)

Tactic:
Sieve.mem_functorPushforward_iff_of_full_of_faithful

Goal state after:
case mp.refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this✝ : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.I₀
fi : (𝒰.X i).asOverProp S ⋯ ⟶ X := Hom.asOverProp (𝒰.f i) S
this : R.arrows fi
⊢ R.arrows (Hom.asOverProp (𝒰.f i) S)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case h
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp p ≤ R.arrows
Y : Over S
i : 𝒰.I₀
⊢ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows (Hom.asOver (𝒰.f i) S)

Tactic:
exact ⟨(𝒰.X i).asOverProp S (p i), (𝒰.f i).asOverProp S, 𝟙 _, le _ _ ⟨i⟩, rfl⟩

Goal state after:
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
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ LocallyOfFiniteType ((basicOpen 𝒜 ↑i).ι ≫ toSpecZero 𝒜)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType)
    (Proj.basicOpenIsoSpec 𝒜 (i : A) (hxd _ i.2) (hd _ i.2).bot_lt).inv, ← Category.assoc,
    ← Proj.awayι, Proj.awayι_toSpecZero, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)))).FiniteType
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows) →
    R ∈ (smallPretopology P P).toGrothendieck X

Tactic:
rintro ⟨𝒰, h𝒰, p, hle⟩

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h𝒰 : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ R ∈ (smallPretopology P P).toGrothendieck X
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op

Tactic:
liftAux_fac _ _ _ ha₁,

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } =
    liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op
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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
⊢ restriction data G₀ f ≫ G₀.obj.map g.op = presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
by
  have hg : (data X).sieve f g := ⟨i, p, fac⟩
  dsimp only [restriction]
  rw [G₀.2.amalgamate_map _ _ _ ⟨_, g, hg⟩]
  apply presheafObj_mapPreimage_condition
  rw [hg.some.fac, fac]

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
⊢ Presieve.IsSheaf zariskiTopology F

Tactic:
exact Presieve.isSheaf_of_le _ zariskiTopology_le_propQCTopology hF

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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
G₀✝ : Sheaf J₀ A
⊢ (F.map c ≫ Sieve.ofArrows.h hd) ≫ (data X).f (Sieve.ofArrows.i hd) = F.map (c ≫ d) ≫ f

Tactic:
simp; grind

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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
G₀✝ : Sheaf J₀ A
⊢ Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map (c ≫ d) ≫ f ≫ g

Tactic:
simp; grind

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
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
rw [← Scheme.Cover.forgetQc_toPreZeroHypercover,
      ← Scheme.Cover.isSheafFor_sigma_iff hzar, Presieve.ofArrows_of_unique]

Goal state after:
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
⊢ Presieve.IsSheafFor F (Presieve.singleton (𝒰.forgetQc.sigma.f default))
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
⊢ UniversallyClosed (toSpecZero 𝒜)

Tactic:
by
  rw [UniversallyClosed.eq_valuativeCriterion]
  exact ⟨valuativeCriterion_existence 𝒜, inferInstance⟩

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
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j ↦ X.map j.hom, naturality := ⋯ }
⊢ Mono (c.ι.app j₀)

Tactic:
have := NatTrans.mono_of_mono_app f

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j ↦ X.map j.hom, naturality := ⋯ }
this : Mono f
⊢ Mono (c.ι.app j₀)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ c₁.ι.app j ≫ (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)).hom ≫ (S.map colim).f =
    c₁.ι.app j ≫ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom

Tactic:
dsimp
    rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

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✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : (monomorphisms C).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : ∀ (j : J), Mono (f.app j)
⊢ monomorphisms C φ

Tactic:
have := NatTrans.mono_of_mono_app f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : (monomorphisms C).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this✝ : ∀ (j : J), Mono (f.app j)
this : Mono f
⊢ monomorphisms C φ
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj.obj X
⊢ (ConcreteCategory.hom (f.hom.app X)).toFun x = (ConcreteCategory.hom (g.hom.app X)).toFun x
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj.obj X
⊢ (ConcreteCategory.hom (f.hom.app X)).toFun x = (ConcreteCategory.hom (g.hom.app X)).toFun x