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

Goal state before:
pp: case refine_3
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) :=
  fun ijk ↦
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).f ijk.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f ijk.fst) ∧
            P.2 ∈
              Scheme.Hom.opensRange ((𝒲 ijk.fst).f ijk.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f g) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))
⊢ ∀ (i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀),
    IsEmbedding ((fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)) ∘ ⇑(𝓤.f i))

Tactic:
· intro i
    have := H (S.affineOpenCover.X i.1) (((𝒰.pullback₁ f).X i.1).affineOpenCover.X i.2.1)
        (((𝒰.pullback₁ g).X i.1).affineOpenCover.X i.2.2)
        ((𝒱 i.1).f i.2.1 ≫ 𝒰.pullbackHom f i.1)
        ((𝒲 i.1).f i.2.2 ≫ 𝒰.pullbackHom g i.1)
        ((𝒱 i.1).f i.2.1 ≫ (𝒰.pullback₁ f).f i.1)
        ((𝒲 i.1).f i.2.2 ≫ (𝒰.pullback₁ g).f i.1)
        (𝒰.f i.1) (by simp [pullback.condition]) (by simp [pullback.condition])
        inferInstance inferInstance inferInstance
    convert! this using 7
    apply pullback.hom_ext <;>
      simp [𝓤, Scheme.Cover.pullbackHom]

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

Goal state before:
pp: case inr.refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
⊢ ∃ a, ↑s = Y.basicOpen a

Tactic:
obtain ⟨a, ha⟩ := hUs s.2
        use a, ha.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) = I.ideal U

Tactic:
rw [U.2.ideal_ext_iff]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ ∀ (x : ↥X) (h_1 : x ∈ ↑U),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1)) (I.ideal U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
⊢ False

Tactic:
obtain ⟨⟨s', ⟨_, n, rfl⟩⟩, hs'⟩ :=
    (IsLocalization.mem_map_algebraMap_iff (.powers f) Γ(X, X.basicOpen f)).mp this

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
      (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) n, ⋯⟩).2 =
    (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) n, ⋯⟩).1
⊢ False
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ stalkClosedPointTo (f ≫ g) = Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
rw [stalkClosedPointTo, Scheme.Hom.stalkMap_comp]

Goal state after:
X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ (Hom.stalkMap g (f (closedPoint ↑R)) ≫ Hom.stalkMap f (closedPoint ↑R)) ≫ (stalkClosedPointIso R).hom =
    Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : (X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯

Tactic:
have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp

Goal state after:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : (X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
this : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i = 𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2)

Tactic:
apply pullback.hom_ext
    · rw [← cancel_mono (glueDataObjι _ _)]
      simp [pullback.condition]
    · simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ x ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := ⋯
x : S
⊢ ↑s ⊆ ↑(adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support))

R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := ⋯
x : S
⊢ ∀ (i : ↑↑s), l i ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := ⋯
x : S
⊢ ∀ (r : ↑↑s), ∃ n, ↑r ^ n • x ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝ : IsEmpty ↥X
f : X ⟶ Y
⊢ IsClosed (Set.range ⇑f)

Tactic:
Set.range_eq_empty

Goal state after:
X Y : Scheme
inst✝ : IsEmpty ↥X
f : X ⟶ Y
⊢ IsClosed ∅
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (Spec.map f) x))

Tactic:
by
    have : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by
      rw [← RingHom.toMorphismProperty_respectsIso_iff]
      exact RingHom.surjective_respectsIso
    apply (MorphismProperty.arrow_mk_iso_iff
      (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
      (Scheme.arrowStalkMapSpecIso f x)).mpr
    exact RingHom.surjective_localRingHom_of_surjective f.hom h x.asIdeal

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
let res (i : 𝒰.I₀) : Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := (𝒰.f i).appTop

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
⊢ IsSeparated f

Tactic:
wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _
      (iSup_affineOpens_eq_top Y)]
    intro U
    have H : IsAffineHom (f ∣_ U) := IsZariskiLocalAtTarget.restrict h U
    exact this _ U.2
  have : IsAffine X := HasAffineProperty.iff_of_isAffine.mp h
  rw [MorphismProperty.arrow_mk_iso_iff @IsSeparated (arrowIsoSpecΓOfIsAffine f)]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.lift (𝟙 X) f ⋯)

Tactic:
← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (pullback.fst f (𝟙 Y))

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective
    (⇑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B)) ∘
      ⇑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm ∘
        ⇑(Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val) ∘
          ⇑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B') ∘
            ⇑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))

Tactic:
simp_rw [EmbeddingLike.comp_injective, ← Function.comp_assoc, EquivLike.injective_comp]

Goal state after:
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective ⇑(Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (comap C '' ⋃₀ S)

Tactic:
Set.image_sUnion

Goal state after:
R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋂ i, zeroLocus {↑i})ᶜ

Tactic:
Set.compl_iInter

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋃ i, (zeroLocus {↑i})ᶜ)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsCompact (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
by
  obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg
  rw [ht, ← (t : Set R).iUnion_of_singleton_coe, zeroLocus_iUnion, Set.compl_iInter]
  apply isCompact_iUnion
  exact fun _ ↦ by simpa using isCompact_basicOpen _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_

Goal state after:
case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
x : ↥X
⊢ IsOpen {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (comap C '' ⋃₀ S)

Tactic:
Set.image_sUnion

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯.toField
⊢ P Z

Tactic:
apply hf (W.isoSpec.inv ≫ q) snd (fst ≫ W.isoSpec.hom)

Goal state after:
case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
Z S X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ R, Y = Spec R
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) →
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
exact fun a i ↦ this _ ⟨_, rfl⟩ (a i)

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

Goal state before:
pp: R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ IsOpen s

Tactic:
refine ((PrimeSpectrum.isQuotientMap_of_generalizingMap ?_ ?_).isOpen_preimage).mp hs

Goal state after:
case refine_1
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

case refine_2
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app (Classical.arbitrary I)) ⋯ = s.ι.app j

Tactic:
change _ ≫ f _ = _

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f (Classical.arbitrary I) = s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
by
  rw [descColimitType_injective_iff_of_isFiltered]
  constructor
  · intro h j x x' eq
    obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
    refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
    rw [map_comp, comp_apply, eq]
    simp only [← comp_apply, ← map_comp]
    rw [coeq_condition]
  · intro h j j' x x' eq
    obtain ⟨k, g, eq⟩ := h (max j j') (F.map (leftToMax _ _) x)
      (F.map (rightToMax _ _) x') (by simpa only [c.ι_naturality_apply])
    exact ⟨k, leftToMax _ _ ≫ g, rightToMax _ _ ≫ g, by simp [eq]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosedImmersion (X.fromSpecResidueField x)
⊢ IsFinite (X.fromSpecResidueField x ≫ f)

Tactic:
rw [isFinite_iff_locallyOfFiniteType_of_jacobsonSpace]

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosedImmersion (X.fromSpecResidueField x)
⊢ LocallyOfFiniteType (X.fromSpecResidueField x ≫ f)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
this✝ : IsClosedImmersion ↑p
this : IsClosed (Set.range ⇑↑p)
⊢ ↑p (IsLocalRing.closedPoint K) ∈ closedPoints ↥X

Tactic:
rwa [Set.range_eq_singleton] at this

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
this✝ : IsClosedImmersion ↑p
this : IsClosed (Set.range ⇑↑p)
⊢ ∀ (x : ↥(Spec (CommRingCat.of K))), ↑p x = ↑p (IsLocalRing.closedPoint K)