awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).coeff (d + n) = p.coeff d * r
rw₁ :
  (p * HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
rw₂ :
  (HMul.hMul (β := R[X]) (p * HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
rw₃ : (p * HPow.hPow (α := R[X]) X n).coeff (d + n) * r = p.coeff d * r
⊢ (HMul.hMul (β := R[X]) p ((monomial n : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
have rw₄ : p.coeff d * r = p.coeff d * r
Tactic: rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).coeff (d + n) = r * p.coeff d
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * p).coeff (d + n) = r * p.coeff d
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * p).coeff (d + n) = r * p.coeff d
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).coeff (d + n) = r * p.coeff d
have rw₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * p)).coeff (d + n) = r * p.coeff d
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * p).coeff (d + n) = r * p.coeff d
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * p)).coeff (d + n) = r * p.coeff d
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).coeff (d + n) = r * p.coeff d
have rw₂ : r * (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = r * p.coeff d
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * p).coeff (d + n) = r * p.coeff d
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * p)).coeff (d + n) = r * p.coeff d
rw₂ : r * (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = r * p.coeff d
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).coeff (d + n) = r * p.coeff d
have rw₃ : r * (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = r * p.coeff d
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * p).coeff (d + n) = r * p.coeff d
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * p)).coeff (d + n) = r * p.coeff d
rw₂ : r * (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = r * p.coeff d
rw₃ : r * (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = r * p.coeff d
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).coeff (d + n) = r * p.coeff d
have rw₄ : r * p.coeff d = r * p.coeff d
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ IsRegular (HPow.hPow (α := R[X]) X n)
have suffices : IsLeftRegular (HPow.hPow (α := R[X]) X n)
Tactic: suffices IsLeftRegular (X ^ n : R[X]) from
    ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
hPQ : HPow.hPow (α := R[X]) X n * P = HPow.hPow (α := R[X]) X n * Q
⊢ P = Q
have a : ∀ (i : ℕ), P.coeff i = Q.coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
hPQ : HPow.hPow (α := R[X]) X n * P = HPow.hPow (α := R[X]) X n * Q
i : ℕ
⊢ P.coeff i = Q.coeff i
have a : (HPow.hPow (α := R[X]) X n * P).coeff (i + n) = Q.coeff i
Tactic: rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
hPQ : HPow.hPow (α := R[X]) X n * P = HPow.hPow (α := R[X]) X n * Q
i : ℕ
a : (HPow.hPow (α := R[X]) X n * P).coeff (i + n) = Q.coeff i
⊢ P.coeff i = Q.coeff i
have a₁ : (HPow.hPow (α := R[X]) X n * Q).coeff (i + n) = Q.coeff i
Tactic: rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
hPQ : HPow.hPow (α := R[X]) X n * P = HPow.hPow (α := R[X]) X n * Q
i : ℕ
a : (HPow.hPow (α := R[X]) X n * P).coeff (i + n) = Q.coeff i
a₁ : (HPow.hPow (α := R[X]) X n * Q).coeff (i + n) = Q.coeff i
⊢ P.coeff i = Q.coeff i
have a₂ : Q.coeff i = Q.coeff i
Tactic: rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).coeff k = r ^ (n - k) * (↑(n.choose k) : R)
have rw : ∑ x ∈ range (n + 1),
    (lcoeff R k : (a : R[X]) → R)
      (HPow.hPow (α := R[X]) X x * HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (n - x) *
        (↑(n.choose x) : R[X])) =
  r ^ (n - k) * (↑(n.choose k) : R)
Tactic: rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, map_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1),
      (lcoeff R k : (a : R[X]) → R)
        (HPow.hPow (α := R[X]) X x * HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (n - x) *
          (↑(n.choose x) : R[X])) =
    r ^ (n - k) * (↑(n.choose k) : R)
have simp : ∑ x ∈ range (n + 1), (HPow.hPow (α := R[X]) X x).coeff k * r ^ (n - x) * (↑(n.choose x) : R) =
  r ^ (n - k) * (↑(n.choose k) : R)
