awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ZariskisMainProperty R p
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ZariskisMainProperty R p
have obtain : ∀ (n : ℕ) (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ 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
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have 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
Tactic: obtain (_ | m) := m
Cleared hypotheses: m, IH, hm
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have 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
Tactic: obtain (_ | m) := m
Cleared hypotheses: m, IH, hm
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have 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
Tactic: obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp hm
Cleared hypotheses: f, hf, hfn, hm
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have h : ∀ (hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) 0) : S) ∉ p), ZariskisMainProperty R p
Tactic: cases n
Cleared hypotheses: n, hfn
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have h₁ : ∀ (n : ℕ) (hfn : ((algebraMap R S : (a : R) → S) (coeff ((C : (a : R) → R[X]) r) (n + 1)) : S) ∉ p),
  ZariskisMainProperty R p
Tactic: cases n
Cleared hypotheses: n, hfn
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have pos : ∀ (Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)), ZariskisMainProperty R p
Tactic: by_cases Hfp : algebraMap _ _ f.leadingCoeff ∈ p
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have neg : ∀ (Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p), ZariskisMainProperty R p
Tactic: by_cases Hfp : algebraMap _ _ f.leadingCoeff ∈ p
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ZariskisMainProperty R p
have pos : ∀ (a : R) (ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x), ZariskisMainProperty R p
Tactic: obtain ⟨a, ha⟩ := H.le (isIntegral_leadingCoeff_smul f x hf)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
have pos : (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1
Tactic: refine IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have 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)
Tactic: refine IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ZariskisMainProperty R p
have 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
Tactic: refine IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1
have hbc : max f.eraseLead.natDegree (0 + m * 1) < m + 1
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ (f.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1
have hbc₁ : max f.eraseLead.natDegree m < m + 1
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)).natDegree < m + 1
have pos : f.eraseLead.natDegree ≤ m
Tactic: suffices f.eraseLead.natDegree ≤ m by compute_degree!
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ((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
have 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
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)]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ 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
have pos : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S)
Tactic: rwa [Ideal.add_mem_iff_left]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S)
have pos : n = m → Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) a : S)
Tactic: split_ifs