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

Goal state before:
pp: case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑g)
⊢ CompactSpace ↥(pullback f₁ f₂)

Tactic:
IsOpenImmersion.range_pullback_to_base_of_left

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑f₁ ∩ Set.range ⇑f₂)
⊢ CompactSpace ↥(pullback f₁ f₂)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact
    (Set.range
      ⇑(pullback.fst ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j) ≫
          (X.openCoverOfIsOpenCover U hU).f i))

Tactic:
IsOpenImmersion.range_pullback_to_base_of_left

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact (Set.range ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩ Set.range ⇑((X.openCoverOfIsOpenCover U hU).f j))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) = 0

Tactic:
convert! congr_arg (X.presheaf.map (homOfLE _).op).hom H

Goal state after:
case e'_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x)

case e'_3
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ 0 = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op)) 0

case refine_1.convert_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
obtain ⟨r, r', hBrr', hBfx⟩ := exists_basicOpen_le_affine_inter U₁.2 U₂.2 (f x)
    ⟨hfx₁, e₂ hx₂⟩
  have ha : IsAffineOpen (X.basicOpen (f.appLE U₂ V₂ e₂ r')) := V₂.2.basicOpen _
  have hxa : x ∈ X.basicOpen (f.appLE U₂ V₂ e₂ r') := by
    simpa [Scheme.Hom.appLE, ← Scheme.preimage_basicOpen] using And.intro hx₂ (hBrr' ▸ hBfx)
  obtain ⟨s, s', hBss', hBx⟩ := exists_basicOpen_le_affine_inter V₁.2 ha x ⟨hx₁, hxa⟩
  have := V₂.2.isLocalization_basicOpen (f.appLE U₂ V₂ e₂ r')
  have := U₂.2.isLocalization_basicOpen r'
  have := ha.isLocalization_basicOpen s'
  have ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r := by
    rw [hBss', hBrr']
    apply le_trans (X.basicOpen_le _)
    simp [Scheme.Hom.appLE]
  have heq : f.appLE (Y.basicOpen r') (X.basicOpen s') (hBrr' ▸ hBss' ▸ ers) =
      f.appLE (Y.basicOpen r') (X.basicOpen (f.appLE U₂ V₂ e₂ r')) (by simp [Scheme.Hom.appLE]) ≫
        CommRingCat.ofHom (algebraMap _ _) := by
    simp only [Scheme.Hom.appLE, homOfLE_leOfHom, Category.assoc]
    congr
    apply X.presheaf.map_comp
  refine ⟨r, s, hBx, ers, ?_⟩
  · rw [f.appLE_congr _ hBrr' hBss' (fun f => P f.hom), heq]
    apply hPa _ s' _
    rw [U₂.2.appLE_eq_away_map f V₂.2]
    exact hPl _ _ _ _ h₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))

Tactic:
have : IsIso (f.appLE (f ''ᵁ V) V.1 (f.preimage_image_eq _).ge) :=
    inferInstanceAs (IsIso (f.app _ ≫
      X.presheaf.map (eqToHom (f.preimage_image_eq _).symm).op))

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁹ : IsZariskiLocalAtTarget P
inst✝⁸ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom (Localization.awayMap f r)))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) r)).mp (IsZariskiLocalAtTarget.restrict H (basicOpen r))

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsPrime), I.height) = ringKrullDim R

Tactic:
by
  rw [← sup_height_eq_ringKrullDim, WithBot.coe_inj]
  apply le_antisymm
  · exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, le_refl _⟩
  · refine iSup_mono' fun I => ?_
    by_cases I_top : I = ⊤
    · exact ⟨⊥, by simp [I_top]⟩
    · obtain ⟨P, hP⟩ := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)
      refine ⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩
      have := hP.isPrime
      exact iInf_le_of_le P (iInf_le_of_le hP (ge_of_eq (Ideal.height_eq_primeHeight P)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0

Tactic:
induction U using reduce_to_affine_global generalizing hX with

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
xf : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ (fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
      ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) xf) =
    xf

Tactic:
obtain ⟨x, ⟨f, hf⟩⟩ := xf

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ (fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
      ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩) =
    ⟨x, ⟨f, hf⟩⟩
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial ≫ (Spec R).residue x

Tactic:
← Spec.algebraMap_stalkIso_inv_assoc

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (Spec.stalkIso R x).inv ≫ (Spec R).residue x
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ ⇑fst ⁻¹' s ⊆ ⇑(snd ≫ g) ⁻¹' ⇑f '' s

Tactic:
← h.1.1

Goal state after:
case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ ⇑fst ⁻¹' s ⊆ ⇑(fst ≫ f) ⁻¹' ⇑f '' s
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
e : CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ ↑U) :=
  (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).symm ≪≫
    (Hom.appIso (I.subschemeCover.f U) ⊤).symm ≪≫ Functor.mapIso I.subscheme.presheaf (eqToIso ⋯).op
⊢ RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv)) =
    I.ideal U

Tactic:
change RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp
    (Ideal.Quotient.mk (I.ideal U))) = _

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
e : CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ ↑U) :=
  (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).symm ≪≫
    (Hom.appIso (I.subschemeCover.f U) ⊤).symm ≪≫ Functor.mapIso I.subscheme.presheaf (eqToIso ⋯).op
⊢ RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app (↑U).ι ((↑U).ι ''ᵁ ⊤) ≫ Hom.appLE (pullback.snd f (↑U).ι) ((↑U).ι ⁻¹ᵁ (↑U).ι ''ᵁ ⊤) ⊤ ⋯ =
    Hom.appLE (pullback.snd f (↑U).ι ≫ 𝟙 ↑↑U) ⊤ ⊤ ⋯

