awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
inr : (if p.natTrailingDegree = 0 then 0 else p.coeff (p.natTrailingDegree + 1)) = p.coeff (p.natTrailingDegree + 1)
inr₁ inr₂ : p.coeff (p.natTrailingDegree + 1) = p.coeff (p.natTrailingDegree + 1)
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
rw [nextCoeffUp, if_neg (natTrailingDegree_ne_zero.2 ⟨hp₀, hp⟩)]

Premises used: Iff.mpr, Polynomial.natTrailingDegree_ne_zero, Polynomial.nextCoeffUp, And.intro, if_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingDegree < q.trailingDegree
⊢ q.coeff p.natTrailingDegree = 0

Tactic:
coeff_eq_zero_of_lt_trailingDegree <| natTrailingDegree_le_trailingDegree.trans_lt h

Premises used: Polynomial.natTrailingDegree_le_trailingDegree, Polynomial.coeff_eq_zero_of_lt_trailingDegree, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ∞
h : p.trailingDegree < n
h₀ : p = 0
⊢ n ≤ p.trailingDegree

Tactic:
simp [h₀]
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Ne (α := R) ((constantCoeff : (a : R[X]) → R) p : R) (0 : R)
⊢ p.natTrailingDegree = 0

Tactic:
le_antisymm (natTrailingDegree_le_of_ne_zero h) zero_le'

Premises used: le_antisymm, zero_le', Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
⊢ p = HPow.hPow (α := R[X]) X p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
refine_1 : ∀ (h : p = HPow.hPow (α := R[X]) X p.natDegree), p.natDegree ≤ p.natTrailingDegree
refine_2 : ∀ (h : p.natDegree ≤ p.natTrailingDegree), p = HPow.hPow (α := R[X]) X p.natDegree
⊢ p = HPow.hPow (α := R[X]) X p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p = HPow.hPow (α := R[X]) X p.natDegree
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p = HPow.hPow (α := R[X]) X p.natDegree
h_1 : Nontrivial R
rw : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ (HPow.hPow (α := R[X]) X p.natDegree).natTrailingDegree
rw₁ : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ p.natDegree
rw₂ rw₃ : p.natDegree ≤ p.natDegree
⊢ p.natDegree ≤ p.natTrailingDegree

Tactic:
rw [h, natTrailingDegree_X_pow, ← h]

Premises used: Polynomial.natTrailingDegree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
refine_2 : ∀ (n : ℕ), p.coeff n = (HPow.hPow (α := R[X]) X p.natDegree).coeff n
⊢ p = HPow.hPow (α := R[X]) X p.natDegree

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
refine_2 : p.coeff n = if n = p.natDegree then 1 else 0
⊢ p.coeff n = (HPow.hPow (α := R[X]) X p.natDegree).coeff n

Tactic:
rw [coeff_X_pow]

Premises used: Polynomial.coeff_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
refine_2 : ∀ (hn : n < p.natDegree), p.coeff n = if n = p.natDegree then 1 else 0
refine_2₁ : p.coeff p.natDegree = if p.natDegree = p.natDegree then 1 else 0
refine_2₂ : ∀ (hn : p.natDegree < n), p.coeff n = if n = p.natDegree then 1 else 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
obtain hn | rfl | hn := lt_trichotomy n p.natDegree

Premises used: Polynomial.natDegree, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
refine_2 : p.coeff n = 0
refine_2₁ refine_2₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree, LT.lt.trans_le, if_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
⊢ p.coeff p.natDegree = if p.natDegree = p.natDegree then 1 else 0

Tactic:
simpa only [if_pos rfl] using h₁.leadingCoeff

Premises used: if_pos, Polynomial.Monic.leadingCoeff, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
refine_2 : p.coeff n = 0
refine_2₁ refine_2₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]

Premises used: LT.lt.ne', Polynomial.coeff_eq_zero_of_natDegree_lt, if_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
⊢ p = HPow.hPow (α := R[X]) X p.natDegree ↔ p.natTrailingDegree = p.natDegree

Tactic:
h₁.eq_X_pow_iff_natDegree_le_natTrailingDegree.trans (natTrailingDegree_le_natDegree p).ge_iff_eq

Premises used: Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree, Polynomial.natTrailingDegree_le_natDegree, LE.le.ge_iff_eq, Iff.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
obtain : ∀ (q : R[X]) (hq : p * q = 1), p.natDegree = 0
⊢ p.natDegree = 0

Tactic:
obtain ⟨q, hq⟩ := h.exists_right_inv

