awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
refine :
  ∀ (k : ℕ) (hk : k ∈ range n.succ),
    (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
        ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
          MvPolynomial (Fin 2) K) =
      p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
⊢ Eq.{u_1 + 1} (α := K)
    (∑ i ∈ range n.succ,
      (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
        ((MvPolynomial.monomial fun₀ | 0 => i | 1 => n - i : (a : K) → MvPolynomial (Fin 2) K) (p.coeff i) :
          MvPolynomial (Fin 2) K))
    (∑ i ∈ range n.succ, p.coeff i * (x 0 / x 1) ^ i * x 1 ^ n)

Tactic:
refine Finset.sum_congr rfl fun k hk ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
h : k ≤ n
rw₁ : HPow.hPow (β := ℕ) (x 1) 0 = 1
rw₂ : HPow.hPow (β := ℕ) (x 0) 0 = 1
h_zero : ∀ (a : Fin 2), HPow.hPow (β := ℕ) (x a) 0 = 1
h_add : ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂
h₁ : Eq (α := ℕ) ((fun₀ | 0 => k : (a : Fin 2) → ℕ) 1 : ℕ) (0 : ℕ)
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

Tactic:
rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]

Premises used: Finsupp.update_eq_add_single, Finsupp.prod_add_index', MvPolynomial.eval_monomial, pow_sub₀, Finsupp.prod_single_index
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 1 ≠ 0

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ k ≤ n

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ HPow.hPow (β := ℕ) (x 1) 0 = 1

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ HPow.hPow (β := ℕ) (x 0) 0 = 1

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), HPow.hPow (β := ℕ) (x a) 0 = 1

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ Eq (α := ℕ) ((fun₀ | 0 => k : (a : Fin 2) → ℕ) 1 : ℕ) (0 : ℕ)

Tactic:
simp_all [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
⊢ p.toTupleMvPolynomial 0 = p.homogenize p.natDegree

Tactic:
rfl

Premises used: Multiset.sum, Eq.mpr, Multiset.foldr, Polynomial.homogenize, Fin.cons, Fin.induction.go, Polynomial.toTupleMvPolynomial, Fin.induction, Matrix.vecCons, Finset.sum, rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
⊢ p.toTupleMvPolynomial 1 = HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) p.natDegree

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Polynomial.toTupleMvPolynomial, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
i : Fin 2
0 : (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).IsHomogeneous p.natDegree
1 : (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).IsHomogeneous p.natDegree
⊢ (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree

Tactic:
fin_cases i
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).IsHomogeneous p.natDegree

Tactic:
simp [toTupleMvPolynomial]

Premises used: Polynomial.toTupleMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).IsHomogeneous p.natDegree

Tactic:
simpa [toTupleMvPolynomial] using MvPolynomial.isHomogeneous_X_pow 1 p.natDegree

Premises used: Polynomial.toTupleMvPolynomial, Polynomial.natDegree, OfNat.ofNat, MvPolynomial.isHomogeneous_X_pow
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
⊢ (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.toTupleMvPolynomial 0) =
    HMul.hMul (β := R[X]) p
      ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.toTupleMvPolynomial 1) :
        R[X])

Tactic:
simp [toTupleMvPolynomial]

Premises used: Polynomial.toTupleMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_2
inst : Field R
p : R[X]
x : R
⊢ eval x p =
    HDiv.hDiv (α := R) (β := R)
      ((MvPolynomial.eval ![x, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R) (p.toTupleMvPolynomial 0) : R)
      ((MvPolynomial.eval ![x, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R) (p.toTupleMvPolynomial 1) : R)

Tactic:
simp [toTupleMvPolynomial, eval_homogenize]

Premises used: Polynomial.eval_homogenize, Polynomial.toTupleMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((s : (a : Fin 2) → ℕ) 0 : ℕ) ((s : (a : Fin 2) → ℕ) 1 : ℕ) = p.natDegree

Tactic:
simp [(isHomogeneous_homogenize p).degree_eq_sum_deg_support hs, ← Finsupp.degree_apply,
        Finsupp.degree_eq_sum]

Premises used: Finsupp.degree_eq_sum, Polynomial.isHomogeneous_homogenize, MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support, Finsupp.degree_apply
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
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))
⊢ 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)

Tactic:
rw [MvPolynomial.sum_def, sum_def p]

Premises used: MvPolynomial.sum_def, Polynomial.sum_def
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ))
      ((fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ)) n) =
    n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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
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))
⊢ 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:
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 ↦ ?_

Premises used: HSub.hSub, Finsupp.update, Polynomial.natDegree, OfNat.ofNat, Finset.sum_nbij', Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun (s : Fin 2 →₀ ℕ) ↦ ((s : (a : Fin 2) → ℕ) 0 : ℕ)) s ∈ p.support

Tactic:
simpa [coeff_homogenize, sum_eq_natDegree_of_mem_support_homogenize p hs] using hs

Premises used: Polynomial.sum_eq_natDegree_of_mem_support_homogenize, Polynomial.coeff_homogenize
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun (n : ℕ) ↦ (fun₀ | 0 => n | 1 => p.natDegree - n : Fin 2 →₀ ℕ)) n ∈ (p.homogenize p.natDegree).support

