awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • p.leadingCoeff ^ n)
refine :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
      (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
        (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))
⊢ Membership.mem (α := S[X]) (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
    ((C : (a : S) → S[X]) p.leadingCoeff : S[X])

Tactic:
refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n_1 : ℕ
IH :
  ∀ m < n_1,
    ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n_1
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • p.leadingCoeff ^ n)
n : ℕ
obtain :
  ∀ (s : R) (hs : ((algebraMap R S : R →+* S) : (a : R) → S) s = r • p.leadingCoeff ^ n),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
      (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
        (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))
⊢ Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
    (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))

Tactic:
obtain ⟨s, hs⟩ := hr' n
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n_1 : ℕ
IH :
  ∀ m < n_1,
    ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n_1
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • p.leadingCoeff ^ n)
n : ℕ
s : R
hs : ((algebraMap R S : R →+* S) : (a : R) → S) s = r • p.leadingCoeff ^ n
⊢ (algebraMap R[X] S[X] : (a : R[X]) → S[X]) ((C : (a : R) → R[X]) s) =
    HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n)

Tactic:
simp [Algebra.smul_def, hs]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n_1 : ℕ
IH :
  ∀ m < n_1,
    ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n_1
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • p.leadingCoeff ^ n)
n : ℕ
s : R
hs : ((algebraMap R S : R →+* S) : (a : R) → S) s = r • p.leadingCoeff ^ n
⊢ Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
    (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))

Tactic:
exact ⟨C s, by simp [Algebra.smul_def, hs]⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ IsAlmostIntegral.{u_1, u_2} R[X] p.eraseLead

Tactic:
have : IsAlmostIntegral R[X] p.eraseLead := by
    rw [← self_sub_monomial_natDegree_leadingCoeff, ← mem_completeIntegralClosure,
      ← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S), ← Polynomial.map_pow]
    refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))
    obtain ⟨r, hr, hr'⟩ := H hp
    refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩
    obtain ⟨s, hs⟩ := hr' n
    exact ⟨C s, by simp [Algebra.smul_def, hs]⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
this : IsAlmostIntegral.{u_1, u_2} R[X] p.eraseLead
⊢ p.natDegree - 1 < n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
this : IsAlmostIntegral.{u_1, u_2} R[X] p.eraseLead
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
simpa [hi, eraseLead_coeff_of_ne] using
    IH (p := p.eraseLead) _ (p.eraseLead_natDegree_le.trans_lt (by lia)) this rfl

Premises used: Polynomial.eraseLead_natDegree_le, Polynomial.eraseLead_coeff_of_ne, LE.le.trans_lt, rfl
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
induction : ∀ (x : ℕ) (hn : p.natDegree = x), IsAlmostIntegral R (p.coeff i)
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
induction hn : p.natDegree using Nat.strong_induction_on generalizing p with | h n IH =>
  by_cases hp' : p.natDegree = 0
  · obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'
    simp only [coeff_C]
    split_ifs with h
    · simpa using H hp
    · exact (completeIntegralClosure R S).zero_mem
  by_cases hi : i = p.natDegree
  · simp [hi, H hp]
  have : IsAlmostIntegral R[X] p.eraseLead := by
    rw [← self_sub_monomial_natDegree_leadingCoeff, ← mem_completeIntegralClosure,
      ← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S), ← Polynomial.map_pow]
    refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))
    obtain ⟨r, hr, hr'⟩ := H hp
    refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩
    obtain ⟨s, hs⟩ := hr' n
    exact ⟨C s, by simp [Algebra.smul_def, hs]⟩
  simpa [hi, eraseLead_coeff_of_ne] using
    IH (p := p.eraseLead) _ (p.eraseLead_natDegree_le.trans_lt (by lia)) this rfl

Premises used: Subalgebra.zero_mem, Polynomial.coeff_C, Polynomial.natDegree, Polynomial.eraseLead_coeff_of_ne, completeIntegralClosure, rfl
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
inl : ∀ (hp : IsIntegral.{u_1, u_2} R[X] (A := S[X]) 0), IsIntegral.{u_1, u_2} R (A := S) (coeff 0 i)
inr : ∀ (hp0 : p ≠ 0), IsIntegral R (p.coeff i)
⊢ IsIntegral R (p.coeff i)

Tactic:
obtain rfl | hp0 := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp : IsIntegral.{u_1, u_2} R[X] (A := S[X]) 0
⊢ IsIntegral.{u_1, u_2} R (A := S) (coeff 0 i)

Tactic:
simp [isIntegral_zero]

Premises used: isIntegral_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
pos : ∀ (hi : i ∈ q.support), (q.coeff i).natDegree < m
neg : ∀ (hi : i ∉ q.support), (q.coeff i).natDegree < m
⊢ (q.coeff i).natDegree < m

Tactic:
by_cases hi : i ∈ q.support

Premises used: Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∈ q.support
⊢ (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) < m

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∈ q.support
⊢ (q.coeff i).natDegree < m

Tactic:
exact (Finset.le_sup (f := fun i ↦ (q.coeff i).natDegree) hi).trans_lt (by lia)

Premises used: LE.le.trans_lt, Finset.le_sup
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree < m

Tactic:
simp_all [m]
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
⊢ ∀ (i : ℕ), (q.coeff i).natDegree < m

