awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
inr :
  ∀ (hi' : i = p.natDegree),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
inr₁ :
  ∀ (hi' : i ≠ p.natDegree),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
obtain hi' | hi' := eq_or_ne i p.natDegree

Premises used: eq_or_ne, Polynomial.natDegree
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i = p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
simpa [hi'] using this _ hp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
simp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t -
      p.leadingCoeff • t * HPow.hPow (α := S) ((φ : (a : R[X]) → S) X : S) p.natDegree)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p.eraseLead : S) t)

Tactic:
simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]

Premises used: map_sub, map_pow, sub_mul, map_mul, mul_right_comm, AlgHom.commutes, Algebra.smul_def, Polynomial.self_sub_C_mul_X_pow, Polynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t -
      p.leadingCoeff • t * HPow.hPow (α := S) ((φ : (a : R[X]) → S) X : S) p.natDegree)

Tactic:
sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))

Premises used: Set.Mem, setOf, sub_mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t -
      p.leadingCoeff • t * HPow.hPow (α := S) ((φ : (a : R[X]) → S) X : S) p.natDegree)

Tactic:
exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))

Premises used: sub_mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p.eraseLead : S) t)

Tactic:
have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this_1 :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
this :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p.eraseLead : S) t)
⊢ p.natDegree - 1 < n + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this_1 :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
this :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p.eraseLead : S) t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl

Premises used: Polynomial.eraseLead_natDegree_le, Polynomial.eraseLead_coeff, LE.le.trans_lt, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
n : ℕ
IH :
  ∀ m < n,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
hpn : p.natDegree = n
inr :
  ∀
    (IH :
      ∀ m < 0,
        ∀ (p : R[X])
          (hp :
            Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
              (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
          (hpn : p.natDegree = m),
          Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
            (p.coeff i • t))
    (hpn : p.natDegree = 0),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
inr₁ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n + 1,
        ∀ (p : R[X])
          (hp :
            Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
              (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
          (hpn : p.natDegree = m),
          Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
            (p.coeff i • t))
    (hpn : p.natDegree = n + 1),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl

Premises used: Polynomial.coeff_natDegree, Polynomial.eraseLead_coeff, eq_or_ne, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
inr :
  ∀ (x : ℕ) (hpn : p.natDegree = x),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with
    | h n IH =>
    cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl

Premises used: Polynomial.coeff_natDegree, Polynomial.eraseLead_coeff, eq_or_ne, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
hi : i = p.natDegree
obtain :
  ∀ (n : ℕ)
    (hn :
      Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
obtain ⟨n, hn⟩ := hp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
⊢ Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) (p ^ n) : S) (t ^ n))

Tactic:
simpa [mul_pow] using hn

Premises used: mul_pow
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
obtain :
  ∀ (k : ℕ)
    (hk :
      Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
        ((p ^ n).leadingCoeff ^ k • t ^ n)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
obtain ⟨k, hk⟩ := exists_leadingCoeff_pow_smul_mem_conductor φ (t ^ n) (p ^ n) hRS hφ
    (by simpa [mul_pow] using hn)

Premises used: HPow.hPow, exists_leadingCoeff_pow_smul_mem_conductor
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
pos :
  ∀ (hpn : p.leadingCoeff ^ n = 0),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
neg :
  ∀ (hpn : ¬p.leadingCoeff ^ n = 0),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
by_cases hpn : p.leadingCoeff ^ n = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
hpn : p.leadingCoeff ^ n = 0
h : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p.coeff i • t) ^ n)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
use n
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
hpn : p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p.coeff i • t) ^ n)

Tactic:
simp [_root_.smul_pow, hpn, hi]

Premises used: smul_pow
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)

Tactic:
rw [leadingCoeff_pow' hpn, ← pow_mul] at hk

Premises used: Polynomial.leadingCoeff_pow', pow_mul
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
hk₁ : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
⊢ ¬p.leadingCoeff ^ n = 0

Tactic:
rw [leadingCoeff_pow' hpn, ← pow_mul] at hk

Premises used: Polynomial.leadingCoeff_pow', pow_mul