awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
⊢ Eq.{u_2 + 1} (α := M) (Finsupp.sum (p.homogenize p.natDegree) fun (x : Fin 2 →₀ ℕ) (c : R) ↦ f c)
    (p.sum fun (x : ℕ) (c : R) ↦ f c)
have rw : Eq.{u_2 + 1} (α := M) (∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)))
  (∑ n ∈ p.support, f (p.coeff n))
Tactic: rw [MvPolynomial.sum_def, sum_def p]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
⊢ Eq.{u_2 + 1} (α := M) (∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)))
    (∑ n ∈ p.support, f (p.coeff n))
have refine_1 : ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
  (fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s ∈ p.support
Tactic: refine Finset.sum_nbij' (fun s ↦ s 0) (fun n ↦ fun₀ | 0 => n | 1 => p.natDegree - n)
    (fun s hs ↦ ?_) (fun n hn ↦ ?_) (fun s hs ↦ ?_) (fun n hn ↦ by simp)
    fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
refine_1 :
  ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
    (fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s ∈ p.support
⊢ Eq.{u_2 + 1} (α := M) (∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)))
    (∑ n ∈ p.support, f (p.coeff n))
have refine_2 : ∀ (n : ℕ) (hn : n ∈ p.support),
  (fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ)) n ∈ (p.homogenize p.natDegree).support
Tactic: refine Finset.sum_nbij' (fun s ↦ s 0) (fun n ↦ fun₀ | 0 => n | 1 => p.natDegree - n)
    (fun s hs ↦ ?_) (fun n hn ↦ ?_) (fun s hs ↦ ?_) (fun n hn ↦ by simp)
    fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
refine_1 :
  ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
    (fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s ∈ p.support
refine_2 :
  ∀ (n : ℕ) (hn : n ∈ p.support),
    (fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ)) n ∈ (p.homogenize p.natDegree).support
⊢ Eq.{u_2 + 1} (α := M) (∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)))
    (∑ n ∈ p.support, f (p.coeff n))
have refine_3 : ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
  (fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ))
      ((fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s) =
    s
Tactic: refine Finset.sum_nbij' (fun s ↦ s 0) (fun n ↦ fun₀ | 0 => n | 1 => p.natDegree - n)
    (fun s hs ↦ ?_) (fun n hn ↦ ?_) (fun s hs ↦ ?_) (fun n hn ↦ by simp)
    fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
refine_1 :
  ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
    (fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s ∈ p.support
refine_2 :
  ∀ (n : ℕ) (hn : n ∈ p.support),
    (fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ)) n ∈ (p.homogenize p.natDegree).support
refine_3 :
  ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
    (fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ))
        ((fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s) =
      s
⊢ Eq.{u_2 + 1} (α := M) (∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)))
    (∑ n ∈ p.support, f (p.coeff n))
