awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
H : IsUnit q
hr : r ≠ 0
obtain :
  ∀ (s : R) (hs : IsUnit s)
    (hq : p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) s : R[X]))
    (H : IsUnit (M := R[X]) ((C : (a : R) → R[X]) s : R[X])), False
⊢ False

Tactic:
obtain ⟨s, hs, rfl⟩ := Polynomial.isUnit_iff.mp H

Premises used: Polynomial.isUnit_iff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
hr : r ≠ 0
s : R
hs : IsUnit s
hq : p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) s : R[X])
H : IsUnit (M := R[X]) ((C : (a : R) → R[X]) s : R[X])
⊢ False

Tactic:
simp [hq, Polynomial.natDegree_C_mul hr] at hp'

Premises used: Polynomial.natDegree_C_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
F : Type u_2
inst : Field F
p : F[X]
⊢ p.IsPrimitive ↔ p ≠ 0

Tactic:
⟨IsPrimitive.ne_zero, fun h _ hrp ↦ .mk0 _ fun hr ↦ ne_zero_of_dvd_ne_zero h hrp <| hr ▸ C_0⟩

Premises used: Polynomial.C_0, Eq.rec, Polynomial.IsPrimitive.ne_zero, IsUnit.mk0, Iff.intro, ne_zero_of_dvd_ne_zero, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
pos : ∀ (h : n ∈ p.support), p.content ∣ p.coeff n
neg : ∀ (h : n ∉ p.support), p.content ∣ p.coeff n
⊢ p.content ∣ p.coeff n

Tactic:
by_cases h : n ∈ p.support

Premises used: Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

Tactic:
apply Finset.gcd_dvd h

Premises used: Finset.gcd_dvd
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.coeff n = 0

Tactic:
rw [mem_support_iff, Classical.not_not] at h

Premises used: Classical.not_not, Polynomial.mem_support_iff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
neg : p.content ∣ 0
⊢ p.content ∣ p.coeff n

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
pos :
  ∀ (h0 : r = 0),
    Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
      ((normalize : (a : R) → R) r : R)
neg :
  ∀ (h0 : ¬r = 0),
    Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
      ((normalize : (a : R) → R) r : R)
⊢ Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)

Tactic:
by_cases h0 : r = 0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ support.{u_1} (R := R) ((C : (a : R) → R[X]) r) = {0}

Tactic:
have h : (C r).support = {0} := support_monomial _ h0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : support.{u_1} (R := R) ((C : (a : R) → R[X]) r) = {0}
⊢ Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 0)) 0
rw₁ : Eq.{u_1 + 1} (α := R) ((normalize : (a : R) → R) 0 : R) (0 : R)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (content 0) 0

Tactic:
rw [← C_0, content_C, normalize_zero]

Premises used: Polynomial.C_0, Polynomial.content_C, normalize_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 1)) 1
rw₁ : Eq.{u_1 + 1} (α := R) ((normalize : (a : R) → R) 1 : R) (1 : R)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (content 1) 1

Tactic:
rw [← C_1, content_C, normalize_one]

Premises used: normalize_one, Polynomial.C_1, Polynomial.content_C
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd

Tactic:
congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
refine : Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd

Tactic:
refine congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ∀ (a : ℕ), a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
⊢ (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support

Tactic:
ext a
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬(X * p).coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a
⊢ a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support

Tactic:
simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]

Premises used: Polynomial.mem_support_iff, Ne, Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬(X * p).coeff 0 = 0 ↔ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ a.succ = 0
h₁ : ∀ (a : ℕ), ¬(X * p).coeff (a + 1) = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
⊢ ¬(X * p).coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a

Tactic:
rcases a with - | a
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ a.succ = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
rw [mul_comm, coeff_mul_X]

