mathlib-initiative/mathlib-tactics huggingface dataset:
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]
ht : φ.IsIntegralElem t
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]
hq : IsIntegral R' ((algebraMap S S') t - (aeval ((algebraMap S S') (φ X))) q)
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = (fun x ↦ a ^ x) n • q
this : (algebraMap S S') (φ q') = (algebraMap R S') a ^ n * (aeval ((algebraMap S S') (φ X))) q
⊢ IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q'))

Tactic:
simpa using

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]
ht : φ.IsIntegralElem t
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]
hq : IsIntegral R' ((algebraMap S S') t - (aeval ((algebraMap S S') (φ X))) q)
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = (fun x ↦ a ^ x) n • q
this : (algebraMap S S') (φ q') = (algebraMap R S') a ^ n * (aeval ((algebraMap S S') (φ X))) q
⊢ IsIntegral R' ((algebraMap R S') a ^ n * ((algebraMap S S') t - (aeval ((algebraMap S S') (φ X))) q))
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
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := ⋯
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := ⋯
this✝³ : SMul p.ResidueField (p.Fiber S) := ⋯
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := ⋯
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := ⋯
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := ⋯
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
Q' : Ideal S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under R Q)
H✝ : Q' ≠ Q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime Q') := ⋯
hsQ'' : (algebraMap R Q'.ResidueField) s ≠ 0
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField := ⋯
H : φ' r = 0
⊢ φ' (1 ⊗ₜ[R] t) = 0

Tactic:
simpa using

Goal state after:
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✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := ⋯
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := ⋯
this✝³ : SMul p.ResidueField (p.Fiber S) := ⋯
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := ⋯
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := ⋯
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := ⋯
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
Q' : Ideal S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under R Q)
H✝ : Q' ≠ Q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime Q') := ⋯
hsQ'' : (algebraMap R Q'.ResidueField) s ≠ 0
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField := ⋯
H : φ' r = 0
⊢ φ' (1 ⊗ₜ[R] t) = 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
x : S
⊢ φ p * t * x ∈ φ.range

Tactic:
simpa using

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
x : S
⊢ ∃ x_1, φ x_1 = φ p * t * x
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case add
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 : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x y : S
hx✝ : x ∈ Submodule.span R[X] ↑s
hy✝ : y ∈ Submodule.span R[X] ↑s
hx : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
hy : p.leadingCoeff ^ s.sup n • (t * y) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * (x + y)) ∈ φ.range

Tactic:
simpa using

Goal state after:
case add
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 : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x y : S
hx✝ : x ∈ Submodule.span R[X] ↑s
hy✝ : y ∈ Submodule.span R[X] ↑s
hx : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
hy : p.leadingCoeff ^ s.sup n • (t * y) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * x) + p.leadingCoeff ^ s.sup n • (t * y) ∈ φ.range
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.h.zero.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
IH :
  ∀ m < 0,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = 0
hi' : i ≤ p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
simpa using

Goal state after:
case inr.h.zero.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
IH :
  ∀ m < 0,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = 0
hi' : i ≤ p.natDegree
⊢ p.coeff 0 • t ∈ (conductor R (φ X)).radical
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.h.succ.inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i = p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
simpa using

Goal state after:
case inr.h.succ.inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i = p.natDegree
⊢ p.leadingCoeff • t ∈ (conductor R (φ X)).radical
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.h.succ.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this✝ : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
this : φ p.eraseLead * t ∈ (conductor R (φ X)).radical
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
simpa using

Goal state after:
case inr.h.succ.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this✝ : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
this : φ p.eraseLead * t ∈ (conductor R (φ X)).radical
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical
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
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn : (φ p * t) ^ n ∈ conductor R (φ X)
⊢ φ (p ^ n) * t ^ n ∈ conductor R (φ X)

