awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0
inst_6 : Nontrivial S
this : IsDomain R
rwa : p.content ≠ 0
rwa₁ : ¬p.content = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ¬p = 0
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) p.content : S) (0 : S)

Tactic:
rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]

Premises used: Polynomial.content_eq_zero_iff, map_zero, Ne, FaithfulSMul.algebraMap_injective, Function.Injective.ne_iff'
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s p = 0
⊢ HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0

Tactic:
rw [eq_C_content_mul_primPart p, eval₂_mul, eval₂_C] at hp

Premises used: Polynomial.eq_C_content_mul_primPart, Polynomial.eval₂_mul, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp

Premises used: eq_zero_of_ne_zero_of_mul_left_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
refine : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.content : S) (0 : S)
⊢ eval₂ f s p.primPart = 0

Tactic:
refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp

Premises used: eq_zero_of_ne_zero_of_mul_left_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
rwa : p.content ≠ 0
rwa₁ : ¬p.content = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ¬p = 0
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.content : S) (0 : S)

Tactic:
rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]

Premises used: Polynomial.content_eq_zero_iff, map_zero, Ne, Function.Injective.ne_iff'
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
rw :
  @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ a q.content
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ a q.content

Tactic:
rw [content_eq_gcd_range_of_lt p (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_left _ _) (Nat.lt_succ_self _))]

Premises used: lt_of_le_of_lt, Polynomial.content_eq_gcd_range_of_lt, Nat.lt_succ_self, Max.max, Polynomial.natDegree, le_max_left, Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
rw :
  @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ a q.content

Tactic:
rw [content_eq_gcd_range_of_lt q (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_right _ _) (Nat.lt_succ_self _))]

Premises used: le_max_right, lt_of_le_of_lt, Polynomial.content_eq_gcd_range_of_lt, Nat.lt_succ_self, Max.max, Polynomial.natDegree, Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
h₁ : ∀ x ∈ Finset.range (max p.natDegree q.natDegree).succ, a ∣ p.coeff x - q.coeff x
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)

Tactic:
apply Finset.gcd_eq_of_dvd_sub

Premises used: Finset.gcd_eq_of_dvd_sub
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
x : ℕ
h₁ : x ∈ Finset.range (max p.natDegree q.natDegree).succ → a ∣ p.coeff x - q.coeff x
⊢ x ∈ Finset.range (max p.natDegree q.natDegree).succ → a ∣ p.coeff x - q.coeff x

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
x : ℕ
h_1 : x ∈ Finset.range (max p.natDegree q.natDegree).succ
h₁ : ∀ (w : R[X]) (hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w), a ∣ p.coeff x - q.coeff x
⊢ a ∣ p.coeff x - q.coeff x

Tactic:
obtain ⟨w, hw⟩ := h
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
h_1 : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w
h : p.coeff x - q.coeff x = a * w.coeff x
⊢ a ∣ p.coeff x - q.coeff x

Tactic:
use w.coeff x

Premises used: Polynomial.coeff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
h_1 : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w
h : (p - q).coeff x = a * w.coeff x
h₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w).coeff x = a * w.coeff x
h₂ h₃ : a * w.coeff x = a * w.coeff x
⊢ p.coeff x - q.coeff x = a * w.coeff x

Tactic:
rw [← coeff_sub, hw, coeff_C_mul]

Premises used: Polynomial.coeff_C_mul, Polynomial.coeff_sub
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
rw :
  @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p * q).eraseLead.content =
    @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p.eraseLead * q).content
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (p * q).eraseLead.content p.leadingCoeff =
    @gcd _ CommSemiring.toCommMonoidWithZero _ (p.eraseLead * q).content p.leadingCoeff

Tactic:
rw [gcd_comm (content _) _, gcd_comm (content _) _]

Premises used: Polynomial.content, gcd_comm
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p * q).eraseLead.content =
    @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p.eraseLead * q).content

Tactic:
apply gcd_content_eq_of_dvd_sub

Premises used: Polynomial.gcd_content_eq_of_dvd_sub
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h :
  (C : (a : R) → R[X]) p.leadingCoeff ∣
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree * q) -
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X (p * q).natDegree))
⊢ (C : (a : R) → R[X]) p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q

