awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
hfn : ((algebraMap R S : (a : R) → S) (f.coeff f.natDegree) : S) ∉ p
this :
  HAdd.hAdd (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f.coeff f.natDegree) : S)
      ((algebraMap R S : (a : R) → S) (if f.natDegree = m then a else 0) : S) ∉
    p
⊢ False

Tactic:
exact hfn (by simpa)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
this :
  HAdd.hAdd (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f.coeff n) : S)
      ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S) ∉
    p
⊢ ((algebraMap R S : (a : R) → S)
        ((f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n) :
      S) ∉
    p

Tactic:
simpa [eraseLead_coeff, show n ≠ f.natDegree by rintro rfl; exact hfn (by simpa)]

Premises used: Polynomial.eraseLead_coeff
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
pos :
  HAdd.hAdd (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f.coeff n) : S)
      ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S) ∉
    p
⊢ ((algebraMap R S : (a : R) → S)
        ((f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n) :
      S) ∉
    p

Tactic:
suffices algebraMap R S (f.coeff n) + algebraMap R S (if n = m then a else 0) ∉ p by
        simpa [eraseLead_coeff, show n ≠ f.natDegree by rintro rfl; exact hfn (by simpa)]
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
pos : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S)
⊢ HAdd.hAdd (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f.coeff n) : S)
      ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S) ∉
    p

Tactic:
rwa [Ideal.add_mem_iff_left]

Premises used: Ideal.add_mem_iff_left
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
pos : n = m → Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) a : S)
neg : ¬n = m → Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) 0 : S)
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
h : n = m
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x ∈ p

Tactic:
p.mul_mem_right x Hfp

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
h_1 : n = m
h : (algebraMap R S : (a : R) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) a : S)

Tactic:
convert! p.mul_mem_right x Hfp

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
h : n = m
⊢ (algebraMap R S : (a : R) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x

Tactic:
simpa [Algebra.smul_def] using ha

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
h : ¬n = m
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) 0 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
⊢ ZariskisMainProperty R p

Tactic:
zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩

Premises used: Iff.mpr, isIntegral_algebraMap, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
neg :
  Eq (α := Subalgebra R S)
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯) ⊤
⊢ ZariskisMainProperty R p

Tactic:
refine zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩

Premises used: Iff.mpr, isIntegral_algebraMap, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
neg :
  LE.le (α := Subalgebra R S) R[x]
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯)
⊢ Eq (α := Subalgebra R S)
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯) ⊤

Tactic:
rw [← top_le_iff, ← hx]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
⊢ LE.le (α := Subalgebra R S) R[x]
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯)

Tactic:
Algebra.adjoin_singleton_le ⟨_, ⟨1, rfl⟩, ?_⟩

Premises used: Algebra.adjoin_singleton_le, And.intro, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
neg :
  Membership.mem (γ := Subalgebra R S) (integralClosure R S)
    ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x) 1 * x)
⊢ LE.le (α := Subalgebra R S) R[x]
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯)

Tactic:
refine Algebra.adjoin_singleton_le ⟨_, ⟨1, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
⊢ Membership.mem (γ := Subalgebra R S) (integralClosure R S)
    ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x) 1 * x)

Tactic:
simpa [Algebra.smul_def] using isIntegral_leadingCoeff_smul f x hf

Premises used: Algebra.smul_def, isIntegral_leadingCoeff_smul
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
induction : ∀ (x : ℕ) (hm : f.natDegree = x), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
induction hm : f.natDegree using Nat.strong_induction_on generalizing f n with | h m IH =>
  obtain (_ | m) := m
  · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp hm
    cases n <;> aesop
  by_cases Hfp : algebraMap _ _ f.leadingCoeff ∈ p
  · obtain ⟨a, ha⟩ := H.le (isIntegral_leadingCoeff_smul f x hf)
    refine IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_
    · suffices f.eraseLead.natDegree ≤ m by compute_degree!
      exact (eraseLead_natDegree_le ..).trans (by lia)
    · simp [← self_sub_monomial_natDegree_leadingCoeff, hf, hm, pow_succ', ← Algebra.smul_def,
        ← Algebra.smul_mul_assoc, ← ha]
    · suffices algebraMap R S (f.coeff n) + algebraMap R S (if n = m then a else 0) ∉ p by
        simpa [eraseLead_coeff, show n ≠ f.natDegree by rintro rfl; exact hfn (by simpa)]
      rwa [Ideal.add_mem_iff_left]
      split_ifs
      · convert! p.mul_mem_right x Hfp
        simpa [Algebra.smul_def] using ha
      · simp
  · refine zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩
    rw [← top_le_iff, ← hx]
    refine Algebra.adjoin_singleton_le ⟨_, ⟨1, rfl⟩, ?_⟩
    simpa [Algebra.smul_def] using isIntegral_leadingCoeff_smul f x hf

Premises used: Algebra.algebraMap, Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.eraseLead_natDegree_le, Eq.le, Polynomial.leadingCoeff, Algebra.smul_mul_assoc, top_le_iff, Ideal.add_mem_iff_left, Algebra.smul_def, LE.le.trans, Polynomial.natDegree, DFunLike.coe, isIntegral_leadingCoeff_smul, pow_succ', rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
inr :
  ∀
    (this :
      ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S)
        [inst_7 : p.IsPrime] [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite)
        (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p)
    (H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p
wlog :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
wlog H : integralClosure R S = ⊥

Premises used: integralClosure
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (p : Ideal S) [inst_8 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
⊢ WeaklyQuasiFiniteAt (↥(integralClosure R S)) p

Tactic:
have inst : Algebra.WeaklyQuasiFiniteAt (integralClosure R S) p :=
      .of_restrictScalars R (integralClosure R S) _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ ZariskisMainProperty R p

Tactic:
.restrictScalars (this p (aeval (f X)) ?_ (integralClosure_idem (R := R)))

Premises used: integralClosure_idem, Algebra.ZariskisMainProperty.restrictScalars, Polynomial.aeval, Polynomial.X, DFunLike.coe