awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ @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)

Tactic:
congr rfl (Finset.gcd_congr rfl fun i hi => ?_)

Premises used: Finset.gcd_congr, congr, rfl
-- 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 : ∀ (i : ℕ) (hi : i ∈ p.support.erase p.natDegree), p.coeff i = p.eraseLead.coeff i
⊢ @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)

Tactic:
refine congr rfl (Finset.gcd_congr rfl fun i hi => ?_)

Premises used: Finset.gcd_congr, congr, rfl
-- 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
i : ℕ
hi : i ∈ p.support.erase p.natDegree
⊢ i ≠ p.natDegree ∧ i ∈ p.support

Tactic:
rw [Finset.mem_erase] at hi

Premises used: Finset.mem_erase
-- 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
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
neg : p.coeff i = if i = p.natDegree then 0 else p.coeff i
neg₁ neg₂ : p.coeff i = p.coeff i
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
rw [eraseLead_coeff, if_neg hi.1]

Premises used: Polynomial.eraseLead_coeff, And.left, if_neg
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
r : R
rw : r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.content ↔ (C : (a : R) → R[X]) r ∣ p

Tactic:
rw [C_dvd_iff_dvd_coeff]

Premises used: Polynomial.C_dvd_iff_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
r : R
mp : r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i
mpr : (∀ (i : ℕ), r ∣ p.coeff i) → r ∣ p.content
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ p.content
i : ℕ
⊢ r ∣ p.coeff i

Tactic:
apply h.trans (content_dvd_coeff _)

Premises used: Polynomial.content_dvd_coeff, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
mpr : ∀ b ∈ p.support, r ∣ p.coeff b
⊢ r ∣ p.content

Tactic:
rw [content, Finset.dvd_gcd_iff]

Premises used: Polynomial.content, Finset.dvd_gcd_iff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
mpr : i ∈ p.support → r ∣ p.coeff i
⊢ i ∈ p.support → r ∣ p.coeff i

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
h_1 : i ∈ p.support
⊢ r ∣ p.coeff i

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

Tactic:
dvd_content_iff_C_dvd.1 dvd_rfl

Premises used: Polynomial.dvd_content_iff_C_dvd, Iff.mp, dvd_rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
rw : (∀ (r : R), (C : (a : R) → R[X]) r ∣ p → IsUnit r) ↔ IsUnit p.content
⊢ p.IsPrimitive ↔ p.content = 1

Tactic:
rw [← normalize_content, normalize_eq_one, IsPrimitive]

Premises used: Polynomial.IsPrimitive, Polynomial.normalize_content, normalize_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
simp_rw : (∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content
⊢ (∀ (r : R), (C : (a : R) → R[X]) r ∣ p → IsUnit r) ↔ IsUnit p.content

Tactic:
simp_rw [← dvd_content_iff_C_dvd]

Premises used: Polynomial.dvd_content_iff_C_dvd
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content

Tactic:
⟨fun h => h p.content (dvd_refl p.content), fun h r hdvd => isUnit_of_dvd_unit hdvd h⟩

Premises used: isUnit_of_dvd_unit, Polynomial.content, Iff.intro, dvd_refl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content

Tactic:
exact ⟨fun h => h p.content (dvd_refl p.content), fun h r hdvd => isUnit_of_dvd_unit hdvd h⟩
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ p.content = 1

Tactic:
isPrimitive_iff_content_eq_one.mp hp

Premises used: Polynomial.isPrimitive_iff_content_eq_one, Iff.mp
-- 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 = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
neg : ∀ (h : ¬p = 0), p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
⊢ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart

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 = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart

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
neg :
  p =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X])
      (if p = 0 then 1
      else
        Classical.choose (p := fun (x : R[X]) ↦ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) x) ⋯)
neg₁ :
  p =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X])
      (Classical.choose (p := fun (x : R[X]) ↦ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) x) ⋯)
neg₂ neg₃ : p = p
⊢ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart

Tactic:
rw [primPart, if_neg h, ← Classical.choose_spec (C_content_dvd p)]

Premises used: Classical.choose_spec, Polynomial.primPart, if_neg, Polynomial.C_content_dvd
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
⊢ Eq.{u_1 + 1} (α := R[X]) (primPart 0) 1

Tactic:
if_pos rfl

Premises used: if_pos, Polynomial.primPart, rfl
-- 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.primPart.IsPrimitive
neg : ∀ (h : ¬p = 0), p.primPart.IsPrimitive
⊢ p.primPart.IsPrimitive

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.primPart.IsPrimitive

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.content = 0

Tactic:
rw [← content_eq_zero_iff] at h

Premises used: Polynomial.content_eq_zero_iff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
neg : p.primPart.content = 1
⊢ p.primPart.IsPrimitive

Tactic:
rw [isPrimitive_iff_content_eq_one]

