awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
x : σ
⊢ Eq (α := Multiplicative ℕ →* A)
    (MonoidHom.comp (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
      ((AddMonoidHom.toMultiplicative : (a : ℕ →+ σ →₀ ℕ) → Multiplicative ℕ →* Multiplicative (σ →₀ ℕ))
        (Finsupp.singleAddHom x)))
    (MonoidHom.comp (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
      ((AddMonoidHom.toMultiplicative : (a : ℕ →+ σ →₀ ℕ) → Multiplicative ℕ →* Multiplicative (σ →₀ ℕ))
        (Finsupp.singleAddHom x)))
have refine_2 : Eq (α := A)
  ((MonoidHom.comp (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
          ((AddMonoidHom.toMultiplicative : (a : ℕ →+ σ →₀ ℕ) → Multiplicative ℕ →* Multiplicative (σ →₀ ℕ))
            (Finsupp.singleAddHom x)) :
        (a : Multiplicative ℕ) → A)
      ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) :
    A)
  ((MonoidHom.comp (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
          ((AddMonoidHom.toMultiplicative : (a : ℕ →+ σ →₀ ℕ) → Multiplicative ℕ →* Multiplicative (σ →₀ ℕ))
            (Finsupp.singleAddHom x)) :
        (a : Multiplicative ℕ) → A)
      ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) :
    A)
Tactic: apply MonoidHom.ext_mnat
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
⊢ S = ⊤
have refine : ∀ (p : MvPolynomial σ R) (hp : Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) ⊤ p), p ∈ S
Tactic: refine top_unique fun p hp => ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
⊢ p ∈ S
have C : ∀ (a : R), Membership.mem (α := MvPolynomial σ R) S ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: induction p using MvPolynomial.induction_on with
  | C => exact S.algebraMap_mem _
  | add p q hp hq => exact S.add_mem hp hq
  | mul_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Membership.mem (α := MvPolynomial σ R) S ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ p ∈ S
have add : ∀ (p q : MvPolynomial σ R) (hp : p ∈ S) (hq : q ∈ S), p + q ∈ S
Tactic: induction p using MvPolynomial.induction_on with
  | C => exact S.algebraMap_mem _
  | add p q hp hq => exact S.add_mem hp hq
  | mul_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Membership.mem (α := MvPolynomial σ R) S ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
add : ∀ (p q : MvPolynomial σ R) (hp : p ∈ S) (hq : q ∈ S), p + q ∈ S
⊢ p ∈ S
have mul_X : ∀ (p : MvPolynomial σ R) (i : σ) (hp : p ∈ S), p * X i ∈ S
Tactic: induction p using MvPolynomial.induction_on with
  | C => exact S.algebraMap_mem _
  | add p q hp hq => exact S.add_mem hp hq
  | mul_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
h : Decidable (a = 0)
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    (if a = 0 then ∅ else {s})
have rw : Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
  (if a = 0 then ∅ else {s})
Tactic: rw [← Subsingleton.elim (Classical.decEq R a 0) h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}
have hnc : ¬Eq.{u + 1} (α := R) 1 0
Tactic: rw [X, support_monomial, if_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}
have classical : Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1))
  {Finsupp.single n 1}
Tactic: classical rw [X, support_monomial, if_neg]; exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
classical :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single n 1}
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}
have classical₁ : Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single n 1}) {Finsupp.single n 1}
Tactic: classical rw [X, support_monomial, if_neg]; exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
classical :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single n 1}
classical₁ :
  Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single n 1}) {Finsupp.single n 1}
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}
have classical₂ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single n 1} {Finsupp.single n 1}
Tactic: classical rw [X, support_monomial, if_neg]; exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
classical :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single n 1}
classical₁ :
  Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single n 1}) {Finsupp.single n 1}
classical₂ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single n 1} {Finsupp.single n 1}
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}
have hnc : ¬Eq.{u + 1} (α := R) 1 0
Tactic: classical rw [X, support_monomial, if_neg]; exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}
have rw : Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) 1))
  {Finsupp.single s n}
Tactic: rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
rw :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single s n}
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}
have rw₁ : Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single s n}) {Finsupp.single s n}
Tactic: rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
rw :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single s n}
rw₁ : Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single s n}) {Finsupp.single s n}
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}
have rw₂ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single s n} {Finsupp.single s n}
Tactic: rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}
have rw : Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) 1))
  {Finsupp.single s n}
Tactic: classical
    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
rw :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single s n}
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}
have rw₁ : Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single s n}) {Finsupp.single s n}
Tactic: classical
    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
rw :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) 1))
    {Finsupp.single s n}
rw₁ : Eq (α := Finset (σ →₀ ℕ)) (if Eq.{u + 1} (α := R) 1 0 then ∅ else {Finsupp.single s n}) {Finsupp.single s n}
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}
have rw₂ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single s n} {Finsupp.single s n}
Tactic: classical
    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
p : MvPolynomial σ R
⊢ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
have obtain : ∀ (x : R),
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff.{u, u_1} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) x)) :
      MvPolynomial σ R)
Tactic: obtain ⟨x, rfl⟩ := C_surjective σ p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
⊢ coeff m (HPow.hPow (α := MvPolynomial σ R) (X i) k) = if Finsupp.single i k = m then 1 else 0
have this : Eq.{u + 1} (α := R) (coeff m ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1))
  (if Finsupp.single i k = m then 1 else 0)