Tactic:
rw [← self_sub_C_mul_X_pow, ← self_sub_C_mul_X_pow, sub_mul, sub_sub, add_comm, sub_add,
    sub_sub_cancel, leadingCoeff_mul, map_mul, mul_assoc, mul_assoc]

Premises used: sub_add, Polynomial.leadingCoeff_mul, mul_assoc, add_comm, sub_mul, sub_sub, map_mul, sub_sub_cancel, Polynomial.self_sub_C_mul_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
⊢ (C : (a : R) → R[X]) p.leadingCoeff ∣
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree * q) -
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X (p * q).natDegree))

Tactic:
apply dvd_sub (Dvd.intro _ rfl) (Dvd.intro _ rfl)

Premises used: Dvd.intro, dvd_sub, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h_1 : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < (↑n : WithBot ℕ) → (p * q).content = p.content * q.content
a : (p * q).degree < (↑(Nat.succ (↑(p * q).natDegree : ℕ)) : WithBot ℕ)
n : ℕ
⊢ (p * q).content = p.content * q.content

Tactic:
apply h
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h : Nontrivial R
suffices : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < (↑n : WithBot ℕ) → (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content

Tactic:
suffices h :
        ∀ (n : ℕ) (p q : R[X]), (p * q).degree < n → (p * q).content = p.content * q.content by
      apply h
      apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
p q : R[X]
hpq : (p * q).degree < (↑0 : WithBot ℕ)
⊢ p = 0 ∨ q = 0

Tactic:
rw [Nat.cast_zero, Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq

Premises used: mul_eq_zero, Nat.WithBot.lt_zero_iff, Nat.cast_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
p q : R[X]
hpq : p = 0 ∨ q = 0
zero : (0 * q).content = content 0 * q.content
zero₁ : (p * 0).content = p.content * content 0
⊢ (p * q).content = p.content * q.content

Tactic:
rcases hpq with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q_1 : R[X]
h : Nontrivial R
q : R[X]
⊢ (0 * q).content = content 0 * q.content

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q : R[X]
h : Nontrivial R
p : R[X]
⊢ (p * 0).content = p.content * content 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
⊢ (p * q).content = p.content * q.content

Tactic:
?_
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
p q : R[X]
hpq : (p * q).degree < (↑n : WithBot ℕ)
succ :
  ∀ (n : ℕ) (ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content)
    (p q : R[X]) (hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content

Tactic:
induction n generalizing p q with
    | zero =>
      rw [Nat.cast_zero, Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
      rcases hpq with (rfl | rfl) <;> simp
    | succ n ih => ?_

Premises used: mul_eq_zero, Nat.WithBot.lt_zero_iff, Nat.cast_zero, rfl, Polynomial.degree_eq_bot
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
pos : ∀ (p0 : p = 0), (p * q).content = p.content * q.content
neg : ∀ (p0 : ¬p = 0), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content

Tactic:
by_cases p0 : p = 0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : p = 0
⊢ (p * q).content = p.content * q.content

Tactic:
simp [p0]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
pos : ∀ (q0 : q = 0), (p * q).content = p.content * q.content
neg : ∀ (q0 : ¬q = 0), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content

Tactic:
by_cases q0 : q = 0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
q0 : q = 0
⊢ (p * q).content = p.content * q.content

Tactic:
simp [q0]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
q0 : ¬q = 0
⊢ (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n

Tactic:
rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_lt,
      Nat.lt_succ_iff_lt_or_eq, ← Nat.cast_lt (α := WithBot ℕ),
      ← degree_eq_natDegree (mul_ne_zero p0 q0), natDegree_mul p0 q0] at hpq

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_mul, Nat.lt_succ_iff_lt_or_eq, mul_ne_zero, Nat.cast_lt
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
q0 : ¬q = 0
hpq₁ : (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n
⊢ ¬p = 0

Tactic:
rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_lt,
      Nat.lt_succ_iff_lt_or_eq, ← Nat.cast_lt (α := WithBot ℕ),
      ← degree_eq_natDegree (mul_ne_zero p0 q0), natDegree_mul p0 q0] at hpq

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_mul, Nat.lt_succ_iff_lt_or_eq, mul_ne_zero, Nat.cast_lt
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
q0 : ¬q = 0
hpq₁ : (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n
p0₁ : ¬p = 0
⊢ ¬q = 0

Tactic:
rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_lt,
      Nat.lt_succ_iff_lt_or_eq, ← Nat.cast_lt (α := WithBot ℕ),
      ← degree_eq_natDegree (mul_ne_zero p0 q0), natDegree_mul p0 q0] at hpq

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_mul, Nat.lt_succ_iff_lt_or_eq, mul_ne_zero, Nat.cast_lt
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
neg : ∀ (hlt : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
neg₁ : ∀ (heq : p.natDegree + q.natDegree = n), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content

Tactic:
rcases hpq with (hlt | heq)
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
hlt : (p * q).degree < (↑n : WithBot ℕ)
⊢ (p * q).content = p.content * q.content

Tactic:
apply ih _ _ hlt
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.natDegree + q.natDegree = n
⊢ p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)

Tactic:
rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← Nat.cast_inj (R := WithBot ℕ),
      Nat.cast_add, ← degree_eq_natDegree p.primPart_ne_zero,
      ← degree_eq_natDegree q.primPart_ne_zero] at heq

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_primPart, Nat.cast_inj, Nat.cast_add, Polynomial.primPart_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
⊢ (p * q).content = p.content * q.content

Tactic:
rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]

Premises used: Polynomial.eq_C_content_mul_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
neg : (q.primPart * p.primPart).content = 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content

Tactic:
suffices h : (q.primPart * p.primPart).content = 1 by
      rw [mul_assoc, content_C_mul, content_C_mul, mul_comm p.primPart, mul_assoc, content_C_mul,
        content_C_mul, h, mul_one, content_primPart, content_primPart, mul_one, mul_one]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
neg :
  @gcd _ CommSemiring.toCommMonoidWithZero _ (q.primPart * p.primPart).eraseLead.content
      (q.primPart.leadingCoeff * p.primPart.leadingCoeff) ∣
    1
⊢ (q.primPart * p.primPart).content = 1

Tactic:
rw [← normalize_content, normalize_eq_one, isUnit_iff_dvd_one,
      content_eq_gcd_leadingCoeff_content_eraseLead, leadingCoeff_mul, gcd_comm]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.normalize_content, gcd_comm, Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead, normalize_eq_one, isUnit_iff_dvd_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
neg :
  @gcd _ CommSemiring.toCommMonoidWithZero _ (q.primPart * p.primPart).eraseLead.content q.primPart.leadingCoeff *
      @gcd _ CommSemiring.toCommMonoidWithZero _ (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (q.primPart * p.primPart).eraseLead.content
      (q.primPart.leadingCoeff * p.primPart.leadingCoeff) ∣
    1

Tactic:
apply (gcd_mul_dvd_mul_gcd _ _ _).trans

Premises used: gcd_mul_dvd_mul_gcd, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
neg : (p.primPart.eraseLead * q.primPart).degree < (↑n : WithBot ℕ)
neg₁ : (q.primPart.eraseLead * p.primPart).degree < (↑n : WithBot ℕ)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (q.primPart * p.primPart).eraseLead.content q.primPart.leadingCoeff *
      @gcd _ CommSemiring.toCommMonoidWithZero _ (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1

Tactic:
rw [content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ←
      content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart, one_mul,
      mul_comm q.primPart, content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ←
      content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart]

Premises used: Polynomial.content_mul_aux, gcd_comm, Polynomial.primPart, mul_comm, Polynomial.content_primPart, mul_one, Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
neg : p.primPart.eraseLead.degree < p.primPart.degree
neg₁ : q.primPart.degree ≠ ⊥
⊢ (p.primPart.eraseLead * q.primPart).degree < (↑n : WithBot ℕ)

Tactic:
rw [← heq, degree_mul, WithBot.add_lt_add_iff_right]

Premises used: Polynomial.degree_mul, WithBot.add_lt_add_iff_right