awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hC :
  ∀ (i : S₁),
    Eq (α := (MvPolynomial S₁ R)[X])
      ((AlgHom.comp
              (AlgHom.comp
                (aeval fun (o : Option S₁) ↦
                  o.elim Polynomial.X fun (s : S₁) ↦
                    (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
                (Polynomial.aevalTower (rename Option.some) (X none)))
              CAlgHom :
            (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (X i) :
        (MvPolynomial S₁ R)[X])
      ((AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R)[X]) CAlgHom : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (X i) :
        (MvPolynomial S₁ R)[X])
hX :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff
        ((AlgHom.comp
              (aeval fun (o : Option S₁) ↦
                o.elim Polynomial.X fun (s : S₁) ↦
                  (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
              (Polynomial.aevalTower (rename Option.some) (X none)) :
            (a : (MvPolynomial S₁ R)[X]) → (MvPolynomial S₁ R)[X])
          Polynomial.X)
        n)
      (Polynomial.coeff
        ((AlgHom.id R (MvPolynomial S₁ R)[X] : (a : (MvPolynomial S₁ R)[X]) → (MvPolynomial S₁ R)[X]) Polynomial.X) n)
⊢ Eq (α := (MvPolynomial S₁ R)[X] →ₐ[R] (MvPolynomial S₁ R)[X])
    (AlgHom.comp
      (aeval fun (o : Option S₁) ↦
        o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
      (Polynomial.aevalTower (rename Option.some) (X none)))
    (AlgHom.id R (MvPolynomial S₁ R)[X])

Tactic:
ext : 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
i : S₁
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((AlgHom.comp
            (AlgHom.comp
              (aeval fun (o : Option S₁) ↦
                o.elim Polynomial.X fun (s : S₁) ↦
                  (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
              (Polynomial.aevalTower (rename Option.some) (X none)))
            CAlgHom :
          (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        (X i) :
      (MvPolynomial S₁ R)[X])
    ((AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R)[X]) CAlgHom : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        (X i) :
      (MvPolynomial S₁ R)[X])

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
n : ℕ
⊢ Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff
      ((AlgHom.comp
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            (Polynomial.aevalTower (rename Option.some) (X none)) :
          (a : (MvPolynomial S₁ R)[X]) → (MvPolynomial S₁ R)[X])
        Polynomial.X)
      n)
    (Polynomial.coeff
      ((AlgHom.id R (MvPolynomial S₁ R)[X] : (a : (MvPolynomial S₁ R)[X]) → (MvPolynomial S₁ R)[X]) Polynomial.X) n)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hf :
  ∀ (i : Option S₁) (m : Option S₁ →₀ ℕ),
    Eq.{u + 1} (α := R)
      (coeff m
        ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
              (aeval fun (o : Option S₁) ↦
                o.elim Polynomial.X fun (s : S₁) ↦
                  (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
            (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
          (X i)))
      (coeff m
        ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) :
            (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
          (X i)))
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R →ₐ[R] MvPolynomial.{v, u} (Option S₁) R)
    (AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
      (aeval fun (o : Option S₁) ↦
        o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)))
    (AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R))

Tactic:
ext i : 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
i : Option S₁
m : Option S₁ →₀ ℕ
hf :
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
hf₁ :
  ∀ (val : S₁),
    Eq.{u + 1} (α := R)
      (coeff m
        ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
              (aeval fun (o : Option S₁) ↦
                o.elim Polynomial.X fun (s : S₁) ↦
                  (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
            (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
          (X (Option.some val))))
      (coeff m
        ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) :
            (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
          (X (Option.some val))))
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))

Tactic:
cases i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
m : Option S₁ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
m : Option S₁ →₀ ℕ
val : S₁
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X (Option.some val))))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X (Option.some val))))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
x : S₁
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) (X (Option.some x)) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X x) : (MvPolynomial S₁ R)[X])

Tactic:
simp [optionEquivLeft_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.optionEquivLeft_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) (X none) :
      (MvPolynomial S₁ R)[X])
    (Polynomial.X : (MvPolynomial S₁ R)[X])

Tactic:
simp [optionEquivLeft_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.optionEquivLeft_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
r : R
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
        ((C : (a : R) → MvPolynomial (Option S₁) R) r) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])

Tactic:
simp only [optionEquivLeft_apply, aeval_C, Polynomial.algebraMap_apply, algebraMap_eq]