Tactic: simp only [lcoeff_apply, ← C_eq_natCast, ← C_pow, coeff_mul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1), (HPow.hPow (α := R[X]) X x).coeff k * r ^ (n - x) * (↑(n.choose x) : R) =
    r ^ (n - k) * (↑(n.choose k) : R)
have h₀ : ∀ b ∈ range (n + 1), b ≠ k → (HPow.hPow (α := R[X]) X b).coeff k * r ^ (n - b) * (↑(n.choose b) : R) = 0
Tactic: rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h₀ : ∀ b ∈ range (n + 1), b ≠ k → (HPow.hPow (α := R[X]) X b).coeff k * r ^ (n - b) * (↑(n.choose b) : R) = 0
⊢ ∑ x ∈ range (n + 1), (HPow.hPow (α := R[X]) X x).coeff k * r ^ (n - x) * (↑(n.choose x) : R) =
    r ^ (n - k) * (↑(n.choose k) : R)
have h₁ : k ∉ range (n + 1) → (HPow.hPow (α := R[X]) X k).coeff k * r ^ (n - k) * (↑(n.choose k) : R) = 0
Tactic: rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (HPow.hPow (α := R[X]) X k).coeff k * r ^ (n - k) * (↑(n.choose k) : R) = 0
have h₁ : n + 1 ≤ k → r ^ (n - k) * (↑(n.choose k) : R) = 0
Tactic: simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * (↑(n.choose k) : R) = 0
have h₁ : r ^ (n - k) * (↑0 : R) = 0
Tactic: rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
h₁ : r ^ (n - k) * (↑0 : R) = 0
⊢ r ^ (n - k) * (↑(n.choose k) : R) = 0
have h₂ : r ^ (n - k) * 0 = 0
Tactic: rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
h₁ : r ^ (n - k) * (↑0 : R) = 0
h₂ : r ^ (n - k) * 0 = 0
⊢ r ^ (n - k) * (↑(n.choose k) : R) = 0
have h₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
⊢ (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
have rw : (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) ^ n).coeff k = (↑(n.choose k) : R)
Tactic: rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
rw : (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) ^ n).coeff k = (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
have rw₁ : HPow.hPow (α := R) 1 (n - k) * (↑(n.choose k) : R) = (↑(n.choose k) : R)
Tactic: rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
rw : (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) ^ n).coeff k = (↑(n.choose k) : R)
rw₁ : HPow.hPow (α := R) 1 (n - k) * (↑(n.choose k) : R) = (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
have rw₂ : HMul.hMul (α := R) 1 (↑(n.choose k) : R) = (↑(n.choose k) : R)
Tactic: rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
rw : (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) ^ n).coeff k = (↑(n.choose k) : R)
rw₁ : HPow.hPow (α := R) 1 (n - k) * (↑(n.choose k) : R) = (↑(n.choose k) : R)
rw₂ : HMul.hMul (α := R) 1 (↑(n.choose k) : R) = (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
have rw₃ : Eq.{u_1 + 1} (α := R) (↑(n.choose k) : R) (↑(n.choose k) : R)
Tactic: rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
⊢ (HAdd.hAdd (α := R[X]) 1 X ^ n).coeff k = (↑(n.choose k) : R)
have rw : (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
Tactic: rw [add_comm _ X, coeff_X_add_one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
rw : (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) 1 X ^ n).coeff k = (↑(n.choose k) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (↑(n.choose k) : R) (↑(n.choose k) : R)
Tactic: rw [add_comm _ X, coeff_X_add_one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ HAdd.hAdd (α := S[X]) 1 X ^ d - HPow.hPow (α := S[X]) X d = ∑ i ∈ range d, d.choose i • HPow.hPow (α := S[X]) X i
have a : ∀ (i : ℕ),
  (HAdd.hAdd (α := S[X]) 1 X ^ d - HPow.hPow (α := S[X]) X d).coeff i =
    coeff (∑ i ∈ range d, d.choose i • HPow.hPow (α := S[X]) X i) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
⊢ (HAdd.hAdd (α := S[X]) 1 X ^ d - HPow.hPow (α := S[X]) X d).coeff i =
    coeff (∑ i ∈ range d, d.choose i • HPow.hPow (α := S[X]) X i) i
have a : HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0
Tactic: simp [Polynomial.coeff_one_add_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0
have pos : i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = (↑(d.choose i) : S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
pos : i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = (↑(d.choose i) : S)
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0
have neg : i = d → ¬i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
pos : i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = (↑(d.choose i) : S)
neg : i = d → ¬i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = 0
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0
have pos₁ : ¬i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 0 = (↑(d.choose i) : S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
pos : i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = (↑(d.choose i) : S)
neg : i = d → ¬i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = 0
pos₁ : ¬i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 0 = (↑(d.choose i) : S)
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0
have neg₁ : ¬i = d → ¬i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
⊢ (C : (a : R) → R[X]) r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i
have mp : (C : (a : R) → R[X]) r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
mp : (C : (a : R) → R[X]) r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i
⊢ (C : (a : R) → R[X]) r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i
have mpr : (∀ (i : ℕ), r ∣ φ.coeff i) → (C : (a : R) → R[X]) r ∣ φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) φ).coeff c
have mp : r ∣ r * φ.coeff c
Tactic: rw [coeff_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ φ.coeff i
⊢ (C : (a : R) → R[X]) r ∣ φ
have mpr : ∀ (c : (i : ℕ) → R) (hc : ∀ (i : ℕ), φ.coeff i = r * c i), (C : (a : R) → R[X]) r ∣ φ
Tactic: choose c hc using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
⊢ (C : (a : R) → R[X]) r ∣ φ
have h : φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
Tactic: use ψ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
⊢ φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
have h : ∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
⊢ φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
have h : φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
Tactic: simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
⊢ φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
have pos : ∀ (hi : φ.coeff i ≠ 0), φ.coeff i = r * c i
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
pos : ∀ (hi : φ.coeff i ≠ 0), φ.coeff i = r * c i
⊢ φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
have neg : ∀ (hi : ¬φ.coeff i ≠ 0), φ.coeff i = r * 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
hi : φ.coeff i ≠ 0
⊢ φ.coeff i = r * c i
have pos : r * c i = r * c i
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (hypothesis)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0
have hi₁ : φ.coeff i = 0
Tactic: rw [Classical.not_not] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
mpr mpr₁ mpr₂ mpr₃ : (C : (a : R) → R[X]) r ∣ φ
⊢ (C : (a : R) → R[X]) r ∣ φ
have h : let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
Tactic: classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
mpr mpr₁ mpr₂ mpr₃ : (C : (a : R) → R[X]) r ∣ φ
h :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
⊢ (C : (a : R) → R[X]) r ∣ φ
have h₁ : let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
Tactic: classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
mpr mpr₁ mpr₂ mpr₃ : (C : (a : R) → R[X]) r ∣ φ
h :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
h₁ :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  ∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
⊢ (C : (a : R) → R[X]) r ∣ φ
have h₂ : ∀ (i : ℕ), φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
Tactic: classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
mpr mpr₁ mpr₂ mpr₃ : (C : (a : R) → R[X]) r ∣ φ
h :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
h₁ :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  ∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
h₂ : ∀ (i : ℕ), φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
⊢ (C : (a : R) → R[X]) r ∣ φ
have pos : ∀ (i : ℕ) (hi : φ.coeff i ≠ 0), φ.coeff i = r * c i
Tactic: classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
mpr mpr₁ mpr₂ mpr₃ : (C : (a : R) → R[X]) r ∣ φ
h :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
h₁ :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  ∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
h₂ : ∀ (i : ℕ), φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
pos : ∀ (i : ℕ) (hi : φ.coeff i ≠ 0), φ.coeff i = r * c i
⊢ (C : (a : R) → R[X]) r ∣ φ
have neg : ∀ (i : ℕ) (hi : ¬φ.coeff i ≠ 0), φ.coeff i = r * 0
Tactic: classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
⊢ p.update n a = p + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a - p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)
have a₁ : ∀ (n_1 : ℕ),
  (p.update n a).coeff n_1 =
    (p + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a - p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n_1
Tactic: ext