Tactic:
simpa [coeff_homogenize, mem_support_iff.mp hn]
      using Nat.add_sub_of_le <| le_natDegree_of_mem_supp n hn

Premises used: Polynomial.le_natDegree_of_mem_supp, Polynomial.mem_support_iff, Nat.add_sub_of_le, Iff.mp, Polynomial.coeff_homogenize
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
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:
grind only [= Finsupp.update_apply, = Finsupp.single_apply,
      sum_eq_natDegree_of_mem_support_homogenize p hs]

Premises used: Finsupp.update_apply, Polynomial.sum_eq_natDegree_of_mem_support_homogenize, Finsupp.single_apply
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
p : R[X]
f : R → M
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:
simp [coeff_homogenize, sum_eq_natDegree_of_mem_support_homogenize p hs]

Premises used: Polynomial.sum_eq_natDegree_of_mem_support_homogenize, Polynomial.coeff_homogenize
-- Module: Mathlib.Algebra.Polynomial.Identities
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 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
⊢ HPow.hPow (β := ℕ) (x + y) 0 =
    HPow.hPow (β := ℕ) x 0 + (↑0 : R) * x ^ HSub.hSub (α := ℕ) 0 1 * y + 0 * HPow.hPow (β := ℕ) y 2

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Identities
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 : ℕ
R : Type u_1
inst : CommSemiring R
x y : R
⊢ HPow.hPow (β := ℕ) (x + y) 1 =
    HPow.hPow (β := ℕ) x 1 + (↑1 : R) * x ^ HSub.hSub (α := ℕ) 1 1 * y + 0 * HPow.hPow (β := ℕ) y 2

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Identities
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 : ℕ
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 }
⊢ { 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))

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Identities
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
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
⊢ { k : R // (x + y) ^ (n + 2) = x ^ (n + 2) + (↑(n + 2) : R) * x ^ (n + 2 - 1) * y + k * HPow.hPow (β := ℕ) y 2 }

Tactic:
exists x * z + (n + 1) * x ^ n + z * y

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Identities
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 + y) * (x + y) ^ (n + 1)

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Identities
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
rw 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)
⊢ (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:
rw [hz]
-- Module: Mathlib.Algebra.Polynomial.Identities
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
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
⊢ (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:
push_cast
-- Module: Mathlib.Algebra.Polynomial.Identities
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) + 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:
ring!
-- Module: Mathlib.Algebra.Polynomial.Identities
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)
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
⊢ (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:
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!

Premises used: HMul.hMul, HSub.hSub, Nat.cast, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Identities
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
exists :
  a * (x + y) ^ e = a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2)
⊢ { k : R // a * (x + y) ^ e = a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + k * HPow.hPow (β := ℕ) y 2) }

Tactic:
exists (powAddExpansion x y e).val

Premises used: Polynomial.powAddExpansion, Subtype.val
-- Module: Mathlib.Algebra.Polynomial.Identities
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
e_a : (x + y) ^ e = x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2
⊢ a * (x + y) ^ e = a * (x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2)

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Identities
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
⊢ (x + y) ^ e = x ^ e + (↑e : R) * x ^ (e - 1) * y + (↑(powAddExpansion x y e) : R) * HPow.hPow (β := ℕ) y 2

Tactic:
apply (powAddExpansion _ _ _).property

Premises used: Polynomial.powAddExpansion, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
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))
⊢ 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)

Tactic:
rw [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
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)
⊢ 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:
congr with (n z)
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
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:
apply (polyBinomAux1 x y _ _).property

Premises used: _private.0.Polynomial.polyBinomAux1, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
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
⊢ 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

Tactic:
rw [poly_binom_aux2]

Premises used: _private.0.Polynomial.poly_binom_aux2
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
inst : CommRing R
f : R[X]
x y : R
⊢ (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:
simp [left_distrib, sum_add, mul_assoc]

Premises used: mul_assoc, Polynomial.sum_add, left_distrib
-- Module: Mathlib.Algebra.Polynomial.Identities
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
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
⊢ { k : R // eval (x + y) f = eval x f + eval x ((derivative : (a : R[X]) → R[X]) f) * y + k * HPow.hPow (β := ℕ) y 2 }

Tactic:
exists f.sum fun e a => a * (polyBinomAux1 x y e a).val

Premises used: HMul.hMul, Polynomial.sum, _private.0.Polynomial.polyBinomAux1, Subtype.val
-- Module: Mathlib.Algebra.Polynomial.Identities
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
x y : R
⊢ HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0 = 0 * (x - y)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Identities
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
x y : R
⊢ HPow.hPow (β := ℕ) x 1 - HPow.hPow (β := ℕ) y 1 = 1 * (x - y)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Identities
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 : ℕ
obtain : (z : R) → (hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)) → { z : R // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
⊢ { z : R // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }

Tactic:
obtain ⟨z, hz⟩ := @powSubPowFactor x y (k + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Identities
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)
exists : x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)
⊢ { z : R // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }

Tactic:
exists z * x + y ^ (k + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Identities
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) + x * (z * (x - y)) - ((z * x + y ^ (k + 1)) * (x - y) + x * (x ^ (k + 1) - y ^ (k + 1))) =
    0

Tactic:
ring