awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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)
refine_2 :
  ∀ (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)))
⊢ Eq (α := MonoidHom.{u_1, u_2} (Multiplicative (σ →₀ ℕ)) A) (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
    (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))

Tactic:
apply Finsupp.mulHom_ext'

Premises used: Finsupp.mulHom_ext'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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 : σ
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)
⊢ 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)))

Tactic:
apply MonoidHom.ext_mnat

Premises used: MonoidHom.ext_mnat
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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 (α := 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:
hX _

Premises used: MvPolynomial.X, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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 (α := 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:
exact hX _
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC : f.comp C = g.comp C
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ f = g

Tactic:
ringHom_ext (RingHom.ext_iff.1 hC) hX

Premises used: MvPolynomial.ringHom_ext, RingHom.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : Semiring S₂
f g : MvPolynomial σ R →+* S₂
hC : f.comp C = g.comp C
hX :
  ∀ (n : σ),
    Eq.{w + 1} (α := S₂) ((f : (a : MvPolynomial σ R) → S₂) (X n) : S₂) ((g : (a : MvPolynomial σ R) → S₂) (X n) : S₂)
p : MvPolynomial σ R
⊢ Eq.{w + 1} (α := S₂) ((f : (a : MvPolynomial σ R) → S₂) p : S₂) ((g : (a : MvPolynomial σ R) → S₂) p : S₂)

Tactic:
RingHom.congr_fun (ringHom_ext' hC hX) p

Premises used: RingHom.congr_fun, MvPolynomial.ringHom_ext'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R →+* MvPolynomial σ R
hC : f.comp C = C
hX :
  ∀ (n : σ),
    Eq (α := MvPolynomial σ R) ((f : (a : MvPolynomial σ R) → MvPolynomial σ R) (X n) : MvPolynomial σ R)
      (X n : MvPolynomial σ R)
p : MvPolynomial σ R
⊢ (f : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
hom_eq_hom f (RingHom.id _) hC hX p

Premises used: MvPolynomial.hom_eq_hom, RingHom.id
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f g : MvPolynomial σ A →ₐ[R] B
h₁ :
  Eq (α := A →ₐ[R] B) (f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)))
    (g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)))
h₂ :
  ∀ (i : σ),
    Eq.{u_3 + 1} (α := B) ((f : (a : MvPolynomial σ A) → B) (X i) : B) ((g : (a : MvPolynomial σ A) → B) (X i) : B)
⊢ f = g

Tactic:
AlgHom.coe_ringHom_injective (MvPolynomial.ringHom_ext' (congr_arg AlgHom.toRingHom h₁) h₂)

Premises used: AlgHom.coe_ringHom_injective, congr_arg, AlgHom.toRingHom, MvPolynomial.ringHom_ext'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
f g : MvPolynomial σ R →ₐ[R] A
hf :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ f = g

Tactic:
AddMonoidAlgebra.algHom_ext' (mulHom_ext' fun X : σ => MonoidHom.ext_mnat (hf X))

Premises used: Finsupp.mulHom_ext', MonoidHom.ext_mnat, AddMonoidAlgebra.algHom_ext'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
f : MvPolynomial σ R →ₐ[R] A
r : R
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
f.commutes r

Premises used: AlgHom.commutes
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
set :
  let S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X);
  S = ⊤
⊢ Eq (α := Subalgebra R (MvPolynomial σ R)) (Algebra.adjoin R (range X)) ⊤

Tactic:
set S := Algebra.adjoin R (range (X : σ → MvPolynomial σ R))

Premises used: MvPolynomial.X, Algebra.adjoin, Set.range
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
⊢ S = ⊤

Tactic:
top_unique fun p hp => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
refine : ∀ (p : MvPolynomial σ R) (hp : Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) ⊤ p), p ∈ S
⊢ S = ⊤