Premises used: MvPolynomial.optionEquivLeft_apply, Polynomial.algebraMap_apply, MvPolynomial.algebraMap_eq, MvPolynomial.aeval_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
rw :
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    (Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
      ((monomial m.some : (a : R) → MvPolynomial S₁ R) r)
h_zero :
  ∀ (o : Option S₁),
    HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) 0 =
      1
h_add :
  ∀ (o : Option S₁) (m₁ m₂ : ℕ),
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        (m₁ + m₂) =
      HPow.hPow (α := (MvPolynomial S₁ R)[X])
          (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          m₁ *
        HPow.hPow (α := (MvPolynomial S₁ R)[X])
          (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          m₂
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
        ((monomial m : (a : R) → MvPolynomial (Option S₁) R) r) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        ((monomial m.some : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])

Tactic:
rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]

Premises used: MvPolynomial.optionEquivLeft_apply, Finsupp.prod_option_index, MvPolynomial.aeval_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
rw :
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (HMul.hMul (α := MvPolynomial S₁ R) (β := MvPolynomial S₁ R)
            ((C : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)
            (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e : MvPolynomial S₁ R)) :
        (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))
⊢ HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    (Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
      ((monomial m.some : (a : R) → MvPolynomial S₁ R) r)

Tactic:
rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, MvPolynomial.monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
simp :
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
        (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X a) : (MvPolynomial S₁ R)[X]) k) =
    HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
        (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e) *
        HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))
⊢ HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (HMul.hMul (α := MvPolynomial S₁ R) (β := MvPolynomial S₁ R)
            ((C : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)
            (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e : MvPolynomial S₁ R)) :
        (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))

Tactic:
simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
      map_mul, mul_assoc]

Premises used: Polynomial.algebraMap_apply, mul_assoc, Option.elim_none, Option.elim_some, map_mul, MvPolynomial.algebraMap_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
        (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X a) : (MvPolynomial S₁ R)[X]) k) =
    HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
        (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e) *
        HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))

Tactic:
simp only [mul_comm, map_finsuppProd, map_pow]

Premises used: map_finsuppProd, map_pow, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁),
    HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) 0 =
      1

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o : Option S₁
m₁ m₂ : ℕ
h_add h_add₁ :
  HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        m₁ *
      HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        m₂ =
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        m₁ *
      HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₂
⊢ HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
      (m₁ + m₂) =
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        m₁ *
      HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₂

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
x : S₁
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R)
    ((AlgEquiv.symm (optionEquivLeft R S₁) : (a : (MvPolynomial S₁ R)[X]) → MvPolynomial (Option S₁) R)
        ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X x)) :
      MvPolynomial.{v, u} (Option S₁) R)
    (X (Option.some x) : MvPolynomial.{v, u} (Option S₁) R)

Tactic:
simp [optionEquivLeft]

Premises used: MvPolynomial.optionEquivLeft
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
x : R
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R)
    ((AlgEquiv.symm (optionEquivLeft R S₁) : (a : (MvPolynomial S₁ R)[X]) → MvPolynomial (Option S₁) R)
        ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) x)) :
      MvPolynomial.{v, u} (Option S₁) R)
    ((C : (a : R) → MvPolynomial (Option S₁) R) x : MvPolynomial.{v, u} (Option S₁) R)

Tactic:
simp [optionEquivLeft]

Premises used: MvPolynomial.optionEquivLeft
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R)
    ((AlgEquiv.symm (optionEquivLeft R S₁) : (a : (MvPolynomial S₁ R)[X]) → MvPolynomial (Option S₁) R) Polynomial.X :
      MvPolynomial.{v, u} (Option S₁) R)
    (X none : MvPolynomial.{v, u} (Option S₁) R)

Tactic:
simp [optionEquivLeft]

Premises used: MvPolynomial.optionEquivLeft
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
monomial :
  Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          ((MvPolynomial.monomial j.some : (a : R) → MvPolynomial S₁ R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
⊢ Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
          ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))

Tactic:
rw [optionEquivLeft_monomial]

Premises used: MvPolynomial.optionEquivLeft_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
monomial :
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      0
⊢ Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          ((MvPolynomial.monomial j.some : (a : R) → MvPolynomial S₁ R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))

Tactic:
simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]

Premises used: apply_ite, Polynomial.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
monomial :
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      0
⊢ if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      0

Tactic:
simp only [coeff_zero]

Premises used: MvPolynomial.coeff_zero