awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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)
have 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
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, mul_scaleRoots', X_add_C_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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[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
have 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
Tactic: simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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)
have 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)
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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))
      (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
have inr : HMul.hMul (α := R) (leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff)) 1 ≠ 0
Tactic: rw [(monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r s : R
⊢ (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])
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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 =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])
have 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
Tactic: ext (_ | _ | i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (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])
have 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)
Tactic: ext (_ | _ | i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ (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])
have 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)
Tactic: ext (_ | _ | i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have inl : Subsingleton R → rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have inr : Nontrivial R → rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have inr : rootMultiplicity (r * a) (scaleRoots 0 r) = rootMultiplicity a 0
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have inr₁ : ∀ (hp : p ≠ 0), rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h : Nontrivial R
hp : p ≠ 0
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have 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
Tactic: obtain ⟨q, e, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have contrapose : ∀ (hp : q = 0), p = 0
Tactic: contrapose hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
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
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have hq0 : q ≠ 0
Tactic: have hq0 : q ≠ 0 := by contrapose hp; simp_all
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
| rootMultiplicity (r * a) (p.scaleRoots r)
have 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)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
have 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
Tactic: conv_lhs => rw [e]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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
have inr : rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = 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 _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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
have inr₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff ^ rootMultiplicity a p ≠ 0
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 _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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
have inr₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
    q.leadingCoeff ≠
  0
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 _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
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
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p
have hq₁ : ¬eval a q = 0
Tactic: rw [dvd_iff_isRoot, IsRoot.def] at hq
Cleared hypotheses: hq, hq0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p
have inr : eval (a * r) (q.scaleRoots r) = 0 → q.scaleRoots r = 0
Tactic: simp only [Nat.add_eq_right, rootMultiplicity_eq_zero_iff, IsRoot.def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ eval (a * r) (q.scaleRoots r) = 0 → q.scaleRoots r = 0
have inr : eval a q = 0 → q.scaleRoots r = 0
Tactic: rw [mul_comm, scaleRoots_eval_mul, (hr.pow q.natDegree).mul_left_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
have inr : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff ^ rootMultiplicity a p *
    q.leadingCoeff ≠
  0
Tactic: rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
have inr₁ : HPow.hPow (α := R) 1 (rootMultiplicity a p) * q.leadingCoeff ≠ 0
Tactic: rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
have inr₂ : 1 * q.leadingCoeff ≠ 0
Tactic: rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
have inr₃ : q.leadingCoeff ≠ 0
Tactic: rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
have inr₄ : ¬q.leadingCoeff = 0
Tactic: rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).leadingCoeff *
      q.leadingCoeff ≠
    0
have inr₅ : ¬q = 0
Tactic: rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).roots = Multiset.map (fun (x : R) ↦ r * x) p.roots
have a : ∀ (a : R), Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : R
⊢ Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
have this : Function.Bijective (β := R) fun (x : R) ↦ r * x
Tactic: have : Function.Bijective (α := R) (r * ·) := IsUnit.isUnit_iff_mulLeft_bijective.mp hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun (x : R) ↦ r * x) p.roots)
have 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)
Tactic: obtain ⟨a, rfl⟩ := this.2 a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).roots = Multiset.map (fun (x : R) ↦ r * x) p.roots
have a : ∀ (a : R), Multiset.count a (p.scaleRoots r).roots = Multiset.count a (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]