Premises used: Polynomial.isPrimitive_iff_content_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
neg : p.content * p.primPart.content = p.content * 1
⊢ p.primPart.content = 1

Tactic:
apply mul_left_cancel₀ h

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]
h : ¬p.content = 0
rw : p.content * p.primPart.content
| p.content * 1

Tactic:
rw [p.eq_C_content_mul_primPart, mul_one, content_C_mul, normalize_content]

Premises used: Polynomial.content_C_mul, Polynomial.eq_C_content_mul_primPart, Polynomial.normalize_content, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
conv_rhs : p.content * p.primPart.content = p.content * 1
neg : p.content * p.primPart.content = p.content * p.primPart.content
⊢ p.content * p.primPart.content = p.content * 1

Tactic:
conv_rhs => rw [p.eq_C_content_mul_primPart, mul_one, content_C_mul, normalize_content]

Premises used: Polynomial.content_C_mul, Polynomial.eq_C_content_mul_primPart, Polynomial.normalize_content, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.content = 1

Tactic:
p.isPrimitive_primPart.content_eq_one

Premises used: Polynomial.IsPrimitive.content_eq_one, Polynomial.isPrimitive_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
inst_2 : Nontrivial R
p : R[X]
⊢ p.primPart ≠ 0

Tactic:
p.isPrimitive_primPart.ne_zero

Premises used: Polynomial.IsPrimitive.ne_zero, Polynomial.isPrimitive_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : 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 : R[X]
h : Nontrivial R
pos : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) (0 : R[X])), p.primPart.natDegree = p.natDegree
neg : ∀ (h : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) (0 : R[X])), p.primPart.natDegree = p.natDegree
⊢ p.primPart.natDegree = p.natDegree

Tactic:
by_cases h : C p.content = 0

Premises used: Polynomial.C, Polynomial.content, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_1 : Nontrivial R
h : Eq (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) (0 : R[X])
⊢ p = 0

Tactic:
rw [C_eq_zero, content_eq_zero_iff] at h

Premises used: Polynomial.content_eq_zero_iff, Polynomial.C_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_1 : Nontrivial R
h : p = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_1 : Nontrivial R
h : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) (0 : R[X])
rw : p.primPart.natDegree
| p.natDegree

Tactic:
rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_C, Polynomial.eq_C_content_mul_primPart, zero_add, Polynomial.primPart_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_1 : Nontrivial R
h : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) (0 : R[X])
conv_rhs : p.primPart.natDegree = p.natDegree
neg : p.primPart.natDegree = p.primPart.natDegree
⊢ p.primPart.natDegree = p.natDegree

Tactic:
conv_rhs =>
    rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_C, Polynomial.eq_C_content_mul_primPart, zero_add, Polynomial.primPart_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
rw : 1 * p.primPart = p
rw₁ : (C : (a : R) → R[X]) 1 * p.primPart = p
rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart = p
rw₃ rw₄ : p = p
⊢ p.primPart = p

Tactic:
rw [← one_mul p.primPart, ← C_1, ← hp.content_eq_one, ← p.eq_C_content_mul_primPart]

Premises used: Polynomial.C_1, Polynomial.IsPrimitive.content_eq_one, Polynomial.eq_C_content_mul_primPart, Polynomial.primPart, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
pos : ∀ (h0 : r = 0), IsUnit.{u_1} (M := R[X]) (primPart ((C : (a : R) → R[X]) r))
neg : ∀ (h0 : ¬r = 0), IsUnit.{u_1} (M := R[X]) (primPart ((C : (a : R) → R[X]) r))
⊢ IsUnit.{u_1} (M := R[X]) (primPart ((C : (a : R) → R[X]) 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
⊢ IsUnit.{u_1} (M := R[X]) (primPart ((C : (a : R) → R[X]) 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
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit r)⁻¹ : R) * (↑(normUnit r) : R)) : R[X]) (1 : R[X])
rw₁ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit r) : R) : R[X]) =
    1

Tactic:
rw [← map_mul, Units.inv_mul, C_1]

Premises used: Polynomial.C_1, Units.inv_mul, map_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit r) : R) * (↑(normUnit r)⁻¹ : R)) : R[X]) (1 : R[X])
rw₁ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit r) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R) : R[X]) =
    1

Tactic:
rw [← map_mul, Units.mul_inv, C_1]

Premises used: Polynomial.C_1, Units.mul_inv, map_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
neg :
  Eq (α := R[X])
    ((↑{ val := (C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R), inv := (C : (a : R) → R[X]) (↑(normUnit r) : R),
            val_inv := ⋯, inv_val := ⋯ } :
        R[X]) :
      R[X])
    (primPart ((C : (a : R) → R[X]) r) : R[X])
⊢ ∃ (u : R[X]ˣ), (↑u : R[X]) = primPart ((C : (a : R) → R[X]) r)

