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

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
⊢ x ∈ U → ∃ U_1 f, (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1

Tactic:
hx

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
⊢ LocallyQuasiFinite f

Tactic:
change id _

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
⊢ LocallyQuasiFinite f

Tactic:
change id _

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ IsIso (pullback.snd (colimit.desc F (cocone X)) (↑U).ι)

Tactic:
let e := IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) U.1.ι)
      (U.2.isoSpec.hom ≫ colimit.ι F U) <| by
      rw [Pullback.range_fst, Opens.range_ι, ← Hom.coe_opensRange, Hom.opensRange_comp_of_isIso,
        ← Scheme.Hom.coe_preimage]
      convert! congr($(D.toBase_preimage_eq_opensRange_ι U).1)
      · delta cocone
        congr with U
        simp [D, relativeGluingData, restrictIsoSpec]
      · simp

Goal state after:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e : pullback (colimit.desc F (cocone X)) (↑U).ι ≅ ↑↑U :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ IsIso (pullback.snd (colimit.desc F (cocone X)) (↑U).ι)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ (algebraMap R[X] R⟮X⟯) 0 = 0

pp: case inl.hq
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ 1 ≠ 0

Tactic:
map_zero

Goal state after:
case inl
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ 0 = 0

case inl.hq
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ 1 ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num ∣ p

Tactic:
rw [num_div _ q, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ denom 0 = 1

Tactic:
convert! denom_div (0 : K[X]) one_ne_zero

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (1 / gcd 0 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num /
      (algebraMap K[X] K⟮X⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
num_div p q,

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)) /
      (algebraMap K[X] K⟮X⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
rw [num_dvd (mul_ne_zero (num_ne_zero hx) (num_ne_zero hy))]

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ q, q ≠ 0 ∧ x * y = (algebraMap K[X] K⟮X⟯) (x.num * y.num) / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra R S✝
inst✝ : Algebra R T
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
x : S
⊢ P.HasMap ((Ideal.Quotient.mk I) x) → ∃! a, ↑a - x ∈ I

Tactic:
hx

Goal state after:
R : Type u_1
S✝ : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra R S✝
inst✝ : Algebra R T
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
⊢ ∃! a, ↑a - x ∈ I
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) 0 = 0

Tactic:
map_zero

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ 0 = 0
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum.natDegree ≤
    f.natDegree - 1

Tactic:
refine (natDegree_multiset_sum_le _).trans (Multiset.max_le_of_forall_le _ _ ?_)

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ ∀
    x ∈
      Multiset.map natDegree
        (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m),
    x ≤ f.natDegree - 1
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ (algebraMap S S') 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
⊢ ∃ n, p.leadingCoeff ^ n • t ∈ conductor R (φ X)

Tactic:
have (x : _) : ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range := by
    have : φ p * t * x ∈ φ.range := by simpa [← AlgHom.map_adjoin_singleton] using hp x
    obtain ⟨q, n, hn⟩ :=
      exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range φ _ p
        (hφ.to_isIntegral (t * x)) (by convert! this using 1; ring)
    obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn
    exact ⟨n, (C r + q), by simp [← Polynomial.algebraMap_eq, -Polynomial.algebraMap_apply, hr]⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
this : ∀ (x : S), ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range
⊢ ∃ n, p.leadingCoeff ^ n • t ∈ conductor R (φ X)
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrQ : ↑r ∉ Q
hr : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : FormallyUnramified R (Localization.Away r)
this : IsUnramifiedAt R (Ideal.under (↥S') Q)
f : ↥S'
hfQ : f ∉ Ideal.under (↥S') Q
hf : HasStandardEtaleSurjectionOn R f
e : Localization.Away (r * f) ≃ₐ[R] Localization.Away (↑r * ↑f) :=
  AlgEquiv.ofBijective (Localization.awayMapₐ S'.val (r * f)) ⋯
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨P, φ, hφ⟩ := hf.of_dvd (g := r * f) (by simp)

Goal state after:
R✝ : Type u_1
S✝ : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrQ : ↑r ∉ Q
hr : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : FormallyUnramified R (Localization.Away r)
this : IsUnramifiedAt R (Ideal.under (↥S') Q)
f : ↥S'
hfQ : f ∉ Ideal.under (↥S') Q
hf : HasStandardEtaleSurjectionOn R f
e : Localization.Away (r * f) ≃ₐ[R] Localization.Away (↑r * ↑f) :=
  AlgEquiv.ofBijective (Localization.awayMapₐ S'.val (r * f)) ⋯
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away (r * f)
hφ : Function.Surjective ⇑φ
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑f /ₘ X ^ m = ↑((addLinearEquiv R m n) f).2 ∧ ↑f %ₘ X ^ m = ↑((addLinearEquiv R m n) f).1

Tactic:
refine div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩

Goal state after:
case refine_1
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑((addLinearEquiv R m n) f).1 + X ^ m * ↑((addLinearEquiv R m n) f).2 = ↑f

case refine_2
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ (↑((addLinearEquiv R m n) f).1).degree < (X ^ m).degree
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Submodule.map (↑↑(taylorEquiv r)) R[X]_n = R[X]_n

Tactic:
nth_rw 1 [← comap_taylorEquiv_degreeLT (r := r), Submodule.map_comap_eq_of_surjective]

Goal state after:
case hf
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Function.Surjective ⇑↑↑(taylorEquiv r)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
hfp : f ∉ Ideal.map C (Ideal.under R p)
⊢ ∃ x, (algebraMap R S) (f.coeff x) ∉ p

Tactic:
simpa [Ideal.mem_map_C_iff] using! hfp

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
⊢ x ∈ ↑s → x ∈ ↑(R'.saturation (p.primeCompl ⊓ R'.toSubmonoid) ⋯)

Tactic:
hx

Goal state after:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(R'.saturation (p.primeCompl ⊓ R'.toSubmonoid) ⋯)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case hg
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsAffineHom f
⊢ IsSeparated (fromNormalization f)

pp: case hfg
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsAffineHom f
⊢ IsAffineHom (toNormalization f ≫ fromNormalization f)

Tactic:
· infer_instance

Goal state after:
case hfg
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsAffineHom f
⊢ IsAffineHom (toNormalization f ≫ fromNormalization f)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : ZariskisMainProperty R (Ideal.under (↥R') p)
x : S
⊢ x ∈ ↑s → x ∈ ↑(R'.saturation (Submonoid.powers r) ⋯)

Tactic:
hx

Goal state after:
case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : ZariskisMainProperty R (Ideal.under (↥R') p)
x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(R'.saturation (Submonoid.powers r) ⋯)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case hg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (fromNormalization f)

pp: case hfg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ QuasiCompact (toNormalization f ≫ fromNormalization f)

Tactic:
· infer_instance

Goal state after:
case hfg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ QuasiCompact (toNormalization f ≫ fromNormalization f)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
x : S
⊢ x ∈ ↑s →
    x ∈
      ↑(Subalgebra.comap (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r')))
          (Localization.awayMapₐ (adjoin R t).val r').range)

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
x : S
hx : x ∈ ↑s
⊢ x ∈
    ↑(Subalgebra.comap (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r')))
        (Localization.awayMapₐ (adjoin R t).val r').range)