Tactic:
have hm₁ (i) : (q.coeff i).natDegree < m := by
    by_cases hi : i ∈ q.support
    · exact (Finset.le_sup (f := fun i ↦ (q.coeff i).natDegree) hi).trans_lt (by lia)
    · simp_all [m]
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
rw :
  (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x +
      q.coeff q.natDegree * HPow.hPow (α := R[X]) X m ^ q.natDegree).Monic
⊢ (eval (HPow.hPow (α := R[X]) X m) q).Monic

Tactic:
rw [eval_eq_sum_range, Finset.sum_range_succ]

Premises used: Polynomial.eval_eq_sum_range, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ (q.coeff q.natDegree * HPow.hPow (α := R[X]) X m ^ q.natDegree).Monic

Tactic:
simp [q, minpoly.monic hp, ← pow_mul]

Premises used: minpoly.monic, pow_mul
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
refine :
  natDegree.{u_1} (R := R) (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x) <
    (q.coeff q.natDegree * HPow.hPow (α := R[X]) X m ^ q.natDegree).natDegree
⊢ (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x +
      q.coeff q.natDegree * HPow.hPow (α := R[X]) X m ^ q.natDegree).Monic

Tactic:
refine .add_of_right (by simp [q, minpoly.monic hp, ← pow_mul]) (degree_lt_degree ?_)
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ m * q.natDegree = (q.coeff q.natDegree * HPow.hPow (α := R[X]) X m ^ q.natDegree).natDegree

Tactic:
simp [q, minpoly.monic hp, ← pow_mul]

Premises used: minpoly.monic, pow_mul
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
refine :
  natDegree.{u_1} (R := R) (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x) < m * q.natDegree
⊢ natDegree.{u_1} (R := R) (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x) <
    (q.coeff q.natDegree * HPow.hPow (α := R[X]) X m ^ q.natDegree).natDegree

Tactic:
refine lt_of_lt_of_eq (b := m * q.natDegree) ?_ (by simp [q, minpoly.monic hp, ← pow_mul])

Premises used: lt_of_lt_of_eq
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ 0 < m

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ 0 < m * q.natDegree

Tactic:
simpa using ⟨by lia, minpoly.natDegree_pos hp⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
refine :
  ∀ (i : ℕ) (hi : i ∈ Finset.range q.natDegree),
    Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree (fun (x : ℕ) ↦ q.coeff x * HPow.hPow (α := R[X]) X m ^ x) i <
      m * q.natDegree
⊢ natDegree.{u_1} (R := R) (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x) < m * q.natDegree

Tactic:
refine (natDegree_sum_le ..).trans_lt ((Finset.fold_max_lt _).mpr
      ⟨by simpa using ⟨by lia, minpoly.natDegree_pos hp⟩, fun i hi ↦ ?_⟩)

Premises used: Iff.mpr, Polynomial.natDegree_sum_le, And.intro, Finset.fold_max_lt, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
i : ℕ
hi : i ∈ Finset.range q.natDegree
⊢ i < q.natDegree

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
i : ℕ
hi : i < q.natDegree
grw : (q.coeff i).natDegree + m * i < m * (i + 1)
⊢ (q.coeff i * HPow.hPow (α := R[X]) X m ^ i).natDegree < m * q.natDegree

Tactic:
grw [← pow_mul, natDegree_mul_le, natDegree_X_pow, ← Nat.add_one_le_iff.mpr hi]

Premises used: Iff.mpr, pow_mul, Polynomial.natDegree_X_pow, Nat.add_one_le_iff, Polynomial.natDegree_mul_le
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
i : ℕ
hi : i < q.natDegree
⊢ (q.coeff i).natDegree < m

Tactic:
have := hm₁ i
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i_1 : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
i : ℕ
hi : i < q.natDegree
this : (q.coeff i).natDegree < m
⊢ (q.coeff i).natDegree + m * i < m * (i + 1)

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ (eval (HPow.hPow (α := R[X]) X m) q).Monic

Tactic:
have hm₁' : (q.eval (X ^ m)).Monic := by
    rw [eval_eq_sum_range, Finset.sum_range_succ]
    refine .add_of_right (by simp [q, minpoly.monic hp, ← pow_mul]) (degree_lt_degree ?_)
    refine lt_of_lt_of_eq (b := m * q.natDegree) ?_ (by simp [q, minpoly.monic hp, ← pow_mul])
    refine (natDegree_sum_le ..).trans_lt ((Finset.fold_max_lt _).mpr
      ⟨by simpa using ⟨by lia, minpoly.natDegree_pos hp⟩, fun i hi ↦ ?_⟩)
    dsimp
    simp only [Finset.mem_range] at hi
    grw [← pow_mul, natDegree_mul_le, natDegree_X_pow, ← Nat.add_one_le_iff.mpr hi]
    have := hm₁ i
    lia
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
⊢ p.natDegree < m

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
⊢ p.natDegree < m

Tactic:
have hm₂ : p.natDegree < m := by grind
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
⊢ Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
⊢ Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])

Tactic:
have h₀ : algebraMap R[X] S[X] X = X := by simp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
⊢ IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)

Tactic:
simpa [-algebraMap_def, q, h₀] using
      ((q.map (algebraMap _ _)).taylor_eval (X ^ m) (p - X ^ m) :)

Premises used: Polynomial.taylor_eval, Algebra.algebraMap, Polynomial.algebraMap_def, HSub.hSub, HPow.hPow, Polynomial.map, Polynomial.X