mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
⊢ IsLocalization ((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl
    (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)

Tactic:
constructor

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl.IsLocalizationMap
    ⇑(algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl.IsLocalizationMap
    ⇑(algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
constructor

Goal state after:
case map_units
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ∀ (y : ↥((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl),
    IsUnit ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑y)

case surj
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ∀ (z : AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal),
    ∃ x_1,
      z * (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑x_1.2 =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1.1

case exists_of_eq
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ∀ {x_1 y : A⁰_ f},
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1 =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y →
      ∃ c, ↑c * x_1 = ↑c * y
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) := ⋯
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) := ⋯
⊢ (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯)
      (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0) =
    HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }

Tactic:
ext

Goal state after:
case h
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) := ⋯
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) := ⋯
⊢ val
      ((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯)
        (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0)) =
    (HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }).val
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Existence.IsStableUnderBaseChange

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Y' S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
    IsPullback f' g' g f → Existence g → Existence g'
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) ↔ ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

Tactic:
constructor

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: ⊢ Existence = (topologically @SpecializingMap).universally

Tactic:
ext

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ ↔ (topologically @SpecializingMap).universally f✝
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ ↔ (topologically @SpecializingMap).universally f✝

Tactic:
constructor

Goal state after:
case mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ → (topologically @SpecializingMap).universally f✝

case mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ Existence.universally f✝

Tactic:
rwa [MorphismProperty.IsStableUnderBaseChange.universally_eq]

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left ↔ R ∈ (overPretopology P S).toGrothendieck X

Tactic:
constructor

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left → R ∈ (overPretopology P S).toGrothendieck X

case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
constructor

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (overPretopology P S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ ⋯.HasLift

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ Nonempty ⋯.LiftStruct
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ Nonempty ⋯.LiftStruct

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ ⋯.LiftStruct
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
⊢ Subsingleton ⋯.LiftStruct

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
⊢ ∀ (a b : ⋯.LiftStruct), a = b
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 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ e₂.inv ≫
      ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1) ((affineOpenCover 𝒜).openCover.f (i, j).2)
              (toSpecZero 𝒜)).inv ≫
          snd (diagonal (toSpecZero 𝒜))
            ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                  (toSpecZero 𝒜)).f
              (i, j))) ≫
        e₁.hom =
    Spec.map (CommRingCat.ofHom F)

Tactic:
rw [← cancel_mono (pullbackSpecIso ..).inv]

Goal state after:
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ (e₂.inv ≫
        ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1) ((affineOpenCover 𝒜).openCover.f (i, j).2)
                (toSpecZero 𝒜)).inv ≫
            snd (diagonal (toSpecZero 𝒜))
              ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                    (toSpecZero 𝒜)).f
                (i, j))) ≫
          e₁.hom) ≫
      (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv =
    Spec.map (CommRingCat.ofHom F) ≫ (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: 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)
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows) ↔
    ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
constructor

Goal state after:
case mp
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)
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows) →
    ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

case mpr
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)
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
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
⊢ Function.Bijective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
constructor

Goal state after:
case left
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 := ⋯
g : Z ⟶ Spec (CommRingCat.of S.R) := ⋯
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

case right
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 := ⋯
g : Z ⟶ Spec (CommRingCat.of S.R) := ⋯
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: 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
⊢ R ∈ (smallPretopology P P).toGrothendieck X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
constructor

Goal state after:
case mp
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
⊢ R ∈ (smallPretopology P P).toGrothendieck X →
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

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
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 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : Kmax = 0
this : ∀ (i : ι), φ (Away.isLocalizationElem ⋯ ⋯) = 0 ∧ ¬∏ k ∈ Finset.univ.erase i, d k = 0
⊢ 1 = Away.isLocalizationElem ⋯ ⋯

Tactic:
ext

Goal state after:
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := ⋯
this✝ : Nonempty ι
Kmax : ValueGroup O K := ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : Kmax = 0
this : ∀ (i : ι), φ (Away.isLocalizationElem ⋯ ⋯) = 0 ∧ ¬∏ k ∈ Finset.univ.erase i, d k = 0
⊢ val 1 = val (Away.isLocalizationElem ⋯ ⋯)
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i i' : I
f : i ⟶ i'
⊢ ((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).map f ≫ ⟨limit.π (F ⋙ π A) i', ⋯⟩ =
    ⟨limit.π (F ⋙ π A) i, ⋯⟩ ≫ F.map f

Tactic:
ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i i' : I
f : i ⟶ i'
⊢ ↑(((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).map f ≫ ⟨limit.π (F ⋙ π A) i', ⋯⟩) =
    ↑(⟨limit.π (F ⋙ π A) i, ⋯⟩ ≫ F.map f)
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
⊢ (∃ j f,
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
        (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂) ↔
    ∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
⊢ (∃ j f,
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
        (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂) →
    ∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂

case mpr
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
⊢ (∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂) →
    ∃ j f,
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
        (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
X✝ Y✝ : Cᵒᵖ ⥤ D
f✝ : X✝ ⟶ Y✝
⊢ ((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f✝ ≫
      {
        app := fun x ↦
          match x with
          | Opposite.op X => Y✝.map (hT.from X).op,
        naturality := ⋯ } =
    {
        app := fun x ↦
          match x with
          | Opposite.op X => X✝.map (hT.from X).op,
        naturality := ⋯ } ≫
      (𝟭 (Cᵒᵖ ⥤ D)).map f✝

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
X✝ Y✝ : Cᵒᵖ ⥤ D
f✝ : X✝ ⟶ Y✝
x✝ : Cᵒᵖ
⊢ (((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f✝ ≫
          {
            app := fun x ↦
              match x with
              | Opposite.op X => Y✝.map (hT.from X).op,
            naturality := ⋯ }).app
      x✝ =
    ({
            app := fun x ↦
              match x with
              | Opposite.op X => X✝.map (hT.from X).op,
            naturality := ⋯ } ≫
          (𝟭 (Cᵒᵖ ⥤ D)).map f✝).app
      x✝