Premises used: IsUnit.exists_right_inv
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
q : R[X]
hq : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p.natDegree = 0 ∧ q.natDegree = 0

Tactic:
rw [hq, natDegree_one, eq_comm, add_eq_zero] at this

Premises used: eq_comm, Polynomial.natDegree_one, add_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
q : R[X]
hq : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p.natDegree = 0

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
q : R[X]
hq : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p.natDegree = 0

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
inst_2 : Nontrivial R
h : IsUnit p
⊢ p.degree = 0

Tactic:
(natDegree_eq_zero_iff_degree_le_zero.mp <| natDegree_eq_zero_of_isUnit h).antisymm
    (zero_le_degree_iff.mpr h.ne_zero)

Premises used: Iff.mpr, Polynomial.zero_le_degree_iff, LE.le.antisymm, Iff.mp, IsUnit.ne_zero, Polynomial.natDegree_eq_zero_iff_degree_le_zero, Polynomial.natDegree_eq_zero_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
⊢ (↑u : R[X]).degree = 0

Tactic:
degree_eq_zero_of_isUnit ⟨u, rfl⟩

Premises used: Polynomial.degree_eq_zero_of_isUnit, Exists.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
⊢ IsUnit p ↔ ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = p

Tactic:
⟨fun hp =>
    ⟨p.coeff 0,
      let h := eq_C_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hp)
      ⟨isUnit_C.1 (h ▸ hp), h.symm⟩⟩,
    fun ⟨_, hr, hrp⟩ => hrp ▸ isUnit_C.2 hr⟩

Premises used: Iff.mpr, IsUnit, Eq.rec, Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.isUnit_C, Polynomial.coeff, And.intro, Iff.intro, Exists.intro, Iff.mp, _private.0.Polynomial.isUnit_iff.match_1, Polynomial.natDegree_eq_zero_of_isUnit, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
inl : Subsingleton R → ¬IsUnit p
inr : Nontrivial R → ¬IsUnit p
⊢ ¬IsUnit p

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h : Subsingleton R
⊢ ¬IsUnit p

Tactic:
simp [Subsingleton.elim p 0] at hpl

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h_1 : Nontrivial R
h : IsUnit p
⊢ False

Tactic:
simp [degree_eq_zero_of_isUnit h] at hpl

Premises used: Polynomial.degree_eq_zero_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
hpl : 0 < p.natDegree
⊢ ¬IsUnit p

Tactic:
not_isUnit_of_degree_pos _ (natDegree_pos_iff_degree_pos.mp hpl)

Premises used: Polynomial.not_isUnit_of_degree_pos, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
u : R[X]ˣ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
u : R[X]ˣ
h : Nontrivial R
⊢ (↑u : R[X]).natDegree = 0

Tactic:
natDegree_eq_of_degree_eq_some (degree_coe_units u)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_coe_units
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
u : R[X]ˣ
h : Nontrivial R
⊢ (↑u : R[X]).natDegree = 0

Tactic:
exact natDegree_eq_of_degree_eq_some (degree_coe_units u)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_coe_units
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
rw : (↑u : R[X]).natDegree
| 0

Tactic:
rw [← natDegree_coe_units u]

Premises used: Polynomial.natDegree_coe_units
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
conv : (↑u : R[X]).coeff (↑u : R[X]).natDegree ≠ 0
⊢ (↑u : R[X]).coeff 0 ≠ 0

Tactic:
conv in 0 => rw [← natDegree_coe_units u]

Premises used: Polynomial.natDegree_coe_units
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
rw : ¬(↑u : R[X]) = 0
⊢ (↑u : R[X]).coeff (↑u : R[X]).natDegree ≠ 0

Tactic:
rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]

Premises used: Polynomial.leadingCoeff, Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
⊢ ¬(↑u : R[X]) = 0

Tactic:
Units.ne_zero _

Premises used: Units.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
⊢ ¬(↑u : R[X]) = 0

Tactic:
exact Units.ne_zero _

Premises used: Units.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hp : p.Monic
hu : ¬IsUnit p
⊢ 0 < p.degree

Tactic:
hp.degree_pos.mpr fun hp' ↦ (hp' ▸ hu) isUnit_one

Premises used: Iff.mpr, Polynomial.Monic.degree_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hp : p.Monic
hu : ¬IsUnit p
⊢ 0 < p.natDegree

Tactic:
hp.natDegree_pos.mpr fun hp' ↦ (hp' ▸ hu) isUnit_one

Premises used: Iff.mpr, Polynomial.Monic.natDegree_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : CommSemiring R
a p : R[X]
hp : p.Monic
ha : ¬IsUnit a
hap : a ∣ p
contrapose! : ∀ (h : a.degree ≤ 0), IsUnit a
⊢ 0 < a.degree