have refine_4 : ∀ (s : Fin 2 →₀ ℕ) (hs : s ∈ (p.homogenize p.natDegree).support),
  f (MvPolynomial.coeff s (p.homogenize p.natDegree)) =
    f (p.coeff ((fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s))
Tactic: refine Finset.sum_nbij' (fun s ↦ s 0) (fun n ↦ fun₀ | 0 => n | 1 => p.natDegree - n)
    (fun s hs ↦ ?_) (fun n hn ↦ ?_) (fun s hs ↦ ?_) (fun n hn ↦ by simp)
    fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
⊢ { k : R // (x + y) ^ (n + 2) = x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y + k * HPow.hPow (β := ℕ) y 2 }
have obtain : (z : R) →
  (hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2) →
    { k : R // (x + y) ^ (n + 2) = x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y + k * HPow.hPow (β := ℕ) y 2 }
Tactic: obtain ⟨z, hz⟩ := (powAddExpansion x y (n + 1))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2
⊢ { k : R // (x + y) ^ (n + 2) = x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y + k * HPow.hPow (β := ℕ) y 2 }
have exists : (x + y) ^ (n + 2) =
  x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y +
    (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
Tactic: exists x * z + (n + 1) * x ^ n + z * y
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2
⊢ (x + y) * (x + y) ^ (n + 1) =
    (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2)
have rw : (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2) =
  (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2)
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2
⊢ (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2) =
    x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 1) * y +
      (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
have push_cast : (x + y) * (x ^ (n + 1) + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n * y + z * HPow.hPow (β := ℕ) y 2) =
  x ^ (n + 2) + HAdd.hAdd (α := R) (↑n : R) 2 * x ^ (n + 1) * y +
    (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2
⊢ (x + y) ^ (n + 2) =
    x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y +
      (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
have by : (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)
Tactic: calc
      (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
      _ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
      _ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 := by
        push_cast
        ring!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2
by : (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)
⊢ (x + y) ^ (n + 2) =
    x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y +
      (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
have by₁ : (x + y) * (x + y) ^ (n + 1) =
  (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2)
Tactic: calc
      (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
      _ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
      _ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 := by
        push_cast
        ring!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R_1
m n_1 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2
by : (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)
by₁ :
  (x + y) * (x + y) ^ (n + 1) =
    (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2)
⊢ (x + y) ^ (n + 2) =
    x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y +
      (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
have by₂ : (x + y) * (x ^ (n + 1) + (↑(n + 1) : R) * x ^ (n + 1 - 1) * y + z * HPow.hPow (β := ℕ) y 2) =
  x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 1) * y +
    (x * z + HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n + z * y) * HPow.hPow (β := ℕ) y 2
Tactic: calc
      (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
      _ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
      _ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 := by
        push_cast
        ring!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a_1 b : R
m n : ℕ
inst : CommRing R
x y : R
e : ℕ
a : R
⊢ { k : R // a * (x + y) ^ e = a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + k * HPow.hPow (β := ℕ) y 2) }
have exists : a * (x + y) ^ e = a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2)
Tactic: exists (powAddExpansion x y e).val
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a_1 b : R
m n : ℕ
inst : CommRing R
x y : R
e : ℕ
a : R
⊢ a * (x + y) ^ e = a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2)
have e_a : (x + y) ^ e = x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f =
    f.sum fun (e : ℕ) (a : R) ↦
      a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(polyBinomAux1 x y e a) : R) * HPow.hPow (β := ℕ) y 2)
have rw : Eq (α := R) (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) ((x + y) ^ e))
  (f.sum fun (e : ℕ) (a : R) ↦
    a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(polyBinomAux1 x y e a) : R) * HPow.hPow (β := ℕ) y 2))
Tactic: rw [eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
⊢ Eq (α := R) (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) ((x + y) ^ e))
    (f.sum fun (e : ℕ) (a : R) ↦
      a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(polyBinomAux1 x y e a) : R) * HPow.hPow (β := ℕ) y 2))
have e_f : ∀ (n : ℕ) (z : R),
  HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) z : R) ((x + y) ^ n) =
    z * (x ^ n + (↑n : R) * x ^ (n - 1) * y + (↑(polyBinomAux1 x y n z) : R) * HPow.hPow (β := ℕ) y 2)
Tactic: congr with (n z)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f =
    HAdd.hAdd (α := R) (f.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)
        (f.sum fun (e : ℕ) (a : R) ↦ a * (↑e : R) * x ^ (e - 1) * y) +
      f.sum fun (e : ℕ) (a : R) ↦ a * (↑(polyBinomAux1 x y e a) : R) * HPow.hPow (β := ℕ) y 2
have rw : (f.sum fun (e : ℕ) (a : R) ↦
    a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(polyBinomAux1 x y e a) : R) * HPow.hPow (β := ℕ) y 2)) =
  HAdd.hAdd (α := R) (f.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)
      (f.sum fun (e : ℕ) (a : R) ↦ a * (↑e : R) * x ^ (e - 1) * y) +
    f.sum fun (e : ℕ) (a : R) ↦ a * (↑(polyBinomAux1 x y e a) : R) * HPow.hPow (β := ℕ) y 2