Tactic:
refine
    ⟨⟨C ↑(normUnit r)⁻¹, C ↑(normUnit r), by rw [← map_mul, Units.inv_mul, C_1], by
        rw [← map_mul, Units.mul_inv, C_1]⟩,
      ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ¬Eq (α := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X]) (0 : R[X])

Tactic:
rw [← normalize_eq_zero, ← C_eq_zero] at h0

Premises used: Polynomial.C_eq_zero, normalize_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X]) (0 : R[X])
neg :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
      ((↑{ val := (C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R), inv := (C : (a : R) → R[X]) (↑(normUnit r) : R),
              val_inv := ⋯, inv_val := ⋯ : R[X]ˣ } :
          R[X]) :
        R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
      (primPart ((C : (a : R) → R[X]) r))
⊢ Eq (α := R[X])
    ((↑{ val := (C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R), inv := (C : (a : R) → R[X]) (↑(normUnit r) : R),
            val_inv := ⋯, inv_val := ⋯ } :
        R[X]) :
      R[X])
    (primPart ((C : (a : R) → R[X]) r) : R[X])

Tactic:
apply mul_left_cancel₀ h0

Premises used: mul_left_cancel₀
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X]) (0 : R[X])
rw : ((C : (a : R) → R[X]) r : R[X])
| HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
    (primPart ((C : (a : R) → R[X]) r))

Tactic:
rw [← content_C, ← (C r).eq_C_content_mul_primPart]

Premises used: Polynomial.C, Polynomial.eq_C_content_mul_primPart, Polynomial.content_C, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X]) (0 : R[X])
neg :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
      ((↑{ val := (C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R), inv := (C : (a : R) → R[X]) (↑(normUnit r) : R),
              val_inv := ⋯, inv_val := ⋯ : R[X]ˣ } :
          R[X]) :
        R[X]) =
    (C : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
      ((↑{ val := (C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R), inv := (C : (a : R) → R[X]) (↑(normUnit r) : R),
              val_inv := ⋯, inv_val := ⋯ : R[X]ˣ } :
          R[X]) :
        R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
      (primPart ((C : (a : R) → R[X]) r))

Tactic:
conv_rhs => rw [← content_C, ← (C r).eq_C_content_mul_primPart]

Premises used: Polynomial.C, Polynomial.eq_C_content_mul_primPart, Polynomial.content_C, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X]) (0 : R[X])
neg :
  HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
        ((C : (a : R) → R[X]) (↑(normUnit r) : R) : R[X]))
      ((C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R) : R[X]) =
    (C : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X])
      ((↑{ val := (C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R), inv := (C : (a : R) → R[X]) (↑(normUnit r) : R),
              val_inv := ⋯, inv_val := ⋯ : R[X]ˣ } :
          R[X]) :
        R[X]) =
    (C : (a : R) → R[X]) r

Tactic:
simp only [normalize_apply, map_mul]

Premises used: normalize_apply, map_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) ((normalize : (a : R) → R) r) : R[X]) (0 : R[X])
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit r) : R) : R[X])
        ((C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R) : R[X])) =
    (C : (a : R) → R[X]) r
neg₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((C : (a : R) → R[X]) ((↑(normUnit r) : R) * (↑(normUnit r)⁻¹ : R)) : R[X]) =
    (C : (a : R) → R[X]) r
neg₂ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) 1 : R[X]) =
    (C : (a : R) → R[X]) r
neg₃ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) (1 : R[X]) = (C : (a : R) → R[X]) r
neg₄ neg₅ : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) r : R[X])
⊢ HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
        ((C : (a : R) → R[X]) (↑(normUnit r) : R) : R[X]))
      ((C : (a : R) → R[X]) (↑(normUnit r)⁻¹ : R) : R[X]) =
    (C : (a : R) → R[X]) r

Tactic:
rw [mul_assoc, ← map_mul, Units.mul_inv, C_1, mul_one]

Premises used: Polynomial.C_1, mul_assoc, Units.mul_inv, map_mul, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart ∣ p

Tactic:
Dvd.intro_left (C p.content) p.eq_C_content_mul_primPart.symm

Premises used: Polynomial.C, Dvd.intro_left, Polynomial.eq_C_content_mul_primPart, Polynomial.content, Eq.symm, DFunLike.coe
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
⊢ Nontrivial S

Tactic:
nontriviality S
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
inst_6 : Nontrivial S
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0

Tactic:
rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp

Premises used: Polynomial.eq_C_content_mul_primPart, map_mul, Polynomial.aeval_C
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
inst_6 : Nontrivial S
hp₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0
⊢ Nontrivial S

Tactic:
rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp

Premises used: Polynomial.eq_C_content_mul_primPart, map_mul, Polynomial.aeval_C
-- 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
⊢ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p.primPart : S) (0 : S)

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 : 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
refine : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) p.content : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p.primPart : S) (0 : S)

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 : 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
⊢ IsDomain R

Tactic:
have : IsDomain R := { Module.nontrivial R S with }