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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) ≤
    RingHom.ker (CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))

Tactic:
intro x

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
x : ↑Γ(Y, ⊤)
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) →
    x ∈ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))
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
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 ⋯

Tactic:
convert! germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU

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

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
by
  ext x
  simpa [Scheme.Hom.appLE] using! map_eq_zero_iff _
    (ConcreteCategory.bijective_of_isIso
      (X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op)).1

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ Spec.map (residueFieldIso R x).inv ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField)) =
    (Spec R).fromSpecResidueField x

Tactic:
by
  simp only [Scheme.fromSpecResidueField, Spec.fromSpecStalk_eq, ← Spec.map_comp]
  rw [Spec.map_inj]
  simp [← Scheme.Spec.algebraMap_residueFieldIso_inv]

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

Goal state before:
pp: case a.inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

Tactic:
intro x

Goal state after:
case a.inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
x : ↥Y
⊢ x ∈ ↑(ker f).support → x ∈ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

Tactic:
intro x

Goal state after:
case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
x : ↥(Spec S)
⊢ x ∈ ↑(ker f).support → x ∈ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
have : IsAffine X := by
      apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
      · apply_fun Ideal.map (f.appTop).hom at hs
        rwa [Ideal.map_span, Ideal.map_top] at hs
      · rintro - ⟨r, hr, rfl⟩
        simp_rw [Scheme.preimage_basicOpen] at hf
        exact (hf ⟨r, hr⟩).left

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥Y), ∃ U, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ IsAffineHom f

Tactic:
by
  choose U hxU hU hfU using H
  rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]
  · exact hfU
  · exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

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

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf✝¹ : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
left✝ : IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑a)
hf✝ : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen ↑a).ι ''ᵁ ⊤)))
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen ↑a).ι ''ᵁ ⊤)))
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)

Tactic:
rw [Scheme.Opens.ι_image_top] at hf

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf✝¹ : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
left✝ : IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑a)
hf✝ : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen ↑a).ι ''ᵁ ⊤)))
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen ↑a)))
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := ⋯
⊢ coprod.desc f g ⁻¹ᵁ W ≤ Scheme.Hom.opensRange i

Tactic:
intro x

Goal state after:
case a
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥(U ⨿ V)
⊢ x ∈ coprod.desc f g ⁻¹ᵁ W → x ∈ Scheme.Hom.opensRange i
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 ⊆ ⇑(ConcreteCategory.hom (fst.base ≫ f.base)) ⁻¹' ⇑f '' s

Tactic:
TopCat.coe_comp,

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 ⊆ ⇑f ∘ ⇑fst ⁻¹' ⇑f '' s
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' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ∃ m, m • x ∈ A

Tactic:
use a * y ^ n

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := ⋯
y : ↥M := ⋯
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ (a * y ^ n) • x ∈ A
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
⊢ ↑I.support ⊆ Set.range ⇑I.gluedTo

Tactic:
intro x

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
x : ↥X
⊢ x ∈ ↑I.support → x ∈ Set.range ⇑I.gluedTo
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 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))

Tactic:
intro 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 := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x✝ x : S
⊢ x ∈ ↑s → x ∈ ↑(adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support))
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case refine_1
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
r : ↑↑s
⊢ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r)) ⊆
    ↑(adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)))

Tactic:
intro x

Goal state after:
case refine_1
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
r : ↑↑s
x : S
⊢ x ∈ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r)) →
    x ∈ ↑(adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)))
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ IsStableUnderBaseChange @Finite

Tactic:
by
  refine IsStableUnderBaseChange.mk finite_respectsIso ?_
  simp only [finite_algebraMap]
  intros
  infer_instance

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

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f) (Scheme.Hom.toImage f)

Tactic:
intro x

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
x : ↥X
⊢ Function.Bijective ⇑(CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.toImage f) x))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤ I

Tactic:
← I.ker_subschemeι,

Goal state after:
case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤ Hom.ker I.subschemeι
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ Set.range ⇑(ConcreteCategory.hom ((vanishingIdeal Z).subschemeι.base ≫ f.base))

Tactic:
TopCat.coe_comp,

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ Set.range (⇑f ∘ ⇑(vanishingIdeal Z).subschemeι)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑(ConcreteCategory.hom (I.subschemeι.base ≫ f.base))) =
    ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))

Tactic:
TopCat.coe_comp,

Goal state after:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range (⇑f ∘ ⇑I.subschemeι)) = ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: 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 = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
⊢ ∀ x ∈ ↑s, FiniteType R (Localization.Away x)

Tactic:
intro 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 = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
x : S
⊢ x ∈ ↑s → FiniteType R (Localization.Away x)
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: 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 = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
ht : Ideal.span ↑t = ⊤
this : FinitePresentation R A
g : ↥t
r : S
hr : r ∈ s
hrr : (Ideal.Quotient.mk I) (g' ⟨r, hr⟩) = ↑g
⊢ FinitePresentation R (Localization.Away ((Ideal.Quotient.lift I (↑f) hfI) ((Ideal.Quotient.mk I) (g' ⟨r, hr⟩))))

Tactic:
Ideal.Quotient.lift_mk

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 = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
ht : Ideal.span ↑t = ⊤
this : FinitePresentation R A
g : ↥t
r : S
hr : r ∈ s
hrr : (Ideal.Quotient.mk I) (g' ⟨r, hr⟩) = ↑g
⊢ FinitePresentation R (Localization.Away (↑f (g' ⟨r, hr⟩)))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
simp only [← f.toImage_imageι, Scheme.Hom.comp_appTop, CommRingCat.hom_comp, RingHom.coe_comp,
    Scheme.Hom.image, Scheme.Hom.imageι]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.toImage f))) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.ker f).subschemeι)))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0

Tactic:
let e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
      (Algebra.TensorProduct.comm R _ _).trans (polyEquivTensor R x.asIdeal.ResidueField).symm

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Function.Surjective (comap C)

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ ∃ a, comap C a = x
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
⊢ ∀ (a : ↥X), IsOpen {a}

Tactic:
intro x

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
⊢ IsOpen {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ Function.Surjective (comap C)

Tactic:
intro x

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ ∃ a, comap C a = x
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝¹ : IsIntegral Y
x✝ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : ↑(U i) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
⊢ P X

Tactic:
let e' : ↑(f ⁻¹ᵁ U i) ≅ X := X.isoOfEq (by simp [heq]) ≪≫ X.topIso

Goal state after:
P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝¹ : IsIntegral Y
x✝ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : ↑(U i) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
e' : ↑(f ⁻¹ᵁ U i) ≅ X := X.isoOfEq ⋯ ≪≫ X.topIso
⊢ P X
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
⊢ geometrically P f

Tactic:
geometrically_iff_of_isClosedUnderIsomorphisms

Goal state after:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
⊢ ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
⊢ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)) ≤ ⊥

Tactic:
intro x

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)) → x ∈ ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : JacobsonSpace ↥Y
inst✝ : LocallyOfFiniteType f
⊢ closedPoints ↥X ⊆ ⇑f ⁻¹' closedPoints ↥Y

Tactic:
intro x

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : JacobsonSpace ↥Y
inst✝ : LocallyOfFiniteType f
x : ↥X
⊢ x ∈ closedPoints ↥X → x ∈ ⇑f ⁻¹' closedPoints ↥Y