Tactic: rw [poly_binom_aux2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ { k : R // eval (x + y) f = eval x f + eval x ((derivative : (a : R[X]) → R[X]) f) * y + k * HPow.hPow (β := ℕ) y 2 }
have exists : eval (x + y) f =
  eval x f + eval x ((derivative : (a : R[X]) → R[X]) f) * y +
    (f.sum fun (e : ℕ) (a : R) ↦ a * (↑(polyBinomAux1 x y e a) : R)) * HPow.hPow (β := ℕ) y 2
Tactic: exists f.sum fun e a => a * (polyBinomAux1 x y e a).val
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k_1 : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
x y : R
k : ℕ
⊢ { z : R // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
have obtain : (z : R) → (hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)) → { z : R // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
Tactic: obtain ⟨z, hz⟩ := @powSubPowFactor x y (k + 1)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k_1 : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ { z : R // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
have exists : x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)
Tactic: exists z * x + y ^ (k + 1)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k_1 : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)
have a₁ : x ^ (k + 2) - y ^ (k + 2) + x * (z * (x - y)) - ((z * x + y ^ (k + 1)) * (x - y) + x * (x ^ (k + 1) - y ^ (k + 1))) = 0
Tactic: linear_combination (norm := ring) x * hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ { z : R // eval x f - eval y f = z * (x - y) }
have refine : eval x f - eval y f = (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
Tactic: refine ⟨f.sum fun i r => r * (powSubPowFactor x y i).val, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ eval x f - eval y f = (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
have delta : eval₂ (RingHom.id R) x f - eval₂ (RingHom.id R) y f =
  (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
Tactic: delta eval
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) x f - eval₂ (RingHom.id R) y f =
    (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
have rw : HSub.hSub (α := R) (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (x ^ e))
    (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (y ^ e)) =
  (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
Tactic: rw [eval₂_eq_sum, eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ HSub.hSub (α := R) (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (x ^ e))
      (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (y ^ e)) =
    (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
have simp : Eq.{u + 1} (α := R)
  (∑ x_1 ∈ f.support,
    (HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (x ^ x_1) -
      HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (y ^ x_1)))
  (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))
Tactic: simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ Eq.{u + 1} (α := R)
    (∑ x_1 ∈ f.support,
      (HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (x ^ x_1) -
        HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (y ^ x_1)))
    (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))
have dsimp : Eq.{u + 1} (α := R) (∑ x_1 ∈ f.support, (f.coeff x_1 * x ^ x_1 - f.coeff x_1 * y ^ x_1))
  (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
⊢ Eq.{u + 1} (α := R) (∑ x_1 ∈ f.support, (f.coeff x_1 * x ^ x_1 - f.coeff x_1 * y ^ x_1))
    (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))
have e_f : ∀ (i : ℕ), f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
i : ℕ
⊢ f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y)
have e_f : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * ((↑(powSubPowFactor x y i) : R) * (x - y))
Tactic: rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
i : ℕ
e_f : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * ((↑(powSubPowFactor x y i) : R) * (x - y))
⊢ f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y)
have e_f₁ : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (x ^ i - y ^ i)
Tactic: rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Identities (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
i : ℕ
e_f : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * ((↑(powSubPowFactor x y i) : R) * (x - y))
e_f₁ : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (x ^ i - y ^ i)
⊢ f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y)
have e_f₂ : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * x ^ i - f.coeff i * y ^ i
Tactic: rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (n + 1)
have rw : p.divX.coeff n = p.coeff (1 + n)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (1 + n)
have ofFinsupp : ∀ (toFinsupp : AddMonoidAlgebra R ℕ),
  { toFinsupp := toFinsupp : R[X] }.divX.coeff n = { toFinsupp := toFinsupp : R[X] }.coeff (1 + n)
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p.divX = 0
have rw : Eq.{u + 1} (α := R[X]) (divX ((C : (a : R) → R[X]) (p.coeff 0))) 0
Tactic: rw [h, divX_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = (C : (a : R) → R[X]) (p.coeff 0)
rw : Eq.{u + 1} (α := R[X]) (divX ((C : (a : R) → R[X]) (p.coeff 0))) 0
⊢ p.divX = 0
have rw₁ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [h, divX_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) (divX 1) 0
have a : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff (divX 1) n) (coeff 0 n)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).divX =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.divX
have a₁ : ∀ (n : ℕ),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).divX.coeff n =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.divX).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
⊢ (HPow.hPow (α := R[X]) X n).divX = if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1)
have zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).divX =
  if Eq (α := ℕ) 0 0 then 0 else HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 0 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
zero :
  (HPow.hPow (α := R[X]) (β := ℕ) X 0).divX =
    if Eq (α := ℕ) 0 0 then 0 else HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 0 1)
⊢ (HPow.hPow (α := R[X]) X n).divX = if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1)
have succ : ∀ (n : ℕ), (HPow.hPow (α := R[X]) X (n + 1)).divX = if n + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n + 1 - 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X (n + 1)).divX = if n + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n + 1 - 1)
have succ : ∀ (n_1 : ℕ),
  (HPow.hPow (α := R[X]) X (n + 1)).divX.coeff n_1 =
    (if n + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n + 1 - 1)).coeff n_1
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.divX.natDegree = p.natDegree - 1
have φ_k : ∀ (f : R[X]), f.natDegree < 1 → Eq (α := R[X]) ((divX_hom : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
Tactic: apply map_natDegree_eq_sub (φ := divX_hom)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
φ_k : ∀ (f : R[X]), f.natDegree < 1 → Eq (α := R[X]) ((divX_hom : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ p.divX.natDegree = p.natDegree - 1
have φ_mon : ∀ (n : ℕ) (c : R),
  c ≠ 0 → natDegree.{u} (R := R) ((divX_hom : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) c)) = n - 1
Tactic: apply map_natDegree_eq_sub (φ := divX_hom)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ natDegree.{u} (R := R) ((divX_hom : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) c)) = n - 1
have φ_mon : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
      (if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1))).natDegree =
  n - 1
Tactic: rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]