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

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij : Function.Bijective ⇑((CommRingCat.Hom.hom β).rangeRestrict.comp (CommRingCat.Hom.hom α))
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    ((RingEquiv.ofBijective ((CommRingCat.Hom.hom β).rangeRestrict.comp (CommRingCat.Hom.hom α))
              hbij).symm.toRingHom.comp
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
⊢ i₂ = i₂

Tactic:
]

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
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso
    ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)

Tactic:
]

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
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso
    ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)
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 𝒜
x : ↑Proj.T
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
z : A
hz : z ∈ HomogeneousIdeal.irrelevant 𝒜
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) z), ↑(((decompose 𝒜) z) i) ∈ x.asHomogeneousIdeal

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑Proj.T
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
z : A
hz : z ∈ HomogeneousIdeal.irrelevant 𝒜
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) z), ↑(((decompose 𝒜) z) i) ∈ x.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'

Tactic:
]

Goal state after:
case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
⊢ Sieve.ofArrows 𝒰.X 𝒰.f ≤ (Sieve.overEquiv X) R ↔ Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X) R

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ =
    Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

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

Tactic:
]

Goal state after:
case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ Existence f✝
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:
]

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
⊢ R ∈ (overPretopology P S).toGrothendieck X

Tactic:
]

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
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
⊢ R ∈ (overPretopology P S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

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

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) f
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case right
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
]

Goal state after:
case right
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
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
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:
]

Goal state after:
case mpr
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
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 : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
]

Goal state after:
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 : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
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:
]

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case refine_1
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd)))

Tactic:
simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]

Goal state after:
case refine_1
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i.snd))) =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case refine_2
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))

Tactic:
simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]

Goal state after:
case refine_2
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑j.snd))) =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))
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 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
⊢ IsClosedImmersion
    (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)

Tactic:
]

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 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
⊢ IsClosedImmersion
    (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)
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT✝ : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : ∃ 𝒰 x, 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT✝⟩)).arrows

Tactic:
]

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT✝ : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : ∃ 𝒰 x, 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT✝⟩)).arrows
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.f i ≫ ((MorphismProperty.Over.forget Q ⊤ S).obj X).left ↘ S)

Tactic:
]

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.f i ≫ ((MorphismProperty.Over.forget Q ⊤ S).obj X).left ↘ S)
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) ≫
      (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv =
    Spec.map (CommRingCat.ofHom F) ≫ (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv

Tactic:
]

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.Modules.Tilde

Goal state before:
pp: case h.refine_2
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
i : ι
⊢ f ^ K • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) =
    f ^ K • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)

Tactic:
]

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)
⊢ l₁ = l₂

Tactic:
let g : Z ⟶ Spec (.of S.R) := pullback.snd _ _

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)
⊢ l₁ = l₂
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 : IsAffine Z ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
⊢ IsAffine Z

Tactic:
]

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 : IsAffine Z ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
⊢ IsAffine Z