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

Goal state before:
pp: X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂

Tactic:
e₂,

Goal state after:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
⊢ p.primeHeight = p.height

Tactic:
exact (Ideal.height_eq_primeHeight _).symm

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 : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
by
  rw [iff_of_source_openCover (P := P) (Scheme.coverOfIsIso.{u} (𝟙 _))]
  simp +instances

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ R, X = Spec R
⊢ P f ↔ Q f

Tactic:
obtain ⟨R, rfl⟩ := hX

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
f : Spec R ⟶ Spec S
⊢ P f ↔ Q f
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X✝ X : Scheme
x : ↥X
hx : closure {x} ∈ irreducibleComponents ↥X
inst✝ : IsReduced X
hX : ∃ R, X = Spec R
⊢ IsField ↑(X.presheaf.stalk x)

Tactic:
obtain ⟨R, rfl⟩ := hX

Goal state after:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : closure {x} ∈ irreducibleComponents ↥(Spec R)
inst✝ : IsReduced (Spec R)
⊢ IsField ↑((Spec R).presheaf.stalk x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V

Tactic:
enter [

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : IsEmpty 𝒰.I₀
this : IsEmpty ↥X
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

Tactic:
simp [ker_eq_top_of_isEmpty]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V

Tactic:
enter [

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V
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:
rw [← Spec.algebraMap_stalkIso_inv_assoc]; rfl

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

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (↑↑U ∩ ↑↑V ∩ ↑(⨆ i ∈ ↑s', X.basicOpen i))

Tactic:
← iSup_subtype'',

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (↑↑U ∩ ↑↑V ∩ ↑(⨆ i, X.basicOpen ↑i))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
hX : ∃ R, X = Spec R
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

Tactic:
obtain ⟨R, rfl⟩ := hX

Goal state after:
X Y : Scheme
S R : CommRingCat
f : Spec R ⟶ Spec S
inst✝ : QuasiCompact f
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
let e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(Limits.pullback (C := Scheme) f U.1.ι, ⊤) :=
    X.presheaf.mapIso (eqToIso (by simp [Scheme.Hom.opensRange_pullbackFst])).op
      ≪≫ (Limits.pullback.fst (C := Scheme) f U.1.ι).appIso ⊤
  have he : f.app U ≫ e.hom =
      (ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop := by
    rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
    simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
    rw [Hom.comp_appLE, Opens.ι_app]
    exact Hom.map_appLE _ _ (homOfLE le_top).op
  rw [← he]
  refine (IdealSheafData.ideal_ofIdeals_le _ _).trans_eq
    (RingHom.ker_equiv_comp _ e.commRingCatIsoToRingEquiv).symm

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

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme),
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
⊢ IsAffineHom (f ∣_ ↑U)

Tactic:
exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) U.2

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

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

Tactic:
have : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd _ _) ≫ J.subschemeι =
        I.subschemeι ≫ f := by simp [← pullback.condition]

Goal state after:
case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ J ≤ I.map f
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
enter [

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑f = ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f

Tactic:
exact (Set.image_preimage_eq_of_subset (by simpa using! subset_coborder)).symm

Goal state after:
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
⊢ FinitePresentation R S

Tactic:
let f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI

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
⊢ FinitePresentation R S
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
⊢ (Ideal.Quotient.mk I) (∑ g, g' g * h' g - 1) = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem

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
⊢ ∑ g, g' g * h' g - 1 ∈ I
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
⊢ X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f

Tactic:
rw [Scheme.isSeparated_iff, ← terminal.comp_from f, 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.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
hX : ∃ R, X = Spec R
⊢ IsClosedImmersion g

Tactic:
obtain ⟨R, rfl⟩ := hX

Goal state after:
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
⊢ IsClosedImmersion g
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)
⊢ geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst : Field K] [inst_1 : Algebra R K] ⦃Y : Scheme⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
      IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y

Tactic:
by
  refine ⟨fun hs K _ _ Z fst snd h ↦ hs _ _ _ h, fun H K _ y Z fst snd h ↦ ?_⟩
  obtain ⟨φ, rfl⟩ := Spec.map_surjective y
  algebraize [φ.hom]
  exact H fst snd h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
⊢ IsReduced X

Tactic:
let Z := ∐ fun Z ↦ Spec (pt Z)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
⊢ IsReduced X
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),
    RingHom.finite_iff_isIntegral_and_finiteType, ← and_assoc]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
X : Scheme
inst✝¹ : Subsingleton ↥X
inst✝ : IsReduced X
f : X ⟶ Spec S
hX : ∃ R, X = Spec R
h✝ : Nonempty ↥X
this : IrreducibleSpace ↥X
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
obtain ⟨R, rfl⟩ := hX

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
f : Spec R ⟶ Spec S
h✝ : Nonempty ↥(Spec R)
this : IrreducibleSpace ↥(Spec R)
⊢ IsFinite f ↔ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤))
    ((ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝))

