awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
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] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
    (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
⊢ {x} ⊆ (↑(integralClosure R S) : Set S) ∪ {x}

Tactic:
simp
-- 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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
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] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
    (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
⊢ LE.le (α := Subalgebra R S) R[x] (adjoin R ((↑(integralClosure R S) : Set S) ∪ {x}))

Tactic:
exact Algebra.adjoin_mono (by simp)

Premises used: Algebra.adjoin_mono
-- 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) ⊥
rwa : Eq (α := Subalgebra R S) (AlgHom.range (aeval x)) ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : Eq (α := Subalgebra R S) R[x] ⊤
⊢ Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)

Tactic:
rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_singleton_eq_range_aeval]

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top
-- 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) ⊥
⊢ Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)

Tactic:
have H₀ : Function.Surjective (aeval (R := R) x) := by
    rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_singleton_eq_range_aeval]
-- 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)
have :
  ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S))
    (hfp : f ∉ Ideal.map (F := R →+* R[X]) C (Ideal.under R p)), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
have ⟨f, (hf : aeval x f = 0), hfp⟩ := SetLike.not_le_iff_exists.mp
    (Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt _ H₀ p)
-- 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)
hfp : f ∉ Ideal.map (F := R →+* R[X]) C (Ideal.under R p)
⊢ ∃ (x : ℕ), ((algebraMap R S : (a : R) → S) (f.coeff x) : S) ∉ p

Tactic:
simpa [Ideal.mem_map_C_iff] using hfp

Premises used: Ideal.mem_map_C_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)
hfp : f ∉ Ideal.map (F := R →+* R[X]) C (Ideal.under R p)
obtain : ∀ (n : ℕ) (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain ⟨n, hfn⟩ : ∃ x, algebraMap R S (f.coeff x) ∉ p := by simpa [Ideal.mem_map_C_iff] using hfp
-- 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)
m : ℕ
IH :
  ∀ m_1 < m,
    ∀ (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
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
h :
  ∀
    (IH :
      ∀ m < 0,
        ∀ (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), ZariskisMainProperty R p)
    (hm : f.natDegree = 0), ZariskisMainProperty R p
h₁ :
  ∀ (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), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain (_ | m) := m
-- 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
IH :
  ∀ m < 0,
    ∀ (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), ZariskisMainProperty R p
hm : f.natDegree = 0
h :
  ∀ (r : R) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) ((C : (a : R) → R[X]) r : R[X]) : S) (0 : S))
    (hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) n) : S) ∉ p)
    (hm : natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) = 0), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp hm

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, 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)
n : ℕ
IH :
  ∀ m < 0,
    ∀ (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), ZariskisMainProperty R p
r : R
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) ((C : (a : R) → R[X]) r : R[X]) : S) (0 : S)
hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) n) : S) ∉ p
hm : natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) = 0
h : ∀ (hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) 0) : S) ∉ p), ZariskisMainProperty R p
h₁ :
  ∀ (n : ℕ) (hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) (n + 1)) : S) ∉ p),
    ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
cases n
-- 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)
IH :
  ∀ m < 0,
    ∀ (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), ZariskisMainProperty R p
r : R
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) ((C : (a : R) → R[X]) r : R[X]) : S) (0 : S)
hm : natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) = 0
hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) 0) : S) ∉ p
⊢ ZariskisMainProperty R p

Tactic:
aesop
-- 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)
IH :
  ∀ m < 0,
    ∀ (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), ZariskisMainProperty R p
r : R
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) ((C : (a : R) → R[X]) r : R[X]) : S) (0 : S)
hm : natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) = 0
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) (n + 1)) : S) ∉ p
⊢ ZariskisMainProperty R p

Tactic:
aesop
-- 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
pos : ∀ (Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)), ZariskisMainProperty R p
neg : ∀ (Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
by_cases Hfp : algebraMap _ _ f.leadingCoeff ∈ p

Premises used: Algebra.algebraMap, Polynomial.leadingCoeff, DFunLike.coe
-- 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)
pos : ∀ (a : R) (ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain ⟨a, ha⟩ := H.le (isIntegral_leadingCoeff_smul f x hf)

Premises used: Eq.le, 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
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
⊢ ZariskisMainProperty R p

Tactic:
IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_

Premises used: Polynomial.C, HMul.hMul, Polynomial.eraseLead, HPow.hPow, HAdd.hAdd, Polynomial.X, DFunLike.coe, 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 : 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 :
  (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1
pos₁ :
  Eq (α := S)
    ((aeval x : (a : R[X]) → S)
        (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
      S)
    (0 : S)
pos₂ :
  ((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
⊢ ZariskisMainProperty R p

Tactic:
refine IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_

Premises used: Polynomial.C, HMul.hMul, Polynomial.eraseLead, HPow.hPow, HAdd.hAdd, Polynomial.X, DFunLike.coe, 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 : 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 : f.eraseLead.natDegree ≤ m
hbc : max f.eraseLead.natDegree (0 + m * 1) < m + 1
hbc₁ : max f.eraseLead.natDegree m < m + 1
⊢ (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1

Tactic:
compute_degree!
-- 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 : f.eraseLead.natDegree ≤ m
⊢ (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1

Tactic:
suffices f.eraseLead.natDegree ≤ m by compute_degree!
-- 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
⊢ f.natDegree - 1 ≤ m

Tactic:
lia
-- 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
⊢ f.eraseLead.natDegree ≤ m

Tactic:
exact (eraseLead_natDegree_le ..).trans (by lia)

Premises used: Polynomial.eraseLead_natDegree_le, LE.le.trans
-- 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
⊢ Eq (α := S)
    ((aeval x : (a : R[X]) → S)
        (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
      S)
    (0 : S)

Tactic:
simp [← self_sub_monomial_natDegree_leadingCoeff, hf, hm, pow_succ', ← Algebra.smul_def,
        ← Algebra.smul_mul_assoc, ← ha]

Premises used: Polynomial.self_sub_monomial_natDegree_leadingCoeff, Algebra.smul_mul_assoc, Algebra.smul_def, pow_succ'
-- 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
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) (f.coeff f.natDegree) : S)

Tactic:
simpa