awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
(coeff_monomial_mul' _ _ _ _).trans ?_

Premises used: MvPolynomial.X, MvPolynomial.coeff_monomial_mul', Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
refine :
  (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
⊢ coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
refine (coeff_monomial_mul' _ _ _ _).trans ?_

Premises used: MvPolynomial.coeff_monomial_mul', Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw₁ :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
simp_rw₂ :
  (if LT.lt (α := ℕ) (0 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
simp_rw₃ :
  (if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]

Premises used: Finsupp.mem_support_iff, Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw : (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
⊢ p = 0 ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
rw [MvPolynomial.ext_iff]

Premises used: MvPolynomial.ext_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
simp only [coeff_zero]

Premises used: MvPolynomial.coeff_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw : (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0
⊢ p ≠ 0 ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0

Tactic:
rw [Ne, eq_zero_iff]

Premises used: Ne, MvPolynomial.eq_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
push : (∃ (d : σ →₀ ℕ), coeff d p ≠ 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (∃ (d : σ →₀ ℕ), coeff d p ≠ 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
rw : ∃ (d : σ →₀ ℕ), Ne.{u + 1} (α := R) (coeff d (X s)) 0
⊢ Ne (α := MvPolynomial σ R) (X s) 0

Tactic:
rw [ne_zero_iff]

Premises used: MvPolynomial.ne_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
h : Ne.{u + 1} (α := R) (coeff (Finsupp.single s 1) (X s)) 0
⊢ ∃ (d : σ →₀ ℕ), Ne.{u + 1} (α := R) (coeff d (X s)) 0

Tactic:
use Finsupp.single s 1

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
⊢ Ne.{u + 1} (α := R) (coeff (Finsupp.single s 1) (X s)) 0

Tactic:
simp only [coeff_X, ne_eq, one_ne_zero, not_false_eq_true]

Premises used: MvPolynomial.coeff_X, ne_eq, one_ne_zero, not_false_eq_true
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.support = ∅ ↔ p = 0

Tactic:
Finsupp.support_eq_empty

Premises used: MvPolynomial.support, Finsupp.support_eq_empty, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw : p.support ≠ ∅ ↔ p ≠ 0
rw₁ : ¬p.support = ∅ ↔ p ≠ 0
rw₂ rw₃ : ¬p = 0 ↔ p ≠ 0
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]

Premises used: MvPolynomial.support_eq_empty, Finset.nonempty_iff_ne_empty, ne_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0

Tactic:
ne_zero_iff.mp h

Premises used: MvPolynomial.ne_zero_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
rw : IsLeftRegular (R := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ IsRegular (R := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
rw [← isLeftRegular_iff_isRegular]

Premises used: isLeftRegular_iff_isRegular
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
a₁ : ∀ (d : σ →₀ ℕ), coeff d p = coeff d q
⊢ p = q

Tactic:
ext d
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
d : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff (m + d)
      ((fun (x : MvPolynomial σ R) ↦
          HMul.hMul (α := MvPolynomial σ R)
            ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x)
        p))
    (coeff (m + d)
      ((fun (x : MvPolynomial σ R) ↦
          HMul.hMul (α := MvPolynomial σ R)
            ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x)
        q))

Tactic:
have h' := congr_arg (coeff (m + d)) h
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
d : σ →₀ ℕ
h' :
  Eq.{u + 1} (α := R)
    (coeff (m + d)
      ((fun (x : MvPolynomial σ R) ↦
          HMul.hMul (α := MvPolynomial σ R)
            ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x)
        p))
    (coeff (m + d)
      ((fun (x : MvPolynomial σ R) ↦
          HMul.hMul (α := MvPolynomial σ R)
            ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x)
        q))
⊢ a * coeff d p = a * coeff d q

Tactic:
simp only [coeff_monomial_mul] at h'

Premises used: MvPolynomial.coeff_monomial_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
d : σ →₀ ℕ
h' a₁ : a * coeff d p = a * coeff d q
a₂ a₃ : a * coeff d q = a * coeff d q
⊢ coeff d p = coeff d q

Tactic:
rw [← ha.left.eq_iff, h']

Premises used: Function.Injective.eq_iff, IsRegular.left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (monomial m : (a : R) → MvPolynomial σ R) 1 * p = (monomial m : (a : R) → MvPolynomial σ R) 1 * q ↔ p = q

Tactic:
isRegular_one.monomial.left.eq_iff

Premises used: Function.Injective.eq_iff, IsRegular.monomial, IsRegular.left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
⊢ X i * p = X i * q ↔ p = q

Tactic:
monomial_one_mul_cancel_left_iff

Premises used: MvPolynomial.X, MvPolynomial.monomial_one_mul_cancel_left_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
m : σ →₀ ℕ
⊢ p * (monomial m : (a : R) → MvPolynomial σ R) 1 = q * (monomial m : (a : R) → MvPolynomial σ R) 1 ↔ p = q

Tactic:
isRegular_one.monomial.right.eq_iff

Premises used: Function.Injective.eq_iff, IsRegular.right, IsRegular.monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
⊢ p * X i = q * X i ↔ p = q

Tactic:
monomial_one_mul_cancel_right_iff

Premises used: MvPolynomial.X, MvPolynomial.monomial_one_mul_cancel_right_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
mp : (C : (a : R) → MvPolynomial σ R) r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
mpr : (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → (C : (a : R) → MvPolynomial σ R) r ∣ φ
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
mp : r ∣ r * coeff c φ
⊢ r ∣ coeff c (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)

Tactic:
rw [coeff_C_mul]

Premises used: MvPolynomial.coeff_C_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ r * coeff c φ

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
h : ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
mpr :
  ∀ (C : (i : σ →₀ ℕ) → R) (hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i),
    (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ

Tactic:
choose C hc using h

Premises used: MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
h : φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ

Tactic:
use ψ
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
h :
  ∀ (m : σ →₀ ℕ),
    coeff m φ =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
⊢ φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ

Tactic:
apply MvPolynomial.ext

Premises used: MvPolynomial.ext
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
h : coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
⊢ coeff i φ =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)

Tactic:
simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']

Premises used: Finset.sum_ite_eq', MvPolynomial.coeff_C_mul, MvPolynomial.coeff_monomial, MvPolynomial.coeff_sum
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
pos : ∀ (hi : i ∈ φ.support), coeff i φ = r * C i
neg : ∀ (hi : i ∉ φ.support), coeff i φ = r * 0
⊢ coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0

Tactic:
split_ifs with hi
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
hi : i ∈ φ.support
pos pos₁ : r * C i = r * C i
⊢ coeff i φ = r * C i

Tactic:
rw [hc]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
hi : i ∉ φ.support
⊢ coeff i φ = 0

Tactic:
rw [notMem_support_iff] at hi

Premises used: MvPolynomial.notMem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
hi neg neg₁ neg₂ neg₃ : coeff i φ = 0
⊢ coeff i φ = r * 0

Tactic:
rwa [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
mpr mpr₁ mpr₂ mpr₃ : (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
h :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
h₁ h₂ :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  ∀ (i : σ →₀ ℕ),
    coeff i φ =
      coeff i (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
h₃ : ∀ (i : σ →₀ ℕ), coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
pos : ∀ (i : σ →₀ ℕ) (hi : i ∈ φ.support), coeff i φ = r * C i
neg neg₁ : ∀ (i : σ →₀ ℕ) (hi : i ∉ φ.support), coeff i φ = r * 0
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ

Tactic:
classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]

Premises used: MvPolynomial.notMem_support_iff, Finset.sum_ite_eq', MvPolynomial.ext, MvPolynomial.coeff_C_mul, MulZeroClass.mul_zero, MvPolynomial.coeff_monomial, MvPolynomial.coeff_sum
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
suffices : IsLeftRegular (R := MvPolynomial σ R) (X n)
⊢ IsRegular (R := MvPolynomial σ R) (X n)

Tactic:
suffices IsLeftRegular (X n : MvPolynomial σ R) from
    ⟨this, this.right_of_commute <| Commute.all _⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
P₁ : ∀ (hPQ : X n * P = X n * Q), P = Q
⊢ Eq (α := MvPolynomial σ R) ((fun (x : MvPolynomial σ R) ↦ X n * x) P) ((fun (x : MvPolynomial σ R) ↦ X n * x) Q) →
    P = Q

Tactic:
(hPQ : (X n) * P = (X n) * Q)
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
a : ∀ (i : σ →₀ ℕ), coeff i P = coeff i Q
⊢ P = Q

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
a : coeff (Finsupp.single n 1 + i) (X n * P) = coeff i Q
a₁ : coeff (Finsupp.single n 1 + i) (X n * Q) = coeff i Q
a₂ a₃ : coeff i Q = coeff i Q
⊢ coeff i P = coeff i Q

Tactic:
rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]

Premises used: MvPolynomial.coeff_X_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
k : ℕ
⊢ IsRegular (HPow.hPow (α := MvPolynomial σ R) (X n) k)

Tactic:
isRegular_X.pow k

Premises used: MvPolynomial.isRegular_X, IsRegular.pow
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : Finset σ
⊢ IsRegular (R := MvPolynomial σ R) (∏ n ∈ s, X n)

Tactic:
IsRegular.prod fun _ _ ↦ isRegular_X

Premises used: MvPolynomial.isRegular_X, IsRegular.prod
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Finset R) (coeffs.{u, u_1} (σ := σ) 0) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, MvPolynomial.coeffs, List.dedup, Multiset.zero, Finset.empty, Multiset.ofList, List.pwFilter, List.foldr, Finset.image, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw :
  ∀ (x : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) x →
      Membership.mem (γ := Finset R) {1} (coeff x 1)
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}

Tactic:
rw [coeffs, Finset.image_subset_iff]

Premises used: MvPolynomial.coeffs, Finset.image_subset_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ ∀ (x : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) x →
      Membership.mem (γ := Finset R) {1} (coeff x 1)

Tactic:
simp_all [coeff_one]

Premises used: MvPolynomial.coeff_one
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : Subset (α := Finset R) (Finset.image (fun (m : σ →₀ ℕ) ↦ coeff m 1) (support.{u, u_1} (R := R) 1)) {1}
rw₁ rw₂ rw₃ :
  ∀ (x : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) x →
      Membership.mem (γ := Finset R) {1} (coeff x 1)
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}

Tactic:
classical
    rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]

Premises used: MvPolynomial.coeffs, MvPolynomial.coeff_one, Finset.image_subset_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Subsingleton R
p : MvPolynomial σ R
⊢ p.coeffs = ∅

Tactic:
simpa [coeffs] using Subsingleton.eq_zero p

Premises used: MvPolynomial.coeffs, Subsingleton.eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
apply : Subset (α := Finset R) {1} (coeffs.{u, u_1} (σ := σ) 1)
⊢ Eq (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}

Tactic:
apply Finset.Subset.antisymm coeffs_one

Premises used: MvPolynomial.coeffs_one, Finset.Subset.antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
simp :
  ∃ (a : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) a ∧ Eq.{u + 1} (α := R) (coeff a 1) 1
⊢ Subset (α := Finset R) {1} (coeffs.{u, u_1} (σ := σ) 1)

Tactic:
simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]

Premises used: Finset.mem_image, MvPolynomial.coeffs, Finset.singleton_subset_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) 0 ∧
    Eq.{u + 1} (α := R) (coeff.{u, u_1} (σ := σ) 0 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ∃ (a : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) a ∧ Eq.{u + 1} (α := R) (coeff a 1) 1

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p

Tactic:
simp [coeffs, eq_comm, (Finset.mem_image)]

Premises used: Finset.mem_image, MvPolynomial.coeffs, eq_comm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
h : coeff m p ≠ 0
⊢ coeff m p ∈ p.coeffs

Tactic:
letI := Classical.decEq R
  Finset.mem_image_of_mem p.coeff (mem_support_iff.mpr h)

Premises used: Iff.mpr, MvPolynomial.mem_support_iff, Set.Mem, setOf, MvPolynomial.coeff, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
obtain : ∀ (n : σ →₀ ℕ) (hnsupp : n ∈ p.support) (hn : 0 = coeff n p), False
⊢ False

Tactic:
obtain ⟨n, hnsupp, hn⟩ := mem_coeffs_iff.mp hz

Premises used: Iff.mp, MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
n : σ →₀ ℕ
hnsupp : n ∈ p.support
hn : 0 = coeff n p
⊢ False

Tactic:
(mem_support_iff.mp hnsupp) hn.symm

Premises used: MvPolynomial.mem_support_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
n : σ →₀ ℕ
hnsupp : n ∈ p.support
hn : 0 = coeff n p
⊢ False

Tactic:
exact (mem_support_iff.mp hnsupp) hn.symm

Premises used: MvPolynomial.mem_support_iff, Iff.mp, Eq.symm