awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.coeff p.natDegree ≠ 0

Tactic:
simp [integralNormalization_coeff_natDegree, *]

Premises used: Polynomial.integralNormalization_coeff_natDegree
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
neg : p.integralNormalization.degree ≤ (↑p.natDegree : WithBot ℕ)
⊢ p.integralNormalization.degree = (↑p.natDegree : WithBot ℕ)

Tactic:
refine degree_eq_of_le_of_coeff_ne_zero ?_ (by simp [integralNormalization_coeff_natDegree, *])

Premises used: Polynomial.degree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree ≤ (↑p.natDegree : WithBot ℕ)

Tactic:
(Finset.sup_le fun i h =>
      WithBot.coe_le_coe.2 <| le_natDegree_of_mem_supp i <| support_integralNormalization_subset h)

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Polynomial.degree, Finset.sup_le, WithBot.coe_le_coe, Polynomial.support_integralNormalization_subset, Finset.max
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree ≤ (↑p.natDegree : WithBot ℕ)

Tactic:
exact (Finset.sup_le fun i h =>
      WithBot.coe_le_coe.2 <| le_natDegree_of_mem_supp i <| support_integralNormalization_subset h)

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Finset.sup_le, WithBot.coe_le_coe, Polynomial.support_integralNormalization_subset
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
pos : ∀ (hp : p = 0), p.integralNormalization.natDegree = p.natDegree
neg : ∀ (hp : ¬p = 0), p.integralNormalization.natDegree = p.natDegree
⊢ p.integralNormalization.natDegree = p.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : p = 0
⊢ p.integralNormalization.natDegree = p.natDegree

Tactic:
simp [hp]
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq p.degree_integralNormalization

Premises used: Polynomial.degree_integralNormalization, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.natDegree = p.natDegree

Tactic:
exact natDegree_eq_of_degree_eq p.degree_integralNormalization

Premises used: Polynomial.degree_integralNormalization, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.integralNormalization.Monic

Tactic:
monic_of_degree_le p.natDegree
    (Finset.sup_le fun i h =>
      WithBot.coe_le_coe.2 <| le_natDegree_of_mem_supp i <| support_integralNormalization_subset h)
    (integralNormalization_coeff_natDegree hp)

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Polynomial.integralNormalization_coeff_natDegree, Finset.sup_le, WithBot.coe_le_coe, Polynomial.support_integralNormalization_subset, Polynomial.monic_of_degree_le, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
rw :
  (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
⊢ p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
rw [integralNormalization_coeff]

Premises used: Polynomial.integralNormalization_coeff
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
pos : ∀ (h : p.degree = (↑i : WithBot ℕ)), 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
neg :
  ∀ (h : ¬p.degree = (↑i : WithBot ℕ)),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i =
      p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
⊢ (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : p.degree = (↑i : WithBot ℕ)
⊢ 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp [natDegree_eq_of_degree_eq_some h, leadingCoeff,
      ← pow_succ', tsub_add_cancel_of_le (natDegree_eq_of_degree_eq_some h ▸ hp)]

Premises used: tsub_add_cancel_of_le, Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
neg : p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp only [mul_assoc, ← pow_add]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
pos :
  ∀ (h' : (↑i : WithBot ℕ) < p.degree),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
neg :
  ∀ (h' : ¬(↑i : WithBot ℕ) < p.degree),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
by_cases h' : i < p.degree

Premises used: Polynomial.degree
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
pos : i ≤ p.natDegree - 1
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
rw [tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
pos : i < p.natDegree
⊢ i ≤ p.natDegree - 1

Tactic:
rw [le_tsub_iff_right hp, Nat.succ_le_iff]

Premises used: Nat.succ_le_iff, le_tsub_iff_right
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ i < p.natDegree

Tactic:
coe_lt_degree.mp h'

Premises used: Polynomial.coe_lt_degree, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ i < p.natDegree

Tactic:
exact coe_lt_degree.mp h'

Premises used: Polynomial.coe_lt_degree, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : ¬(↑i : WithBot ℕ) < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

Premises used: le_of_not_gt, lt_of_le_of_ne, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
a :
  ∀ (i : ℕ),
    (HMul.hMul (β := R[X]) p.integralNormalization ((C : (a : R) → R[X]) p.leadingCoeff : R[X])).coeff i =
      (p.scaleRoots p.leadingCoeff).coeff i
⊢ HMul.hMul (β := R[X]) p.integralNormalization ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) =
    p.scaleRoots p.leadingCoeff

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
a :
  (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff =
    (p.scaleRoots p.leadingCoeff).coeff i
⊢ (HMul.hMul (β := R[X]) p.integralNormalization ((C : (a : R) → R[X]) p.leadingCoeff : R[X])).coeff i =
    (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
rw [coeff_mul_C, integralNormalization_coeff]

Premises used: Polynomial.coeff_mul_C, Polynomial.integralNormalization_coeff
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
pos : ∀ (h : p.degree = (↑i : WithBot ℕ)), 1 * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
neg :
  ∀ (h : ¬p.degree = (↑i : WithBot ℕ)),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
⊢ (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff =
    (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : p.degree = (↑i : WithBot ℕ)
⊢ 1 * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
simp [natDegree_eq_of_degree_eq_some h, leadingCoeff]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
neg :
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
simp only [coeff_scaleRoots]

Premises used: Polynomial.coeff_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
pos :
  ∀ (h' : (↑i : WithBot ℕ) < p.degree),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
neg :
  ∀ (h' : ¬(↑i : WithBot ℕ) < p.degree),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)

Tactic:
by_cases h' : i < p.degree

Premises used: Polynomial.degree
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
pos : 1 ≤ p.natDegree - i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)

Tactic:
rw [mul_assoc, ← pow_succ, tsub_right_comm, tsub_add_cancel_of_le]

Premises used: pow_succ, mul_assoc, tsub_right_comm, tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
pos : i < p.natDegree
⊢ 1 ≤ p.natDegree - i

Tactic:
rw [le_tsub_iff_left (coe_lt_degree.mp h').le, Nat.succ_le_iff]

Premises used: Polynomial.coe_lt_degree, LT.lt.le, le_tsub_iff_left, Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ i < p.natDegree

Tactic:
coe_lt_degree.mp h'

Premises used: Polynomial.coe_lt_degree, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ i < p.natDegree

Tactic:
exact coe_lt_degree.mp h'

Premises used: Polynomial.coe_lt_degree, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : ¬(↑i : WithBot ℕ) < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)

Tactic:
simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

Premises used: le_of_not_gt, lt_of_le_of_ne, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
S : Type v
inst : CommSemiring S
p : S[X]
rw :
  HMul.hMul (α := S[X]) ((algebraMap S S[X] : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
rw₁ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
rw₂ :
  HMul.hMul (β := S[X]) p.integralNormalization ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) =
    p.scaleRoots p.leadingCoeff
rw₃ rw₄ : p.scaleRoots p.leadingCoeff = p.scaleRoots p.leadingCoeff
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

Tactic:
rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]

Premises used: mul_comm, Polynomial.integralNormalization_mul_C_leadingCoeff, Algebra.smul_def, Polynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
A : Type u_1
inst_1 : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
rw :
  Eq.{u_1 + 1} (α := A)
    (∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
      HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff i) : A)
        (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ i))
    (∑ i ∈ Finset.range (p.natDegree + 1),
      HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
        HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff i) : A) (x ^ i))
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x) p.integralNormalization =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) * eval₂ f x p

Tactic:
rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]

Premises used: Finset.mul_sum, Polynomial.eval₂_eq_sum_range
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
A : Type u_1
inst_1 : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
h₃ : Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)
a :
  ∀ x_1 ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff x_1) : A)
        (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ x_1) =
      HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
        HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff x_1) : A) (x ^ x_1)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
      HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff i) : A)
        (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ i))
    (∑ i ∈ Finset.range (p.natDegree + 1),
      HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
        HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff i) : A) (x ^ i))