Tactic:
simpa using

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
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn : (φ p * t) ^ n ∈ conductor R (φ X)
⊢ φ p ^ n * t ^ n ∈ conductor R (φ X)
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
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval x) p * u ∈ (conductor R x).radical
i : ℕ
⊢ (map (algebraMap R (S ⧸ (conductor R x).radical)) p * C ((Ideal.Quotient.mk (conductor R x).radical) u)).coeff i =
    coeff 0 i

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval x) p * u ∈ (conductor R x).radical
i : ℕ
⊢ (algebraMap R S) (p.coeff i) * u ∈ (conductor R x).radical
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
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval x) p * u ∈ (conductor R x).radical
i : ℕ
⊢ (aeval x) p * u ∈ (conductor R ((aeval x) X)).radical

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval x) p * u ∈ (conductor R x).radical
i : ℕ
⊢ (aeval x) p * u ∈ (conductor R x).radical
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case inr.refine_1
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
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H✝ : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ s * f ∉ Q

Tactic:
simpa using

Goal state after:
case inr.refine_1
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
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H✝ : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ f ∉ Q
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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (algebraMap S (Localization.Away f)) p
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
⊢ g ∉ p

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (algebraMap S (Localization.Away f)) p
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
⊢ g ∉ p
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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
by
  obtain ⟨f, hfp, H⟩ := IsSmoothAt.exists_notMem_isStandardSmooth R p
  obtain ⟨n, φ, hgC, hg⟩ := RingHom.IsStandardSmooth.exists_etale_mvPolynomial
    (f := algebraMap R (Localization.Away f)) (by simpa [RingHom.isStandardSmooth_algebraMap])
  algebraize [φ]
  have := IsScalarTower.of_algebraMap_eq' hgC.symm
  have : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_›
      ((Ideal.disjoint_powers_iff_notMem_of_isPrime _).mpr hfp)
  obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))
  obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀
  replace hg : g ∉ p := by simpa [Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem,
    IsLocalization.mk'_mem_map_algebraMap_iff, mt (‹p.IsPrime›.mem_of_pow_mem _) hfp,
    ← hg₀] using hg
  have : IsLocalization.Away (f * g) (Localization.Away g₀) := by
    suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
    refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩
    simp only [← hg₀, IsUnit.unit_spec, ← map_pow, mul_comm, IsLocalization.mk'_spec'_mk]
  let e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
    IsLocalization.algEquiv (.powers (f * g)) _ _
  let : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
    (e.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) _)).toAlgebra
  have : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g)) := by
    refine .of_algebraMap_eq' ?_
    simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
    exact (e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm
  let e' : Localization.Away g₀ ≃ₐ[MvPolynomial (Fin n) R] Localization.Away (f * g) :=
    { __ := e, commutes' r := rfl }
  exact ⟨f * g, ‹p.IsPrime›.mul_notMem ‹_› ‹_›, n, ‹_›, ‹_›, .of_equiv e'⟩

Goal state after:
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✝² : IsReduced S
x✝ : S
hx' : (aeval x✝).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
x : S
⊢ (IsScalarTower.toAlgHom R S L) x ∈ Subalgebra.restrictScalars R S'

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x✝ : S
hx' : (aeval x✝).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
x : S
⊢ (algebraMap S L) x ∈ S'
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ LinearMap.det ↑(taylorLinearEquiv r n) = 1

Tactic:
rw [← LinearMap.det_toMatrix (degreeLT.basis R n),
    Matrix.det_of_isUpperTriangular, Fintype.prod_eq_one]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ∀ (a : Fin n), (LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) (↑(taylorLinearEquiv r n)) a a = 1

R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) ↑(taylorLinearEquiv r n)).IsUpperTriangular
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✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
y : S
⊢ ↑(g (1 ⊗ₜ[R] y)) = (algebraMap S L) y

Tactic:
simp [g, S']

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
y : S
⊢ ↑(f y) = (algebraMap S L) y
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
m n : ℕ
i j : Fin (m + n)
⊢ f.sylvester g m n i j =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m) i j

Tactic:
induction j using Fin.addCases <;> simp [sylvester]

Goal state after:
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
⊢ RingHom.ker (Ideal.Quotient.mk J) ≤ p

Tactic:
simpa using

Goal state after:
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
⊢ J ≤ p
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f : R[X]
n m : ℕ
this : ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i ⟨0, ⋯⟩ = 0
⊢ f.resultant 0 (m + 1) n = 0 ^ (m + 1) * f.coeff 0 ^ n

Tactic:
simpa using

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f : R[X]
n m : ℕ
this : ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i ⟨0, ⋯⟩ = 0
⊢ (f.sylvester 0 (m + 1) n).det = 0