Tactic:
contrapose! ha with h
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : CommSemiring R
a p : R[X]
hp : p.Monic
hap : a ∣ p
h : a.degree ≤ 0
rw :
  ∀ (hap : (C : (a : R) → R[X]) (a.coeff 0) ∣ p) (h : a.degree ≤ 0),
    IsUnit (M := R[X]) ((C : (a : R) → R[X]) (a.coeff 0) : R[X])
⊢ IsUnit a

Tactic:
rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : CommSemiring R
a p : R[X]
hp : p.Monic
hap : (C : (a : R) → R[X]) (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (a.coeff 0) : R[X])

Tactic:
simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap

Premises used: Polynomial.isUnit_C, Polynomial.Monic.C_dvd_iff_isUnit
-- Module: Mathlib.Algebra.Polynomial.Degree.Units
Goal:
R : Type u
inst : CommSemiring R
a p : R[X]
hp : p.Monic
ha : ¬IsUnit a
hap : a ∣ p
⊢ 0 < a.natDegree

Tactic:
natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_not_isUnit_of_dvd_monic hp ha hap

Premises used: Iff.mpr, Polynomial.degree_pos_of_not_isUnit_of_dvd_monic, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
⊢ (i : (a : R) → K) 0 =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi) (Polynomial.map i 0)

Tactic:
simp only [eval_zero, map_zero, mul_zero, Polynomial.map_zero]

Premises used: map_zero, Polynomial.eval_zero, MulZeroClass.mul_zero, Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
⊢ DenomsClearable a b N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) i

Tactic:
⟨r * a ^ n * b ^ (N - n), bi, bu, ?_⟩

Premises used: HMul.hMul, HSub.hSub, DenomsClearable, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
refine :
  (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi)
        (Polynomial.map i (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
⊢ DenomsClearable a b N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) i

Tactic:
refine ⟨r * a ^ n * b ^ (N - n), bi, bu, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
rw :
  (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi) X ^ n)
⊢ (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi)
        (Polynomial.map i (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))

Tactic:
rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]

Premises used: Polynomial.eval_C, Polynomial.eval_pow, Polynomial.map_monomial, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.eval_mul
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
rw :
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
⊢ (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi) X ^ n)

Tactic:
rw [map_mul, map_mul, map_pow, map_pow, eval_X, mul_comm]

Premises used: Polynomial.eval_X, map_pow, map_mul, mul_comm
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
rw :
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
⊢ HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)

Tactic:
rw [← tsub_add_cancel_of_le nN]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
rw :
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K)
      (HMul.hMul (α := K) ((i : (a : R) → K) a : K) (HMul.hMul (β := K) bi ((i : (a : R) → K) b : K)) ^ n)
| HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n)

Tactic:
rw [← mul_one (i a), ← bu]

Premises used: mul_one, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
conv_lhs :
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K)
        (HMul.hMul (α := K) ((i : (a : R) → K) a : K) (HMul.hMul (β := K) bi ((i : (a : R) → K) b : K)) ^ n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
⊢ HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)

Tactic:
conv_lhs => rw [← mul_one (i a), ← bu]

Premises used: mul_one, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
n : ℕ
r : R
nN : n ≤ N
⊢ HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K)
        (HMul.hMul (α := K) ((i : (a : R) → K) a : K) (HMul.hMul (β := K) bi ((i : (a : R) → K) b : K)) ^ n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)

Tactic:
simp [mul_assoc, mul_comm, mul_left_comm, pow_add, mul_pow]

Premises used: mul_assoc, pow_add, mul_left_comm, mul_comm, mul_pow
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
h : DenomsClearable a b N f i
h_1 : DenomsClearable a b N g i
Df : R
bf : K
bfu : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
Hf :
  (i : (a : R) → K) Df =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
Hg :
  (i : (a : R) → K) Dg =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g)
rw :
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f) +
      HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f) +
      HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i g)
⊢ (i : (a : R) → K) (Df + Dg) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i (f + g))

Tactic:
rw [map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]

Premises used: Polynomial.map_add, map_add, Polynomial.eval_add, mul_add
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
h : DenomsClearable a b N f i
h_1 : DenomsClearable a b N g i
Df : R
bf : K
bfu : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
Hf :
  (i : (a : R) → K) Df =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
Hg :
  (i : (a : R) → K) Dg =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g)
e_a : bg = bf
⊢ HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f) +
      HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f) +
      HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i g)

Tactic:
congr