Tactic:
enter [

Goal state after:
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤))
    ((ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
    ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

Tactic:
enter [

Goal state after:
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
    ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n

Tactic:
constructor
  · intro h
    cases isEmpty_or_nonempty S
    · exact .inl ‹_›
    refine .inr ?_
    wlog hS : ∃ R, S = Spec R
    · obtain ⟨x⟩ := ‹Nonempty S›
      obtain ⟨y, hy⟩ := S.affineCover.covers x
      exact this (S.affineCover.X _) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
        (isPullback_map (S.affineCover.f _)) h) ⟨y⟩ ⟨_, rfl⟩
    obtain ⟨R, rfl⟩ := hS
    have : Nontrivial R := (subsingleton_or_nontrivial R).resolve_left fun H ↦
        not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))
    constructor
    intro i
    have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso.{u}
    rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom (SpecIso n R).inv,
      SpecIso_inv_over, HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)] at h
    obtain ⟨p : Polynomial R, hp, hp'⟩ :=
      (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
        (arrowIsoΓSpecOfIsAffine _)).mpr h.2 (X i)
    have : (rename fun _ ↦ i).comp (uniqueAlgEquiv.{_, u} _ PUnit).symm.toAlgHom p = 0 := by
      simp [← hp', ← algebraMap_eq]
    rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this
    simp only [AlgEquiv.coe_toAlgHom, EmbeddingLike.map_eq_zero_iff] at this
    simp [this] at hp
  · rintro (_ | _) <;> infer_instance

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

Goal state before:
pp: case intro.h₂
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := ⋯
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := ⋯
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) := ⋯
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) := ⋯
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) := ⋯
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
val✝ : Fintype ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) := ⋯
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) := ⋯
⊢ ((ψY.comp (CommRingCat.Hom.hom (pushoutSection H hUST hUSX hUY))).comp (CommRingCat.Hom.hom e.inv)).comp
      Algebra.TensorProduct.includeRight.toRingHom =
    (φ.comp (Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ).toRingHom).comp
      Algebra.TensorProduct.includeRight.toRingHom

Tactic:
· have H₁ : e.inv.hom.comp Algebra.TensorProduct.includeRight.toRingHom =
        (pushout.inl (C := CommRingCat) _ _).hom :=
      congr($((CommRingCat.isPushout_tensorProduct _ _ _).flip.inl_isoPushout_hom).hom)
    have H₂ (x j) : φ (1 ⊗ₜ[↑Γ(S, US)] x) j = pushoutSection H hUST (UX := VX j) (by simp_all) rfl
        (pushout.inl (C := CommRingCat) _ _ (x j)) := congr(pushoutSection H hUST (UX := VX j) _ rfl
        ($((CommRingCat.isPushout_tensorProduct ↑Γ(S, US)
          ↑Γ(T, UT) ↑Γ(X, VX j)).flip.inl_isoPushout_hom) (x j)))
    simp only [RingHom.comp_assoc, H₁]
    ext x j
    simp [ψY, H₂, -CommRingCat.hom_comp, ← CategoryTheory.comp_apply, pushoutSection, ψ]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
⊢ (if w ∈ h.toFinset then D w else 0) = D w

Tactic:
set s := h.toFinset with hs

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
⊢ (if w ∈ s then D w else 0) = D w
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ closure {⊥} = Set.univ

Tactic:
rw [← PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.vanishingIdeal_singleton]

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
⊢ ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩

Tactic:
Scheme.homOfLE_base

Goal state after:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
⊢ ⟨x, ⋯⟩ = (ConcreteCategory.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE hU'))) ⟨x, hx⟩
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ g.equiv f

Tactic:
exact ⟨W, hW, hWr, hWl, e.symm⟩

Goal state after: