awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
⊢ Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0))
      r)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      r)
inr :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (a * r) : R[X]) *
      Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
        r).Splits
inr₁ :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff *
      leadingCoeff
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s)) ≠
    0
⊢ Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (a ::ₘ s)))
      r)

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, mul_scaleRoots', X_add_C_scaleRoots]

Premises used: Multiset.map_cons, Multiset.prod_cons, Polynomial.X_add_C_scaleRoots, Polynomial.mul_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      r)
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (a * r) : R[X]) *
      Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
        r).Splits

Tactic:
.mul (.X_add_C _) IH

Premises used: Polynomial.Splits.X_add_C, Polynomial.Splits.mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      r)
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (a * r) : R[X]) *
      Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
        r).Splits

Tactic:
exact .mul (.X_add_C _) IH
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      r)
inr :
  ¬Eq (α := R[X])
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      0
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff *
      leadingCoeff
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s)) ≠
    0

Tactic:
simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]

Premises used: ne_eq, Polynomial.leadingCoeff_X_add_C, Polynomial.leadingCoeff_eq_zero, one_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      r)
⊢ ¬Eq (α := R[X])
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      0

Tactic:
(monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).ne_zero

Premises used: Polynomial.monic_multiset_prod_of_monic, Polynomial.monic_X_add_C, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      r)
⊢ ¬Eq (α := R[X])
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
      0

Tactic:
exact (monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).ne_zero

Premises used: Polynomial.monic_multiset_prod_of_monic, Polynomial.monic_X_add_C, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
inr :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0))
      r)
inr₁ :
  ∀ (a : R) (s : Multiset R)
    (IH :
      Splits
        (Polynomial.scaleRoots
          (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s))
          r)),
    Splits
      (Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (a ::ₘ s)))
        r)
⊢ Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
      r)

Tactic:
induction m using Multiset.induction_on with
    | empty => simp
    | cons a s IH =>
      rw [Multiset.map_cons, Multiset.prod_cons, mul_scaleRoots', X_add_C_scaleRoots]
      · exact .mul (.X_add_C _) IH
      · simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]
        exact (monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).ne_zero

Premises used: Multiset.map_cons, Multiset.prod_cons, Polynomial.monic_multiset_prod_of_monic, Polynomial.X_add_C_scaleRoots, Polynomial.monic_X_add_C, ne_eq, Polynomial.leadingCoeff_X_add_C, Polynomial.leadingCoeff_eq_zero, Polynomial.mul_scaleRoots', one_mul, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm :
  p =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
inr : HMul.hMul (α := R) (leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff)) 1 ≠ 0
⊢ HMul.hMul (α := R) (leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff))
      (leadingCoeff
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))) ≠
    0

Tactic:
rw [(monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).leadingCoeff]

Premises used: Polynomial.monic_multiset_prod_of_monic, Polynomial.monic_X_add_C, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm :
  p =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ HMul.hMul (α := R) (leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff)) 1 ≠ 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Ring R
r s : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Nontrivial R
a :
  ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff 0 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff 0
a₁ :
  ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (HAdd.hAdd (α := ℕ) 0 1) =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (HAdd.hAdd (α := ℕ) 0 1)
a₂ :
  ∀ (i : ℕ),
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (i + 1 + 1) =
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (i + 1 + 1)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])

Tactic:
ext (_ | _ | i)
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Nontrivial R
⊢ ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff 0 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Nontrivial R
⊢ ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (HAdd.hAdd (α := ℕ) 0 1) =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Nontrivial R
i : ℕ
⊢ ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (i + 1 + 1) =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (i + 1 + 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
inl : Subsingleton R → rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
inr : Nontrivial R → rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Subsingleton R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
simp [Subsingleton.elim p 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
inr : rootMultiplicity (r * a) (scaleRoots 0 r) = rootMultiplicity a 0
inr₁ : ∀ (hp : p ≠ 0), rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
r a : R
hr : IsLeftRegular r
h : Nontrivial R
⊢ rootMultiplicity (r * a) (scaleRoots 0 r) = rootMultiplicity a 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
inr :
  ∀ (q : R[X]) (e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q)
    (hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q),
    rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
obtain ⟨q, e, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp a

Premises used: Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
contrapose : ∀ (hp : q = 0), p = 0
⊢ q ≠ 0

Tactic:
contrapose hp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hp : q = 0
⊢ p = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
⊢ q ≠ 0

Tactic:
have hq0 : q ≠ 0 := by contrapose hp; simp_all
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
rw :
  rootMultiplicity (r * a)
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q).scaleRoots r)
| rootMultiplicity (r * a) (p.scaleRoots r)

Tactic:
rw [e]
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
inr :
  rootMultiplicity (r * a)
      ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q).scaleRoots r) =
    rootMultiplicity a p
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
conv_lhs => rw [e]
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
inr : rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p
inr₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff ^ rootMultiplicity a p ≠ 0
inr₂ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
⊢ rootMultiplicity (r * a)
      ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q).scaleRoots r) =
    rootMultiplicity a p

Tactic:
rw [mul_scaleRoots', pow_scaleRoots', X_sub_C_scaleRoots, mul_comm, mul_comm _ (q.scaleRoots r),
    rootMultiplicity_mul_X_sub_C_pow (q.scaleRoots_ne_zero hq0 _)]

Premises used: Polynomial.rootMultiplicity_mul_X_sub_C_pow, Polynomial.scaleRoots_ne_zero, Polynomial.X_sub_C_scaleRoots, Polynomial.scaleRoots, mul_comm, Polynomial.pow_scaleRoots', Polynomial.mul_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
⊢ ¬eval a q = 0

Tactic:
rw [dvd_iff_isRoot, IsRoot.def] at hq

Premises used: Polynomial.IsRoot.def, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
hq₁ : ¬eval a q = 0
⊢ q ≠ 0

Tactic:
rw [dvd_iff_isRoot, IsRoot.def] at hq

Premises used: Polynomial.IsRoot.def, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬eval a q = 0
hq0 : q ≠ 0
inr : eval (a * r) (q.scaleRoots r) = 0 → q.scaleRoots r = 0
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p

Tactic:
simp only [Nat.add_eq_right, rootMultiplicity_eq_zero_iff, IsRoot.def]

Premises used: Nat.add_eq_right, Polynomial.rootMultiplicity_eq_zero_iff, Polynomial.IsRoot.def
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬eval a q = 0
hq0 : q ≠ 0
inr : eval a q = 0 → q.scaleRoots r = 0
⊢ eval (a * r) (q.scaleRoots r) = 0 → q.scaleRoots r = 0

Tactic:
rw [mul_comm, scaleRoots_eval_mul, (hr.pow q.natDegree).mul_left_eq_zero_iff]

Premises used: IsLeftRegular.mul_left_eq_zero_iff, IsLeftRegular.pow, mul_comm, Polynomial.natDegree, Polynomial.scaleRoots_eval_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬eval a q = 0
hq0 : q ≠ 0
inr : eval a q = 0 → q.scaleRoots r = 0
⊢ eval a q = 0 → q.scaleRoots r = 0

Tactic:
tauto
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff ^ rootMultiplicity a p ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q
hq : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
hq0 : q ≠ 0
inr :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff ^ rootMultiplicity a p *
      q.leadingCoeff ≠
    0
inr₁ : HPow.hPow (α := R) 1 (rootMultiplicity a p) * q.leadingCoeff ≠ 0
inr₂ : 1 * q.leadingCoeff ≠ 0
inr₃ : q.leadingCoeff ≠ 0
inr₄ : ¬q.leadingCoeff = 0
inr₅ inr₆ inr₇ inr₈ : ¬q = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0

Tactic:
rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]

Premises used: one_pow, Polynomial.leadingCoeff_pow', ne_eq, Polynomial.leadingCoeff_X_sub_C, Polynomial.leadingCoeff_eq_zero, one_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : ∀ (a : R), Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
⊢ (p.scaleRoots r).roots = Multiset.map (fun (x : R) ↦ r * x) p.roots

Tactic:
ext a
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : R
⊢ Function.Bijective (β := R) fun (x : R) ↦ r * x

Tactic:
have : Function.Bijective (α := R) (r * ·) := IsUnit.isUnit_iff_mulLeft_bijective.mp hr
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : R
this : Function.Bijective (β := R) fun (x : R) ↦ r * x
a₁ :
  ∀ (a : R),
    Multiset.count ((fun (x : R) ↦ r * x) a) (p.scaleRoots r).roots =
      Multiset.count (α := R) ((fun (x : R) ↦ r * x) a) (Multiset.map (fun (x : R) ↦ r * x) p.roots)
⊢ Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)

Tactic:
obtain ⟨a, rfl⟩ := this.2 a

Premises used: And.right, rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
this : Function.Bijective (β := R) fun (x : R) ↦ r * x
a : R
⊢ Multiset.count ((fun (x : R) ↦ r * x) a) (p.scaleRoots r).roots =
    Multiset.count (α := R) ((fun (x : R) ↦ r * x) a) (Multiset.map (fun (x : R) ↦ r * x) p.roots)

Tactic:
simp [Multiset.count_map_eq_count' _ p.roots this.1 a,
    rootMultiplicity_scaleRoots _ hr.isRegular.left]

Premises used: Polynomial.rootMultiplicity_scaleRoots, Polynomial.roots, And.left, IsUnit.isRegular, IsRegular.left, Multiset.count_map_eq_count'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : ∀ (a : R), Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
a₁ :
  ∀ (a : R) (this : Function.Bijective (β := R) fun (x : R) ↦ r * x),
    Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
a₂ :
  ∀ (this : Function.Bijective (β := R) fun (x : R) ↦ r * x) (a : R),
    Multiset.count ((fun (x : R) ↦ r * x) a) (p.scaleRoots r).roots =
      Multiset.count (α := R) ((fun (x : R) ↦ r * x) a) (Multiset.map (fun (x : R) ↦ r * x) p.roots)
⊢ (p.scaleRoots r).roots = Multiset.map (fun (x : R) ↦ r * x) p.roots

Tactic:
classical
  ext a
  have : Function.Bijective (α := R) (r * ·) := IsUnit.isUnit_iff_mulLeft_bijective.mp hr
  obtain ⟨a, rfl⟩ := this.2 a
  simp [Multiset.count_map_eq_count' _ p.roots this.1 a,
    rootMultiplicity_scaleRoots _ hr.isRegular.left]

Premises used: Polynomial.rootMultiplicity_scaleRoots, IsUnit.isRegular, IsRegular.left, rfl
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
⊢ HPow.hPow (β := ℕ) z 3 = 1

Tactic:
linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
⊢ HPow.hPow (β := ℕ) z 3 = 1

Tactic:
replace h3 : z ^ 3 = 1 := by
    linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2
-- Module: Mathlib.RingTheory.Polynomial.Selmer
Goal:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + HPow.hPow (β := ℕ) z 2 = 0
h3 : HPow.hPow (β := ℕ) z 3 = 1
rw : z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = HPow.hPow (β := ℕ) z 2
⊢ z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = HPow.hPow (β := ℕ) z 2

Tactic:
rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]

Premises used: one_pow, pow_add, pow_mul, Nat.mod_add_div, mul_one, OfNat.ofNat