Premises used: Polynomial.coeff_mul_X, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0 → ∃ (a_2 : ℕ), ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1
h₁ : (∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0
⊢ ¬p.coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0
w : ℕ
h₁ : ¬p.coeff a = 0 ∧ a.succ = a + 1
⊢ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
use a
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
h : ¬p.coeff b = 0
⊢ ¬p.coeff a = 0

Tactic:
rw [← Nat.succ_injective h2]

Premises used: Nat.succ_injective
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
⊢ ¬p.coeff b = 0

Tactic:
apply h1
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support

Tactic:
have h : (X * p).support = p.support.map ⟨Nat.succ, Nat.succ_injective⟩ := by
    ext a
    simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]
    rcases a with - | a
    · simp
    rw [mul_comm, coeff_mul_X]
    constructor
    · intro h
      use a
    · rintro ⟨b, ⟨h1, h2⟩⟩
      rw [← Nat.succ_injective h2]
      apply h1
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
rw :
  Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support).val =
    Multiset.map p.coeff p.support.val
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
⊢ Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support).val =
    Multiset.map p.coeff p.support.val

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
⊢ (HPow.hPow (α := R[X]) (β := ℕ) X 0).content = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
k : ℕ
hi : (HPow.hPow (α := R[X]) X k).content = 1
succ : (X * HPow.hPow (α := R[X]) X k).content = 1
succ₁ : (HPow.hPow (α := R[X]) X k).content = 1
succ₂ succ₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (HPow.hPow (α := R[X]) X (k + 1)).content = 1

Tactic:
rw [pow_succ', content_X_mul, hi]

Premises used: Polynomial.content_X_mul, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
k : ℕ
zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).content = 1
succ : ∀ (k : ℕ) (hi : (HPow.hPow (α := R[X]) X k).content = 1), (HPow.hPow (α := R[X]) X (k + 1)).content = 1
⊢ (HPow.hPow (α := R[X]) X k).content = 1

Tactic:
induction k with
  | zero => simp
  | succ k hi => rw [pow_succ', content_X_mul, hi]

Premises used: Polynomial.content_X_mul, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : (HMul.hMul (α := R[X]) X 1).content = 1
rw₁ : Eq.{u_1 + 1} (α := R) (content 1) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (content X) 1

Tactic:
rw [← mul_one X, content_X_mul, content_one]

Premises used: Polynomial.content_X_mul, Polynomial.content_one, mul_one, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
pos :
  ∀ (h0 : r = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
      HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
neg :
  ∀ (h0 : ¬r = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
      HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content

Tactic:
by_cases h0 : r = 0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (p.support.gcd p.coeff)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content

Tactic:
rw [content]

Premises used: Polynomial.content
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    p.support.gcd fun (x : ℕ) ↦ r * p.coeff x
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (p.support.gcd p.coeff)

Tactic:
rw [← Finset.gcd_mul_left]

Premises used: Finset.gcd_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    p.support.gcd fun (x : ℕ) ↦ r * p.coeff x

Tactic:
congr (congr rfl ?_) ?_

Premises used: congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support = p.support
neg₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff = fun (x : ℕ) ↦ r * p.coeff x
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    p.support.gcd fun (x : ℕ) ↦ r * p.coeff x

Tactic:
refine congr (congr rfl ?_) ?_

Premises used: congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
neg : ∀ (a : ℕ), a ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support ↔ a ∈ p.support
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support = p.support

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
neg : ∀ (x : ℕ), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff x = r * p.coeff x
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff = fun (x : ℕ) ↦ r * p.coeff x

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a : ℕ
⊢ a ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support ↔ a ∈ p.support

Tactic:
simp [h0, mem_support_iff]

Premises used: Polynomial.mem_support_iff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff x = r * p.coeff x

Tactic:
simp [h0, mem_support_iff]

Premises used: Polynomial.mem_support_iff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
k : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k)).content =
    (normalize : (a : R) → R) r
rw₁ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (HPow.hPow (α := R[X]) X k).content = (normalize : (a : R) → R) r
rw₂ : HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) r : R) (1 : R) = (normalize : (a : R) → R) r
rw₃ rw₄ : Eq (α := R) ((normalize : (a : R) → R) r : R) ((normalize : (a : R) → R) r : R)
⊢ Eq (α := R) (content ((monomial k : (a : R) → R[X]) r) : R) ((normalize : (a : R) → R) r : R)

