awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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 R (p.coeff i)
have this : 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]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
⊢ IsAlmostIntegral R (p.coeff i)
have induction : ∀ (x : ℕ) (hn : p.natDegree = x), 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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 : ℕ
⊢ IsIntegral R (p.coeff i)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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
⊢ IsIntegral R (p.coeff i)
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
⊢ IsIntegral R (p.coeff i)
have inl : ∀ (hp : IsIntegral.{u_1, u_2} R[X] (A := S[X]) 0), IsIntegral.{u_1, u_2} R (A := S) (coeff 0 i)
Tactic: obtain rfl | hp0 := eq_or_ne p 0
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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)
⊢ IsIntegral R (p.coeff i)
have inr : ∀ (hp0 : p ≠ 0), IsIntegral R (p.coeff i)
Tactic: obtain rfl | hp0 := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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 : ℕ
⊢ (q.coeff i).natDegree < m
have pos : ∀ (hi : i ∈ q.support), (q.coeff i).natDegree < m
Tactic: by_cases hi : i ∈ q.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
⊢ (q.coeff i).natDegree < m
have neg : ∀ (hi : i ∉ q.support), (q.coeff i).natDegree < m
Tactic: by_cases hi : i ∈ q.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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
⊢ IsIntegral R (p.coeff i)
have hm₁ : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
have 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
Tactic: rw [eval_eq_sum_range, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
⊢ (∑ 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
have 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
Tactic: refine .add_of_right (by simp [q, minpoly.monic hp, ← pow_mul]) (degree_lt_degree ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
⊢ 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
have refine : 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 lt_of_lt_of_eq (b := m * q.natDegree) ?_ (by simp [q, minpoly.monic hp, ← pow_mul])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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
⊢ natDegree.{u_1} (R := R) (∑ x ∈ Finset.range q.natDegree, q.coeff x * HPow.hPow (α := R[X]) X m ^ x) < m * q.natDegree
have 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
Tactic: refine (natDegree_sum_le ..).trans_lt ((Finset.fold_max_lt _).mpr
      ⟨by simpa using ⟨by lia, minpoly.natDegree_pos hp⟩, fun i hi ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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
⊢ (q.coeff i * HPow.hPow (α := R[X]) X m ^ i).natDegree < m * q.natDegree
have hi₁ : i < q.natDegree
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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 * HPow.hPow (α := R[X]) X m ^ i).natDegree < m * q.natDegree
have grw : (q.coeff i).natDegree + m * i < m * (i + 1)
Tactic: grw [← pow_mul, natDegree_mul_le, natDegree_X_pow, ← Nat.add_one_le_iff.mpr hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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 * i < m * (i + 1)
have this : (q.coeff i).natDegree < m
Tactic: have := hm₁ i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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
⊢ IsIntegral R (p.coeff i)
have hm₁' : (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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
⊢ IsIntegral R (p.coeff i)
have hm₂ : p.natDegree < m
Tactic: have hm₂ : p.natDegree < m := by grind
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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
⊢ IsIntegral R (p.coeff i)
have h₀ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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])
⊢ IsIntegral R (p.coeff i)
have this : 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: have : (((taylor (X ^ m)) q).map (algebraMap R[X] S[X])).IsRoot (p - X ^ m) := by
    simpa [-algebraMap_def, q, h₀] using
      ((q.map (algebraMap _ _)).taylor_eval (X ^ m) (p - X ^ m) :)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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])
this :
  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)
⊢ HPow.hPow (α := S[X]) X m - p ∣ (Algebra.ofId R[X] S[X] : (a : R[X]) → S[X]) (eval (HPow.hPow (α := R[X]) X m) q)
have rw : p - HPow.hPow (α := S[X]) X m ∣
  ((aeval ((Algebra.ofId R[X] S[X] : (a : R[X]) → S[X]) (HPow.hPow (α := R[X]) X m)) :
        AlgHom.{u_1, u_1, u_2} R[X] R[X][X] S[X]) :
      (a : R[X][X]) → S[X])
    q
Tactic: rw [← coe_aeval_eq_eval, ← aeval_algHom_apply, ← neg_dvd, neg_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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])
this :
  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)
⊢ IsIntegral R (p.coeff i)
have this₁ : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
Tactic: have : X ^ m - p ∣ (eval (X ^ m) q).map (algebraMap _ _) := by
    change X ^ m - p ∣ Algebra.ofId R[X] S[X] _
    rw [← coe_aeval_eq_eval, ← aeval_algHom_apply, ← neg_dvd, neg_sub]
    simpa [Polynomial.taylor_coeff_zero, -algebraMap_def, h₀] using this.dvd_coeff_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
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])
this_1 :
  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)
this : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
⊢ IsIntegral R (p.coeff i)
have this₁ : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
Tactic: have := (isIntegral_coeff_of_dvd _ _ hm₁'
    ((monic_X_pow _).sub_of_left (by simpa [← natDegree_lt_iff_degree_lt, hp0])) this i).neg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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])
this_1 :
  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)
this_2 : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
this : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
⊢ IsIntegral R (p.coeff i)
have inr : ∀ (hi : i ≤ p.natDegree), IsIntegral R (p.coeff i)
Tactic: obtain hi | hi := le_or_gt i p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
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])
this_1 :
  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)
this_2 : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
this : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
inr : ∀ (hi : i ≤ p.natDegree), IsIntegral R (p.coeff i)
⊢ IsIntegral R (p.coeff i)
have inr₁ : ∀ (hi : p.natDegree < i), IsIntegral R (p.coeff i)
Tactic: obtain hi | hi := le_or_gt i p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
⊢ IsIntegral.{u_1, u_2} R[X] f ↔ ∀ (n : ℕ), IsIntegral R (f.coeff n)
have refine : ∀ (H : ∀ (n : ℕ), IsIntegral R (f.coeff n)), IsIntegral.{u_1, u_2} R[X] f
Tactic: refine ⟨IsIntegral.coeff, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
H : ∀ (n : ℕ), IsIntegral R (f.coeff n)
⊢ IsIntegral.{u_1, u_2} R[X] f
have rw : IsIntegral.{u_1, u_2} R[X] (A := S[X]) (∑ n ∈ f.support, (monomial n : (a : S) → S[X]) (f.coeff n))
Tactic: rw [← f.sum_monomial_eq, Polynomial.sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
H : ∀ (n : ℕ), IsIntegral R (f.coeff n)
⊢ IsIntegral.{u_1, u_2} R[X] (A := S[X]) (∑ n ∈ f.support, (monomial n : (a : S) → S[X]) (f.coeff n))
have simp : IsIntegral.{u_1, u_2} R[X] (A := S[X])
  (∑ x ∈ f.support,
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (f.coeff x) : S[X]) (HPow.hPow (α := S[X]) (map (algebraMap R S) X) x))
Tactic: simp only [← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p : A[X]
monic : p.Monic
deg : p.natDegree ≠ 0
hx : IsIntegral R (eval x p)
hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)
⊢ IsIntegral R x
have obtain : ∀ (q : (↥(integralClosure R A))[X]) (hqp : Polynomial.map (algebraMap (↥(integralClosure R A)) A) q = p)
  (hdeg : q.natDegree = p.natDegree) (hq : q.Monic), IsIntegral R x
Tactic: obtain ⟨q, hqp, hdeg, hq⟩ :=
    lifts_and_natDegree_eq_and_monic (p := p) (f := algebraMap (integralClosure R A) _)
    (p.lifts_iff_coeff_lifts.mpr (by simpa)) monic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
⊢ IsIntegrallyClosed.{u_4} R[X]
have this : IsIntegrallyClosed.{u_4} K[X]
Tactic: have : IsIntegrallyClosed K[X] := UniqueFactorizationMonoid.instIsIntegrallyClosed
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
⊢ IsIntegrallyClosed.{u_4} R[X]
have suffices : IsIntegrallyClosedIn.{u_4, u_4} R[X] K[X]
Tactic: suffices IsIntegrallyClosedIn R[X] K[X] from .of_isIntegrallyClosed_of_isIntegrallyClosedIn _ K[X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
⊢ IsIntegrallyClosedIn.{u_4, u_4} R[X] K[X]
have refine : ∀ {x : K[X]}, IsIntegral R[X] x → ∃ (y : R[X]), (algebraMap R[X] K[X] : (a : R[X]) → K[X]) y = x
Tactic: refine isIntegrallyClosedIn_iff.mpr ⟨map_injective _ (IsFractionRing.injective _ _), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
⊢ ∀ {x : K[X]}, IsIntegral R[X] x → ∃ (y : R[X]), (algebraMap R[X] K[X] : (a : R[X]) → K[X]) y = x
have refine : ∀ {p : K[X]} (hp : IsIntegral R[X] p) (n : ℕ),
  Membership.mem (γ := Set K) (Set.range (ι := R) (⇑(algebraMap R K) : (a : R) → K)) (p.coeff n)
Tactic: refine fun {p} hp ↦ (lifts_iff_coeff_lifts _).mpr fun n ↦ ?_