Tactic: have := coeff_monomial m (Finsupp.single i k) (1 : R)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this :
  Eq.{u + 1} (α := R) (coeff m ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1))
    (if Finsupp.single i k = m then 1 else 0)
⊢ coeff m (HPow.hPow (α := MvPolynomial σ R) (X i) k) = if Finsupp.single i k = m then 1 else 0
have rwa : ∀
  (this :
    Eq.{u + 1} (α := R)
      (coeff m (Finsupp.prod (Finsupp.single i k) fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e))
      (if Finsupp.single i k = m then 1 else 0)),
  HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
Tactic: rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R) (coeff m (X i)) (if Finsupp.single i 1 = m then 1 else 0)
have rw : coeff m (X i) = coeff m (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)
Tactic: rw [← coeff_X_pow, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
rw : coeff m (X i) = coeff m (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)
⊢ Eq.{u + 1} (α := R) (coeff m (X i)) (if Finsupp.single i 1 = m then 1 else 0)
have rw₁ : Eq.{u + 1} (α := R) (coeff m (X i)) (coeff m (X i))
Tactic: rw [← coeff_X_pow, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single i 1) (X i)) 1
have rw : Eq.{u + 1} (α := R) (if Eq (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1) then 1 else 0) 1
Tactic: rw [coeff_X', if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
rw : Eq.{u + 1} (α := R) (if Eq (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1) then 1 else 0) 1
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single i 1) (X i)) 1
have rw₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [coeff_X', if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single i 1) (X i)) 1
have classical : Eq.{u + 1} (α := R) (if Eq (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1) then 1 else 0) 1
Tactic: classical rw [coeff_X', if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
classical : Eq.{u + 1} (α := R) (if Eq (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1) then 1 else 0) 1
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single i 1) (X i)) 1
have classical₁ : Eq.{u + 1} (α := R) 1 1
Tactic: classical rw [coeff_X', if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p
have rw : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
Tactic: rw [mul_def, sum_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
rw : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p
have rw₁ : Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b)) 0
Tactic: rw [mul_def, sum_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p
have rw : coeff m
    (sum ((C : (a : R) → MvPolynomial σ R) a) fun (m : σ →₀ ℕ) (a : R) ↦
      sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (m + n) : (a : R) → MvPolynomial σ R) (a * b)) =
  a * coeff m p
Tactic: classical
  rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
rw :
  coeff m
      (sum ((C : (a : R) → MvPolynomial σ R) a) fun (m : σ →₀ ℕ) (a : R) ↦
        sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (m + n) : (a : R) → MvPolynomial σ R) (a * b)) =
    a * coeff m p
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p
have rw₁ : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
Tactic: classical
  rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
rw :
  coeff m
      (sum ((C : (a : R) → MvPolynomial σ R) a) fun (m : σ →₀ ℕ) (a : R) ↦
        sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (m + n) : (a : R) → MvPolynomial σ R) (a * b)) =
    a * coeff m p
rw₁ : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p
have rw₂ : Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b)) 0
Tactic: classical
  rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ Eq.{u + 1} (α := R) (coeff d (∏ y ∈ s, HPow.hPow (α := MvPolynomial σ R) (X y) (x y)))
    (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
have simp_rw : Eq.{u + 1} (α := R)
  (coeff d ((monomial (Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i) : (a : R) → MvPolynomial σ R) 1))
  (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
Tactic: simp_rw [prod_X_pow x s, coeff_monomial, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
simp_rw :
  Eq.{u + 1} (α := R)
    (coeff d ((monomial (Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i) : (a : R) → MvPolynomial σ R) 1))
    (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
⊢ Eq.{u + 1} (α := R) (coeff d (∏ y ∈ s, HPow.hPow (α := MvPolynomial σ R) (X y) (x y)))
    (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
have simp_rw₁ : Eq.{u + 1} (α := R) (if (Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i) = d then 1 else 0)
  (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
Tactic: simp_rw [prod_X_pow x s, coeff_monomial, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : m ∈ p.support \ q.support
⊢ m ∈ (p + q).support
have hm₁ : ¬coeff m p = 0 ∧ coeff m q = 0
Tactic: simp only [Classical.not_not, mem_support_iff, Finset.mem_sdiff, Ne] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support
have hs : p.support \ q.support ⊆ (p + q).support
Tactic: apply Finset.union_subset
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
hs : p.support \ q.support ⊆ (p + q).support
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support
have a : q.support \ p.support ⊆ (p + q).support
Tactic: apply Finset.union_subset
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (p + q).support
have a : q.support \ p.support ⊆ (q + p).support
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0
have pos : ∀ (h : s ≤ m),
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s) p * r
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
pos :
  ∀ (h : s ≤ m),
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
      coeff (m - s) p * r
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0
have neg : ∀ (h : ¬s ≤ m),
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
| coeff (m - s) p * r
have rw : coeff (m - s + s) (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
Tactic: rw [← coeff_mul_monomial _ s]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s) p * r
have pos : coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
  coeff (m - s + s)
    (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
Tactic: conv_rhs => rw [← coeff_mul_monomial _ s]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s + s)
      (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
have pos : coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
Tactic: rw [tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) = 0
have neg : ∀
  (h :
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) ≠ 0),
  s ≤ m
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) ≠ 0
⊢ s ≤ m
have h₁ : m ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support
Tactic: rw [← mem_support_iff] at h
Cleared hypotheses: h