Tactic:
rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.content_C_mul, mul_one, Polynomial.content_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
rw : (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0
⊢ p.content = 0 ↔ p = 0

Tactic:
rw [content, Finset.gcd_eq_zero_iff]

Premises used: Finset.gcd_eq_zero_iff, Polynomial.content
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
mp : (∀ x ∈ p.support, p.coeff x = 0) → p = 0
mpr : p = 0 → ∀ x ∈ p.support, p.coeff x = 0
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
mp : ∀ (n : ℕ), p.coeff n = coeff 0 n
⊢ p = 0

Tactic:
ext n
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
⊢ p.coeff n = coeff 0 n

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : p = 0
x : ℕ
⊢ x ∈ p.support → p.coeff x = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (normalize : (a : R) → R) p.content = p.content

Tactic:
Finset.normalize_gcd

Premises used: Polynomial.content, Finset.normalize_gcd
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
pos : ∀ (hp0 : p.content = 0), Eq (α := Rˣ) (normUnit p.content) 1
neg : ∀ (hp0 : ¬p.content = 0), Eq (α := Rˣ) (normUnit p.content) 1
⊢ Eq (α := Rˣ) (normUnit p.content) 1

Tactic:
by_cases hp0 : p.content = 0

Premises used: Polynomial.content
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp0 : p.content = 0
⊢ Eq (α := Rˣ) (normUnit p.content) 1

Tactic:
simp [hp0]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
neg : (↑(normUnit p.content) : R) = (↑1 : R)
⊢ Eq (α := Rˣ) (normUnit p.content) 1

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
neg : p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)
⊢ (↑(normUnit p.content) : R) = (↑1 : R)

Tactic:
apply mul_left_cancel₀ hp0

Premises used: mul_left_cancel₀
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
neg : (normalize : (a : R) → R) p.content = p.content * (↑1 : R)
neg₁ : p.content = p.content * (↑1 : R)
neg₂ : p.content = p.content * 1
neg₃ neg₄ : p.content = p.content
⊢ p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)

Tactic:
rw [← normalize_apply, normalize_content, Units.val_one, mul_one]

Premises used: Polynomial.normalize_content, normalize_apply, Units.val_one, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
hab : p.content ∣ (Finset.range n).gcd p.coeff
hba : (Finset.range n).gcd p.coeff ∣ p.content
⊢ p.content = (Finset.range n).gcd p.coeff

Tactic:
apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd

Premises used: dvd_antisymm_of_normalize_eq, Polynomial.normalize_content, Finset.normalize_gcd
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
hab : ∀ b ∈ Finset.range n, p.content ∣ p.coeff b
⊢ p.content ∣ (Finset.range n).gcd p.coeff

Tactic:
rw [Finset.dvd_gcd_iff]

Premises used: Finset.dvd_gcd_iff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
hab : i ∈ Finset.range n → p.content ∣ p.coeff i
⊢ i ∈ Finset.range n → p.content ∣ p.coeff i

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
h_1 : i ∈ Finset.range n
⊢ p.content ∣ p.coeff i

Tactic:
apply content_dvd_coeff _

Premises used: Polynomial.content_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finset.range n).gcd p.coeff ∣ p.content

Tactic:
Finset.gcd_mono (supp_subset_range h)

Premises used: Polynomial.supp_subset_range, Finset.gcd_mono, Polynomial.content
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finset.range n).gcd p.coeff ∣ p.content

Tactic:
exact Finset.gcd_mono (supp_subset_range h)

Premises used: Polynomial.supp_subset_range, Finset.gcd_mono
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = (Finset.range p.natDegree.succ).gcd p.coeff

Tactic:
content_eq_gcd_range_of_lt _ _ (Nat.lt_succ_self _)

Premises used: Polynomial.content_eq_gcd_range_of_lt, Nat.lt_succ_self
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
pos : ∀ (h : p = 0), p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
neg : ∀ (h : ¬p = 0), p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content

Tactic:
by_cases h : p = 0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.natDegree ∈ p.support

Tactic:
rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] at h

Premises used: Polynomial.mem_support_iff, Polynomial.leadingCoeff, Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
neg :
  @gcd _ CommSemiring.toCommMonoidWithZero _ (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ (p.coeff p.natDegree)
      ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content

Tactic:
rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content,
    eraseLead_support]

Premises used: Polynomial.eraseLead_support, Polynomial.leadingCoeff, Polynomial.content, Finset.gcd_insert, Finset.insert_erase