awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
have rw₁ : HMul.hMul (β := R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f))
    ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X p) : R[X]) =
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
Tactic: rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₁ :
  HMul.hMul (β := R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f))
      ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X p) : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
have rw₂ : eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑p : R) * HPow.hPow (α := R[X]) X (p - 1))
      ((derivative : (a : R[X]) → R[X]) X : R[X]) =
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
Tactic: rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₁ :
  HMul.hMul (β := R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f))
      ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X p) : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₂ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑p : R) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
have rw₃ : eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    HMul.hMul (β := R[X]) ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1)) ((derivative : (a : R[X]) → R[X]) X : R[X]) =
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
Tactic: rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₁ :
  HMul.hMul (β := R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f))
      ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X p) : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₂ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑p : R) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₃ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
have rw₄ : eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1) * 1) =
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
Tactic: rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₁ :
  HMul.hMul (β := R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f))
      ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X p) : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₂ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑p : R) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₃ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₄ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1) * 1) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
have rw₅ : eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1)) =
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
Tactic: rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) n = if p ∣ n then f.coeff (n / p) else 0
have simp : coeff
    (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X p ^ e))
    n =
  if p ∣ n then f.coeff (n / p) else 0
Tactic: simp only [expand_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff
      (f.sum fun (e : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X p ^ e))
      n =
    if p ∣ n then f.coeff (n / p) else 0
have simp_rw : (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0
Tactic: simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0
have pos : ∀ (h : p ∣ n), (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
pos : ∀ (h : p ∣ n), (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0
have neg : ∀ (h : ¬p ∣ n), Eq.{u + 1} (α := R) (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)
have pos : ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0
Tactic: rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
pos : ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)
have pos₁ : n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0
Tactic: rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
⊢ (if p * b = n then f.coeff b else 0) = 0
have pos : ¬p * b = n
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ False
have pos : b = n / p
Tactic: apply hb2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ b = n / p
have pos : b = p * b / p
Tactic: rw [← hb3, Nat.mul_div_cancel_left b hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
pos : b = p * b / p
⊢ b = n / p
have pos₁ : b = b
Tactic: rw [← hb3, Nat.mul_div_cancel_left b hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = 0
have pos : Eq.{u + 1} (α := R) (if p * (n / p) = n then 0 else 0) 0
Tactic: rw [notMem_support_iff.1 hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ Eq.{u + 1} (α := R) (if p * (n / p) = n then 0 else 0) 0
have pos : p * (n / p) = n → Eq.{u + 1} (α := R) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
pos : p * (n / p) = n → Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (if p * (n / p) = n then 0 else 0) 0
have neg : ¬p * (n / p) = n → Eq.{u + 1} (α := R) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ Eq.{u + 1} (α := R) (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) 0
have neg : ∀ x ∈ f.support, (if p * x = n then f.coeff x else 0) = 0
Tactic: rw [Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
h_1 : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0
have neg : ¬p * k = n
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n
have rw : (if p ∣ n * p then f.coeff (n * p / p) else 0) = f.coeff n
Tactic: rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
rw : (if p ∣ n * p then f.coeff (n * p / p) else 0) = f.coeff n
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n
have rw₁ : f.coeff (n * p / p) = f.coeff n
Tactic: rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
rw : (if p ∣ n * p then f.coeff (n * p / p) else 0) = f.coeff n
rw₁ : f.coeff (n * p / p) = f.coeff n
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n
have rw₂ : f.coeff n = f.coeff n
Tactic: rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (p * n) = f.coeff n
have rw : coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n
Tactic: rw [mul_comm, coeff_expand_mul hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
rw : coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (p * n) = f.coeff n
have rw₁ : f.coeff n = f.coeff n
Tactic: rw [mul_comm, coeff_expand_mul hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : Eq (α := R[X]) ((expand R n : (a : R[X]) → R[X]) g : R[X]) ((expand R n : (a : R[X]) → R[X]) g' : R[X])
k : ℕ
⊢ g.coeff k = g'.coeff k
have rw : coeff ((expand R n : (a : R[X]) → R[X]) g) (k * n) = g'.coeff k
Tactic: rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : Eq (α := R[X]) ((expand R n : (a : R[X]) → R[X]) g : R[X]) ((expand R n : (a : R[X]) → R[X]) g' : R[X])
k : ℕ
rw : coeff ((expand R n : (a : R[X]) → R[X]) g) (k * n) = g'.coeff k
⊢ g.coeff k = g'.coeff k
have rw₁ : coeff ((expand R n : (a : R[X]) → R[X]) g') (k * n) = g'.coeff k
Tactic: rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : Eq (α := R[X]) ((expand R n : (a : R[X]) → R[X]) g : R[X]) ((expand R n : (a : R[X]) → R[X]) g' : R[X])
k : ℕ
rw : coeff ((expand R n : (a : R[X]) → R[X]) g) (k * n) = g'.coeff k
rw₁ : coeff ((expand R n : (a : R[X]) → R[X]) g') (k * n) = g'.coeff k
⊢ g.coeff k = g'.coeff k
have rw₂ : g'.coeff k = g'.coeff k
Tactic: rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) r : R[X]) ↔
    f = (C : (a : R) → R[X]) r
have rw : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ↔
  f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
Tactic: rw [← expand_C, expand_inj hp, expand_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ↔
    f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
p₁ : ℕ
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) r : R[X]) ↔
    f = (C : (a : R) → R[X]) r
have rw₁ : f = (C : (a : R) → R[X]) r ↔ f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
Tactic: rw [← expand_C, expand_inj hp, expand_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ↔
    f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
p₁ : ℕ
rw₁ : f = (C : (a : R) → R[X]) r ↔ f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) r : R[X]) ↔
    f = (C : (a : R) → R[X]) r
have rw₂ : f = (C : (a : R) → R[X]) r ↔ f = (C : (a : R) → R[X]) r
Tactic: rw [← expand_C, expand_inj hp, expand_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl : ∀ (hp : p = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
Tactic: rcases p.eq_zero_or_pos with hp | hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
inl : ∀ (hp : p = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inr : ∀ (hp : p > 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
Tactic: rcases p.eq_zero_or_pos with hp | hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl₂ : (eval₂ C 1 f).natDegree = f.natDegree * 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
inl₂ : (eval₂ C 1 f).natDegree = f.natDegree * 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl₃ : (eval₂ C 1 f).natDegree = 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
inl₂ : (eval₂ C 1 f).natDegree = f.natDegree * 0
inl₃ : (eval₂ C 1 f).natDegree = 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl₄ : (eval₂ C ((C : (a : R) → R[X]) 1) f).natDegree = 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
inl₂ : (eval₂ C 1 f).natDegree = f.natDegree * 0
inl₃ : (eval₂ C 1 f).natDegree = 0
inl₄ : (eval₂ C ((C : (a : R) → R[X]) 1) f).natDegree = 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl₅ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval 1 f)) = 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
inl₂ : (eval₂ C 1 f).natDegree = f.natDegree * 0
inl₃ : (eval₂ C 1 f).natDegree = 0
inl₄ : (eval₂ C ((C : (a : R) → R[X]) 1) f).natDegree = 0
inl₅ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval 1 f)) = 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have inl₆ : Eq (α := ℕ) 0 0
Tactic: rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have pos : ∀ (hf : f = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
pos : ∀ (hf : f = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have neg : ∀ (hf : ¬f = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have pos : natDegree (R := R) ((expand R p : (a : R[X]) → R[X]) 0) = natDegree.{u} (R := R) 0 * p
Tactic: rw [hf, map_zero, natDegree_zero, zero_mul]