awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
have inl : rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0
Tactic: obtain rfl | h0 := eq_or_ne f 0
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
inl : rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
have inr : ∀ (h0 : f ≠ 0), rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Tactic: obtain rfl | h0 := eq_or_ne f 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
have inr : ∀ (g : R[X])
  (hg :
    f =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f *
        g)
  (ndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ∣ g),
  rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Tactic: obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ∣ g
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
have ndvd₁ : ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r
Tactic: rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd
Cleared hypotheses: ndvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r
| rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f)
have rw : p ^ n * rootMultiplicity (r ^ p ^ n) f
Tactic: rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
have conv_lhs : rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Tactic: conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r
conv_lhs : rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
have inr : p ^ n * rootMultiplicity (r ^ p ^ n) f = p ^ n * rootMultiplicity (r ^ p ^ n) f
Tactic: conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R p : (a : R[X]) → R[X]) f) = p * rootMultiplicity (r ^ p) f
have rw : rootMultiplicity r ((expand R (HPow.hPow (β := ℕ) p 1) : (a : R[X]) → R[X]) f) =
  HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f
Tactic: rw [← pow_one p, rootMultiplicity_expand_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
rw :
  rootMultiplicity r ((expand R (HPow.hPow (β := ℕ) p 1) : (a : R[X]) → R[X]) f) =
    HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f
⊢ rootMultiplicity r ((expand R p : (a : R[X]) → R[X]) f) = p * rootMultiplicity (r ^ p) f
have rw₁ : HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f =
  HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f
Tactic: rw [← pow_one p, rootMultiplicity_expand_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalHom (R := R[X]) (S := R[X]) (F := R[X] →ₐ[R] R[X]) (expand R p)
have refine : ∀ (f : R[X]) (hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])), IsUnit f
Tactic: refine ⟨fun f hf1 => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
⊢ IsUnit f
have hf2 : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
  ((C : (a : R) → R[X]) (coeff ((expand R p : (a : R[X]) → R[X]) f) 0) : R[X])
Tactic: have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
hf2 :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((C : (a : R) → R[X]) (coeff ((expand R p : (a : R[X]) → R[X]) f) 0) : R[X])
⊢ IsUnit f
have hf2₁ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
Cleared hypotheses: hf2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
hf2 : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ IsUnit f
have hf1₁ : IsUnit (f.coeff 0)
Tactic: rw [hf2, isUnit_C] at hf1
Cleared hypotheses: hf1, hf2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ IsUnit f
have hf2₁ : f = (C : (a : R) → R[X]) (f.coeff 0)
Tactic: rw [expand_eq_C hp] at hf2
Cleared hypotheses: hf2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ IsUnit f
have rwa : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: rwa [hf2, isUnit_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible (M := R[X]) ((expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f : R[X])
⊢ Irreducible f
have rwa : ∀ (hf : Irreducible (M := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])), Irreducible f
Tactic: rwa [pow_zero, expand_one] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible (M := R[X]) ((expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f : R[X])
rwa : ∀ (hf : Irreducible (M := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])), Irreducible f
⊢ Irreducible f
have rwa₁ : ∀ (hf : Irreducible f), Irreducible f
Tactic: rwa [pow_zero, expand_one] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n_1 n : ℕ
ih : Irreducible (M := R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f : R[X]) → Irreducible f
hf : Irreducible (M := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
⊢ Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) : R[X])
have hf₁ : Irreducible (M := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
Tactic: rw [pow_succ'] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have pos : ∀ (h : p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
pos : ∀ (h : p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have neg : ∀ (h : ¬p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
h : ¬p = 0
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have neg : ∀ (g : R[X]) (hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p * g)
  (hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g),
  rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
Tactic: obtain ⟨g, hp, hndvd⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h t
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
h : ¬p = 0
g : R[X]
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p * g
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have neg : let m := rootMultiplicity t p;
∀ (hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R))
  (hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g),
  rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = m - 1
Tactic: set m := p.rootMultiplicity t
Cleared hypotheses: hnzd, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = m - 1
have hm : m - 1 + 1 = m
Tactic: have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
have rw : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ (C : (a : R) → R[X]) (↑m : R) * g
Tactic: rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ (C : (a : R) → R[X]) (↑m : R) * g
have rw : ∀ (hndvd : ¬eval t g = 0),
  let m := rootMultiplicity t p;
  ∀ (hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R))
    (hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g) (hm : m - 1 + 1 = m),
    ¬eval t ((C : (a : R) → R[X]) (↑m : R) * g) = 0
Tactic: rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
Cleared hypotheses: hndvd, m, hnzd, hp, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t ((C : (a : R) → R[X]) (↑m : R) * g) = 0
have rwa : ¬eval t ((C : (a : R) → R[X]) (↑m : R)) * eval t g = 0
Tactic: rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
rwa : ¬eval t ((C : (a : R) → R[X]) (↑m : R)) * eval t g = 0
⊢ ¬eval t ((C : (a : R) → R[X]) (↑m : R) * g) = 0
have rwa₁ : ¬(↑m : R) * eval t g = 0
Tactic: rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = m - 1
have hndvd₁ : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
Tactic: have hndvd : ¬(X - C t) ^ m ∣ derivative p := by
    rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
    rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
    rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h_1 : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
have rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = m - 1
have hnezero : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
Tactic: have hnezero : derivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
hnezero : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) ≤ m - 1
have rwa : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - 1 + 1) ∣ (derivative : (a : R[X]) → R[X]) p
Tactic: rwa [rootMultiplicity_le_iff hnezero, hm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ eval t ((⇑derivative : (a : R[X]) → R[X])^[rootMultiplicity t p] p) =
    (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p)
have set : let m := rootMultiplicity t p;
∀ (hm : m = rootMultiplicity t p),
  eval t ((⇑derivative : (a : R[X]) → R[X])^[m] p) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
Tactic: set m := p.rootMultiplicity t with hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
| eval t ((⇑derivative : (a : R[X]) → R[X])^[m] p)
have rw : eval t
  ((⇑derivative : (a : R[X]) → R[X])^[m]
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)))
Tactic: rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative : (a : R[X]) → R[X])^[m] p) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
have conv_lhs : eval t
    ((⇑derivative : (a : R[X]) → R[X])^[m]
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
Tactic: conv_lhs => rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t
      ((⇑derivative : (a : R[X]) → R[X])^[m]
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
have rw : eval t
    (m.choose 0 •
      ((⇑derivative : (a : R[X]) → R[X])^[m - 0]
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
        (⇑derivative : (a : R[X]) → R[X])^[0]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
  m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
Tactic: rw [iterate_derivative_mul, eval_finsetSum, sum_eq_single_of_mem _ (mem_range.mpr m.succ_pos)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
rw :
  eval t
      (m.choose 0 •
        ((⇑derivative : (a : R[X]) → R[X])^[m - 0]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[0]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
⊢ eval t
      ((⇑derivative : (a : R[X]) → R[X])^[m]
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
have rw₁ : ∀ b ∈ range m.succ,
  b ≠ 0 →
    eval t
        (m.choose b •
          ((⇑derivative : (a : R[X]) → R[X])^[m - b]
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
            (⇑derivative : (a : R[X]) → R[X])^[b]
              (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
      0
Tactic: rw [iterate_derivative_mul, eval_finsetSum, sum_eq_single_of_mem _ (mem_range.mpr m.succ_pos)]