Tactic:
refine top_unique fun p hp => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
a : R
⊢ Membership.mem (α := MvPolynomial σ R) S ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
S.algebraMap_mem _

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
a : R
⊢ Membership.mem (α := MvPolynomial σ R) S ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
exact S.algebraMap_mem _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p q : MvPolynomial σ R
hp : p ∈ S
hq : q ∈ S
⊢ p + q ∈ S

Tactic:
S.add_mem hp hq

Premises used: Subalgebra.add_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p q : MvPolynomial σ R
hp : p ∈ S
hq : q ∈ S
⊢ p + q ∈ S

Tactic:
exact S.add_mem hp hq

Premises used: Subalgebra.add_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
i : σ
hp : p ∈ S
⊢ p * X i ∈ S

Tactic:
S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)

Premises used: Subalgebra.mul_mem, Set.mem_range_self, Set.Mem, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
i : σ
hp : p ∈ S
⊢ p * X i ∈ S

Tactic:
exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)

Premises used: Subalgebra.mul_mem, Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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
mul_X : ∀ (p : MvPolynomial σ R) (i : σ) (hp : p ∈ S), p * X i ∈ S
⊢ p ∈ 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 _)

Premises used: MvPolynomial.induction_on, Subalgebra.algebraMap_mem, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : MvPolynomial σ R →ₗ[R] M
h : ∀ (s : σ →₀ ℕ), f ∘ₗ monomial s = g ∘ₗ monomial s
⊢ f = g

Tactic:
Finsupp.lhom_ext' h

Premises used: Finsupp.lhom_ext', AddMonoidAlgebra
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.support = p.support

Tactic:
rfl

Premises used: MvPolynomial.support, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
h : Decidable (a = 0)
rw :
  Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    (if a = 0 then ∅ else {s})
⊢ 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]

Premises used: Subsingleton.elim, OfNat.ofNat, Classical.decEq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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})

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
c : R
h : Decidable (c = 0)
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c)) (if c = 0 then ∅ else {0})

Tactic:
support_monomial

Premises used: MvPolynomial.support_monomial, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Subset (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) {s}

Tactic:
support_single_subset

Premises used: Set.Mem, setOf, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
Finsupp.support_add

Premises used: Set.Mem, setOf, Finsupp.support_add
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
hnc : ¬Eq.{u + 1} (α := R) 1 0
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}

Tactic:
rw [X, support_monomial, if_neg]

Premises used: MvPolynomial.support_monomial, MvPolynomial.X, if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬Eq.{u + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬Eq.{u + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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}
hnc : ¬Eq.{u + 1} (α := R) 1 0
classical₃ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single n 1} {Finsupp.single n 1}
hnc₁ hnc₂ hnc₃ : ¬Eq.{u + 1} (α := R) 1 0
⊢ support.{u, u_1} (R := R) (X n) = {Finsupp.single n 1}

Tactic:
classical rw [X, support_monomial, if_neg]; exact one_ne_zero

Premises used: MvPolynomial.support_monomial, MvPolynomial.X, one_ne_zero, if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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}
rw₂ rw₃ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single s n} {Finsupp.single s n}
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}

Tactic:
rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.support_monomial, one_ne_zero', if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Basic
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}
rw₂ rw₃ : Eq (α := Finset (σ →₀ ℕ)) {Finsupp.single s n} {Finsupp.single s n}
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).support = {Finsupp.single s n}

Tactic:
classical
    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.support_monomial, one_ne_zero', if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 0) ∅

Tactic:
rfl

Premises used: MvPolynomial.support, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) {0}

Tactic:
simp [show support (1 : MvPolynomial σ R) = if (1 : R) = 0 then ∅ else {0} from rfl]

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) {0}

Tactic:
classical
  simp [show support (1 : MvPolynomial σ R) = if (1 : R) = 0 then ∅ else {0} from rfl]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S₁ : Type u_2
inst_1 : SMulZeroClass S₁ R
a : S₁
f : MvPolynomial σ R
⊢ (a • f).support ⊆ f.support

Tactic:
Finsupp.support_smul