Tactic:
Opens.ι_app

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (pullback.snd f (↑U).ι) ((↑U).ι ⁻¹ᵁ (↑U).ι ''ᵁ ⊤) ⊤ ⋯ =
    Hom.appLE (pullback.snd f (↑U).ι ≫ 𝟙 ↑↑U) ⊤ ⊤ ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ toImageAux f ≫ imageι f = f

Tactic:
apply Cover.hom_ext ((Y.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top Y)).pullback₁ f)

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ ∀ (x : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀),
    (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f x ≫ toImageAux f ≫ imageι f =
      (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f x ≫ f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑(Hom.toImage f)) = Set.univ

Tactic:
f.imageι.isEmbedding.closure_eq_preimage_closure_image,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ ⇑(Hom.imageι f) ⁻¹' closure (⇑(Hom.imageι f) '' Set.range ⇑(Hom.toImage f)) = Set.univ
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))

Tactic:
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈
    adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
⊢ EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ Scheme.Spec X)

Tactic:
let F := MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj _ _
  refine .of_functor F ?_ ?_
  · let Q' : ObjectProperty CommRingCat.{u} := fun S ↦
      ∃ R, (R ∈ Set.range fun U ↦ Γ(X, U)) ∧ ∃ (f : R ⟶ S), f.hom.FiniteType
    have : Q'.EssentiallySmall := CommRingCat.essentiallySmall_of_finiteType fun S ↦ id
    suffices ObjectProperty.EssentiallySmall.{u} (· ∈ Set.range (Opposite.unop ∘ F.obj)) by
      rw [← ObjectProperty.essentiallySmall_unop_iff]
      refine .of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_
      exact fun R ⟨S, e⟩ ↦ ⟨_, ⟨S, rfl⟩, ⟨e.some.unop⟩⟩
    refine CommRingCat.essentiallySmall_of_localizationAway (Q := Q'.isoClosure) ?_
    rintro _ ⟨S, rfl⟩
    have (q : Spec (F.obj S).unop) : ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧
        Q' Γ(Spec (F.obj S).unop, PrimeSpectrum.basicOpen f) := by
      obtain ⟨_, ⟨U, hU, rfl⟩, hqU, -⟩ :=
        X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ <| S.hom q) isOpen_univ
      obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen
      have : LocallyOfFiniteType S.hom := hP _ S.prop
      exact ⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩
    choose f hqf hf using this
    refine ⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩
    · exact top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, hqf _⟩
    · dsimp
      exact fun q ↦ ⟨_, hf q, ⟨(IsLocalization.algEquiv (.powers (f q)) _
        ((Spec.structureSheaf _).obj.obj (op _))).toRingEquiv.toCommRingCatIso⟩⟩
  · intro R
    refine ⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩
    refine fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩
    · simp [← Spec.map_comp_assoc, F]
    · exact (P.cancel_left_of_respectsIso _ _).mpr S.prop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso (Scheme.Hom.imageι f)

Tactic:
simpa [Scheme.Hom.imageι, Scheme.Hom.image] using H ▸ inferInstance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso ((overEquivIdealSheafData X).functor.map f'.op)

Tactic:
simpa [IsClosedImmersion.overEquivIdealSheafData] using ⟨homOfLE h'.le, by simp, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ f ((pullback.fst f f) x) = f ((pullback.snd f f) x)

Tactic:
by rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case e'_2
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsSeparated (f ≫ terminal.from Y) ↔ AffineTargetMorphismProperty.of (@IsSeparated) f

Tactic:
IsSeparated.comp_iff

Goal state after:
case e'_2
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsSeparated f ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
⊢ p z ∈ U (Scheme.Cover.idx 𝒰 (p z))

Tactic:
by simpa [U] using 𝒰.covers (p z)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
wlog hY : IsAffine Y
  · rw [← monomorphisms.iff, IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := monomorphisms _) Y.affineCover]
    simp_rw [this, forall_and]
  rw [HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion),
    HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    RingHom.surjective_iff_epi_and_finite, @and_comm (Epi _), ← and_assoc]
  refine and_congr_right fun ⟨_, _⟩ ↦
    Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)
  trans Mono (f.app ⊤).op
  · exact ⟨fun h ↦ inferInstance, fun h ↦ show Epi (f.app ⊤).op.unop by infer_instance⟩
  exact (Functor.mono_map_iff_mono Scheme.Spec _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

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

Tactic:
rw [← universally_eq_iff (P := @QuasiCompact).mpr inferInstance, ← universally_inf]

Goal state after:
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ ∃
    U' ∈
      {x |
        ∃ r,
          ∃ (_ : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)), X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = x},
    x ∈ U' ∧ U' ≤ U

Tactic:
refine ⟨_, ⟨r, ?_, rfl⟩, hxr, (Set.preimage_mono hrU).trans_eq
    (Set.preimage_image_eq _ X.toSpecΓ.isEmbedding.injective)⟩

Goal state after:
X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this : CompactSpace ↥X
x : ↥X
⊢ ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r

Tactic:
obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ := (IsQuasiAffine.isBasis_basicOpen
    Y).exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this : CompactSpace ↥X
x : ↥X
r : ↑Γ(Y, ⊤)
hr : IsAffineOpen (Y.basicOpen r)
hxr : f x ∈ ↑(Y.basicOpen r)
⊢ ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r