awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ ∃ (q : R[X]),
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
          q =
        p ∧
      p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
have obtain : ∀ (q : R[X])
  (he :
    p =
      prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
        q),
  ∃ (q : R[X]),
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
          q =
        p ∧
      p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
Tactic: obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
⊢ ∃ (q : R[X]),
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
          q =
        p ∧
      p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
have right : p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
Tactic: use q, he.symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
have right : ∀
  (he :
    p =
      HMul.hMul (α := R[X])
        (prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
        0),
  p.roots.card + natDegree.{u} (R := R) 0 = p.natDegree ∧ Eq.{u + 1} (α := Multiset R) (roots 0) 0
Tactic: obtain rfl | hq := eq_or_ne q 0
Cleared hypotheses: q, he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
right :
  ∀
    (he :
      p =
        HMul.hMul (α := R[X])
          (prod
            (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
          0),
    p.roots.card + natDegree.{u} (R := R) 0 = p.natDegree ∧ Eq.{u + 1} (α := Multiset R) (roots 0) 0
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
have right₁ : ∀ (hq : q ≠ 0), p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
Tactic: obtain rfl | hq := eq_or_ne q 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
he :
  p =
    HMul.hMul (α := R[X])
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
      0
⊢ p.roots.card + natDegree.{u} (R := R) 0 = p.natDegree ∧ Eq.{u + 1} (α := Multiset R) (roots 0) 0
have he₁ : p = 0
Tactic: rw [mul_zero] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
he : p = 0
⊢ p.roots.card + natDegree.{u} (R := R) 0 = p.natDegree ∧ Eq.{u + 1} (α := Multiset R) (roots 0) 0
have right : Multiset.card.{u} (α := R) (roots 0) + natDegree.{u} (R := R) 0 = natDegree.{u} (R := R) 0 ∧
  Eq.{u + 1} (α := Multiset R) (roots 0) 0
Tactic: subst he
Cleared hypotheses: p, he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
have right : p.roots.card + q.natDegree = p.natDegree
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
right : p.roots.card + q.natDegree = p.natDegree
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
have right₁ : q.roots = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
| p.natDegree
have rw : (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
    q).natDegree
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree
have right : p.roots.card + q.natDegree =
  (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
      q).natDegree
Tactic: conv_rhs => rw [he]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree =
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
        q).natDegree
have right : p.roots.card + q.natDegree =
  natDegree (R := R)
      (prod
        (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)) +
    q.natDegree
Tactic: rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,
      natDegree_multiset_prod_X_sub_C_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
right :
  p.roots.card + q.natDegree =
    natDegree (R := R)
        (prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)) +
      q.natDegree
⊢ p.roots.card + q.natDegree =
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
        q).natDegree
have right₁ : p.roots.card + q.natDegree = p.roots.card + q.natDegree
Tactic: rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,
      natDegree_multiset_prod_X_sub_C_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
he :
  p =
    prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q
hq : q ≠ 0
⊢ q.roots = 0
have he₁ : (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
      q).roots =
  p.roots
Tactic: replace he := congr_arg roots he.symm
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hq : q ≠ 0
he :
  (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
        q).roots =
    p.roots
⊢ q.roots = 0
have right : ∀ (he : p.roots + q.roots = p.roots), q.roots = 0
Tactic: rw [roots_mul, roots_multiset_prod_X_sub_C] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hq : q ≠ 0
he :
  (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) *
        q).roots =
    p.roots
right : ∀ (he : p.roots + q.roots = p.roots), q.roots = 0
⊢ q.roots = 0
have right₁ : prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) * q ≠ 0
Tactic: rw [roots_mul, roots_multiset_prod_X_sub_C] at he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) = p
have h : prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
      R[X])
Tactic: convert! C_leadingCoeff_mul_prod_multiset_X_sub_C hroots
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
        R[X])
have h : prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1)
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
Tactic: rw [hp.leadingCoeff, C_1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
h :
  prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1)
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
        R[X])
have h₁ : prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
  HMul.hMul (α := R[X]) 1
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
Tactic: rw [hp.leadingCoeff, C_1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
h :
  prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1)
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
h₁ :
  prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
    HMul.hMul (α := R[X]) 1
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
        R[X])
have h₂ : Eq (α := R[X])
  (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
  (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots))