Premises used: Set.Mem, setOf, Finsupp.support_smul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
inst_1 : DecidableEq σ
s : Finset α
f : α → MvPolynomial σ R
⊢ Subset.{u_1} (α := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) (∑ x ∈ s, f x)) (s.biUnion fun (x : α) ↦ (f x).support)

Tactic:
Finsupp.support_finsetSum

Premises used: Set.Mem, setOf, Finsupp.support_finsetSum, MvPolynomial.support, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support ↔ coeff m p ≠ 0

Tactic:
simp [support, coeff]

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

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : AddCommMonoid A
p : MvPolynomial σ R
b : (σ →₀ ℕ) → R → A
⊢ sum p b = ∑ m ∈ p.support, b m (coeff m p)

Tactic:
simp [support, Finsupp.sum, coeff]

Premises used: Finsupp.sum, MvPolynomial.support, MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p * q).support ⊆ p.support + q.support

Tactic:
AddMonoidAlgebra.support_mul p q

Premises used: Set.Mem, setOf, MvPolynomial.support, AddMonoidAlgebra.support_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : σ →₀ ℕ
p : MvPolynomial σ R
s : R
ha : a ∉ p.support
hs : s ≠ 0
⊢ Disjoint (support.{u, u_1} (R := R) ((monomial a : (a : R) → MvPolynomial σ R) s)) p.support

Tactic:
simpa [support_monomial, hs] using notMem_support_iff.mp ha

Premises used: MvPolynomial.support_monomial, MvPolynomial.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : σ →₀ ℕ
p : MvPolynomial σ R
s : R
ha : a ∉ p.support
hs : s ≠ 0
⊢ Disjoint (support.{u, u_1} (R := R) ((monomial a : (a : R) → MvPolynomial σ R) s)) p.support

Tactic:
classical
  simpa [support_monomial, hs] using notMem_support_iff.mp ha

Premises used: MvPolynomial.support_monomial, MvPolynomial.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m p = coeff m q) → p = q

Tactic:
Finsupp.ext

Premises used: Finsupp.ext, MvPolynomial.coeff, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
p q : MvPolynomial σ R
⊢ coeff m (p + q) = coeff m p + coeff m q

Tactic:
add_apply p q m

Premises used: Finsupp.add_apply, MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S₁ : Type u_2
inst_1 : SMulZeroClass S₁ R
m : σ →₀ ℕ
C : S₁
p : MvPolynomial σ R
⊢ coeff m (C • p) = C • coeff m p

Tactic:
AddMonoidAlgebra.smul_apply C p m

Premises used: AddMonoidAlgebra.smul_apply, MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R) (coeff m 0) 0

Tactic:
rfl

Premises used: MvPolynomial.coeff, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
h : Eq (α := σ →₀ ℕ) (Finsupp.single i 1) 0
⊢ False

Tactic:
cases Finsupp.single_eq_zero.1 h

Premises used: Finsupp.single_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
g : S₁ →+ R
φ : MvPolynomial σ S₁
m : σ →₀ ℕ
⊢ coeff m (map g φ) = (g : (a : S₁) → R) (coeff m φ)

Tactic:
rfl

Premises used: MvPolynomial.coeff, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
X : Type u_2
s : Finset X
f : X → MvPolynomial σ R
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R) (coeff m (∑ x ∈ s, f x)) (∑ x ∈ s, coeff m (f x))

Tactic:
map_sum (@coeffAddMonoidHom R σ _ _) _ s

Premises used: map_sum, MvPolynomial.coeff, MvPolynomial.coeffAddMonoidHom
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) 1)
    (m.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e)

Tactic:
simp [monomial_eq]

Premises used: MvPolynomial.monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ coeff m ((monomial n : (a : R) → MvPolynomial σ R) a) = if n = m then a else 0

Tactic:
Finsupp.single_apply

Premises used: MvPolynomial.coeff, Finsupp.single_apply
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
a : R
⊢ coeff m ((C : (a : R) → MvPolynomial σ R) a) = if 0 = m then a else 0

Tactic:
Finsupp.single_apply

Premises used: MvPolynomial.coeff, Finsupp.single_apply