Tactic:
apply Finset.sum_congr

Premises used: Finset.sum_congr
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
A : Type u_1
inst_1 : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
h₃ h₄ : Finset.range (p.natDegree + 1) = Finset.range (p.natDegree + 1)
⊢ Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)

Tactic:
rw [natDegree_eq_of_degree_eq p.degree_integralNormalization]

Premises used: Polynomial.degree_integralNormalization, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : CommSemiring S
h : 1 ≤ p.natDegree
f : R →+* S
x : S
⊢ eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization =
    HPow.hPow (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (p.natDegree - 1) * eval₂ f x p

Tactic:
integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ (.all _ _) (.all _ _)

Premises used: Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute, Commute.all, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
inl :
  ∀ (h : p.natDegree = 0),
    eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
inr :
  ∀ (h : p.natDegree > 0),
    eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0

Tactic:
obtain (h | h) := p.natDegree.eq_zero_or_pos

Premises used: Polynomial.natDegree, Nat.eq_zero_or_pos
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
pos :
  ∀ (h0 : p.coeff 0 = 0),
    eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
neg :
  ∀ (h0 : ¬p.coeff 0 = 0),
    eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0

Tactic:
by_cases h0 : coeff p 0 = 0

Premises used: Polynomial.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
pos :
  eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) (leadingCoeff ((C : (a : R) → R[X]) (p.coeff 0))) : A) z)
      (integralNormalization ((C : (a : R) → R[X]) (p.coeff 0))) =
    0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) (leadingCoeff ((C : (a : R) → R[X]) (p.coeff 0))) : A) z)
      (integralNormalization ((C : (a : R) → R[X]) (p.coeff 0))) =
    0

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)

Tactic:
rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
hz₁ : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
⊢ Commute ((f : (a : R) → A) p.leadingCoeff) z

Tactic:
rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
hz₁ : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
h₃ : Commute ((f : (a : R) → A) p.leadingCoeff) z
⊢ ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)

Tactic:
rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
hz₁ : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
h₃ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₄ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
⊢ ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C