Tactic: rw [hp.leadingCoeff, C_1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hirr : Irreducible p
⊢ p.roots.card ≤ 1
have inl : ∀ (hp : p.roots = 0), p.roots.card ≤ 1
Tactic: obtain hp | ⟨x, hx⟩ := p.roots.empty_or_exists_mem
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hirr : Irreducible p
inl : ∀ (hp : p.roots = 0), p.roots.card ≤ 1
⊢ p.roots.card ≤ 1
have inr : ∀ (x : R) (hx : x ∈ p.roots), p.roots.card ≤ 1
Tactic: obtain hp | ⟨x, hx⟩ := p.roots.empty_or_exists_mem
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hirr : Irreducible p
x : R
hx : x ∈ p.roots
⊢ p.roots.card ≤ 1
have h : 1 = p.natDegree
Tactic: convert! p.card_roots'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hirr : Irreducible p
hdeg : p.natDegree ≠ 1
⊢ p.roots = 0
have by_contra : ∀ (hroots : ¬p.roots = 0), False
Tactic: by_contra hroots
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hirr : Irreducible p
hdeg : p.natDegree ≠ 1
hroots : ¬p.roots = 0
⊢ False
have have : ∀ (x : R) (hx : x ∈ p.roots), False
Tactic: have ⟨x, hx⟩ := exists_mem_of_ne_zero hroots
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
have simp : (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p) ↔
  ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
Tactic: simp only [p_monic.irreducible_iff_lt_natDegree_lt p_1, Finset.mem_Ioc, and_imp,
    natDegree_pos_iff_degree_pos, natDegree_le_iff_degree_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p) ↔
    ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
have mp : (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p) →
  ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
mp :
  (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p) →
    ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p) ↔
    ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
have mpr : (∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q) →
  ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
⊢ IsUnit q
have mp : ∀ (q_unit : ¬IsUnit q), False
Tactic: by_contra q_unit
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
⊢ False
have this : 0 < q.degree
Tactic: have := degree_pos_of_not_isUnit_of_dvd_monic p_monic q_unit dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
⊢ False
have hu : IsUnit q.leadingCoeff
Tactic: have hu := p_monic.isUnit_leadingCoeff_of_dvd dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ False
have mp : 0 < (hu.unit⁻¹ • q).degree
Tactic: refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
mp : 0 < (hu.unit⁻¹ • q).degree
⊢ False
have mp₁ : (hu.unit⁻¹ • q).degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
Tactic: refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
mp : 0 < (hu.unit⁻¹ • q).degree
mp₁ : (hu.unit⁻¹ • q).degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
⊢ False
have mp₂ : hu.unit⁻¹ • q ∣ q
Tactic: refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q
have mp : (↑hu.unit⁻¹ : R) • q ∣ q
Tactic: rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
mp : (↑hu.unit⁻¹ : R) • q ∣ q
⊢ hu.unit⁻¹ • q ∣ q
have mp₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑hu.unit⁻¹ : R) : R[X]) q ∣ q
Tactic: rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
mp : (↑hu.unit⁻¹ : R) • q ∣ q
mp₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑hu.unit⁻¹ : R) : R[X]) q ∣ q
⊢ hu.unit⁻¹ • q ∣ q
have mp₂ : q ∣ q
Tactic: rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ rootMultiplicity a p ≤ rootMultiplicity ((f : (a : A) → B) a) (map f p)
have rw : HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣ map f p
Tactic: rw [le_rootMultiplicity_iff hmap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
    map f p
have refine : HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
  (mapRingHom f : (a : A[X]) → B[X])
    (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]) ^ rootMultiplicity a p)
Tactic: refine _root_.trans ?_ (_root_.map_dvd (mapRingHom f) (pow_rootMultiplicity_dvd p a))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
    (mapRingHom f : (a : A[X]) → B[X])
      (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]) ^ rootMultiplicity a p)
have rw : HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
  HPow.hPow (α := B[X])
    ((mapRingHom f : (a : A[X]) → B[X]) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])) : B[X])
    (rootMultiplicity a p)
Tactic: rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
rw :
  HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
    HPow.hPow (α := B[X])
      ((mapRingHom f : (a : A[X]) → B[X]) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])) : B[X])
      (rootMultiplicity a p)
⊢ HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
    (mapRingHom f : (a : A[X]) → B[X])
      (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]) ^ rootMultiplicity a p)
have rw₁ : HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X]) ^ rootMultiplicity a p ∣
  HSub.hSub (α := B[X]) (β := B[X]) ((mapRingHom f : (a : A[X]) → B[X]) X : B[X])
      ((mapRingHom f : (a : A[X]) → B[X]) ((C : (a : A) → A[X]) a) : B[X]) ^
    rootMultiplicity a p
Tactic: rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]