awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
rw : eval₂ f g ((monomial 0 : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
rw₁ :
  HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (Finsupp.prod 0 fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) =
    (f : (a : R) → S₁) a
rw₂ : HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (1 : S₁) = (f : (a : R) → S₁) a
rw₃ rw₄ : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) a : S₁) ((f : (a : R) → S₁) a : S₁)
⊢ eval₂ f g ((C : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a

Tactic:
rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]

Premises used: MvPolynomial.C_apply, MvPolynomial.eval₂_monomial, mul_one, Finsupp.prod_zero_index
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g 1 = 1

Tactic:
(eval₂_C _ _ _).trans f.map_one

Premises used: RingHom.map_one, MvPolynomial.eval₂_C, Eq.trans, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
n : ℕ
⊢ eval₂ f g (↑n : MvPolynomial σ R) = (↑n : S₁)

Tactic:
(eval₂_C _ _ _).trans (map_natCast f n)

Premises used: MvPolynomial.eval₂_C, map_natCast, Eq.trans, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
n : ℕ
inst_2 : n.AtLeastTwo
⊢ eval₂ f g (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
eval₂_natCast f g n

Premises used: MvPolynomial.eval₂_natCast
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
n : σ
⊢ eval₂ f g (X n) = g n

Tactic:
simp [eval₂_monomial, f.map_one, X, prod_single_index, pow_one]

Premises used: MvPolynomial.X, RingHom.map_one, pow_one, MvPolynomial.eval₂_monomial, Finsupp.prod_single_index
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
s : σ
n : ℕ
⊢ eval₂ f g (HPow.hPow (α := MvPolynomial σ R) (X s) n) = g s ^ n

Tactic:
simp [X_pow_eq_monomial, eval₂_monomial f g]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.eval₂_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
C :
  ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          ((monomial s : (a : R) → MvPolynomial σ R) a_1 : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) ((f : (a : R) → S₁) a_1 : S₁) *
        s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g
              (HMul.hMul (β := MvPolynomial σ R) q ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
            HMul.hMul (β := S₁) (eval₂ f g q) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g
              (HMul.hMul (β := MvPolynomial σ R) (p + q)
                ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
            HMul.hMul (β := S₁) (eval₂ f g (p + q)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) (p * X n)
              ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g (p * X n)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
⊢ ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
a' : R
s : σ →₀ ℕ
a : R
⊢ eval₂ f g
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R)
        ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    HMul.hMul (β := S₁) (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a')) ((f : (a : R) → S₁) a : S₁) *
      s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e

Tactic:
simp [C_mul_monomial, eval₂_monomial, f.map_mul]

Premises used: MvPolynomial.C_mul_monomial, MvPolynomial.eval₂_monomial, RingHom.map_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p_1 : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p q : MvPolynomial σ R
ih_p :
  ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
ih_q :
  ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) q ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g q) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
⊢ ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g
        (HMul.hMul (β := MvPolynomial σ R) (p + q) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g (p + q)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e

Tactic:
simp [add_mul, eval₂_add, ih_p, ih_q]

Premises used: add_mul, MvPolynomial.eval₂_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p_1 : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih :
  ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
s : σ →₀ ℕ
a : R
rw :
  eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) (p * X n) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    eval₂ f g
      (p *
        HMul.hMul (β := MvPolynomial σ R) (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X n) 1)
          ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R))
rw₁ :
  eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) (p * X n) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    eval₂ f g
      (p *
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X n)
          ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R))
rw₂ rw₃ :
  eval₂ f g
      (p *
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X n)
          ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    eval₂ f g
      (p *
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X n)
          ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R))
⊢ eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) (p * X n) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) p
        ((monomial (Finsupp.single n 1 + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R))

Tactic:
rw [monomial_single_add, pow_one, mul_assoc]

Premises used: mul_assoc, pow_one, MvPolynomial.monomial_single_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p_1 : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih :
  ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) p
        ((monomial (Finsupp.single n 1 + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    HMul.hMul (β := S₁) (eval₂ f g (p * (monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1))
        ((f : (a : R) → S₁) a : S₁) *
      s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e

Tactic:
simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
            f.map_one]

Premises used: Finsupp.prod_add_index, mul_assoc, pow_add, RingHom.map_one, mul_left_comm, pow_one, Finsupp.prod_single_index
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p_1 : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih :
  ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) (p * X n) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
    HMul.hMul (β := S₁) (eval₂ f g (p * X n)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e

Tactic:
exact
      calc (p * X n * monomial s a).eval₂ f g
        _ = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g := by
          rw [monomial_single_add, pow_one, mul_assoc]
        _ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
          simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
            f.map_one]

Premises used: HPow.hPow, DFunLike.coe, Finsupp.prod
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
a : R
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ (HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * Finsupp.prod 0 fun (n : σ) (e : ℕ) ↦ g n ^ e) =
    HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
C :
  ∀ (a : R) {p : MvPolynomial σ R},
    eval₂ f g
        (HMul.hMul (β := MvPolynomial σ R) p ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      eval₂ f g p * eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) →
        ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q

Tactic:
apply MvPolynomial.induction_on q

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {p : MvPolynomial σ R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      eval₂ f g p * eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
simp [eval₂_C, eval₂_mul_C]

Premises used: MvPolynomial.eval₂_C, MvPolynomial.eval₂_mul_C
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) →
        ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)

Tactic:
simp +contextual [mul_add, eval₂_add]

Premises used: MvPolynomial.eval₂_add, mul_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)

Tactic:
simp +contextual [X, eval₂_mul_monomial, ← mul_assoc]

Premises used: MvPolynomial.eval₂_mul_monomial, mul_assoc, MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
hp : eval₂ f g p = 0
⊢ eval₂ f g (p * q) = 0

Tactic:
simp [eval₂_mul f g, hp]

Premises used: MvPolynomial.eval₂_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
hq : eval₂ f g q = 0
⊢ eval₂ f g (p * q) = 0

Tactic:
simp [eval₂_mul f g, hq]

Premises used: MvPolynomial.eval₂_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
rw : eval₂ f g 1 = 1
⊢ eval₂ f g (HPow.hPow (β := ℕ) p 0) = HPow.hPow (β := ℕ) (eval₂ f g p) 0

Tactic:
rw [pow_zero, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g 1 = 1

Tactic:
eval₂_one _ _

Premises used: MvPolynomial.eval₂_one
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g 1 = 1

Tactic:
exact eval₂_one _ _

Premises used: MvPolynomial.eval₂_one
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
rw : eval₂ f g (p ^ n * HPow.hPow (β := ℕ) p 1) = eval₂ f g p ^ (n + 1)
rw₁ : eval₂ f g (p ^ n * p) = eval₂ f g p ^ (n + 1)
rw₂ : eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * HPow.hPow (β := ℕ) (eval₂ f g p) 1
rw₃ : eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * eval₂ f g p
rw₄ : eval₂ f g (p ^ n) * eval₂ f g p = eval₂ f g p ^ n * eval₂ f g p
rw₅ rw₆ : eval₂ f g p ^ n * eval₂ f g p = eval₂ f g p ^ n * eval₂ f g p
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)

Tactic:
rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]

Premises used: pow_add, MvPolynomial.eval₂_mul, pow_one
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p q : MvPolynomial σ R
h : p ∣ q
⊢ eval₂ f g p ∣ eval₂ f g q

Tactic:
map_dvd (eval₂Hom f g) h

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, map_dvd, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ (⇑(eval₂Hom f g) : (a : MvPolynomial σ R) → S₁) = eval₂ f g

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((eval₂Hom f₁ g₁ : (a : MvPolynomial σ R) → S₁) p₁ : S₁)
    ((eval₂Hom f₁ g₁ : (a : MvPolynomial σ R) → S₁) p₁ : S₁)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
r : R
⊢ Eq.{v + 1} (α := S₁)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : S₁)
    ((f : (a : R) → S₁) r : S₁)

Tactic:
eval₂_C f g r

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_C, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
i : σ
⊢ (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) (X i) = g i

Tactic:
eval₂_X f g i

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
hC :
  ∀ (x : R),
    Eq.{w + 1} (α := S₂) (((φ.comp (eval₂Hom f g)).comp C : (a : R) → S₂) x : S₂)
      ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i)) C :
            (a : R) → S₂)
          x :
        S₂)
hX :
  ∀ (i : σ),
    Eq.{w + 1} (α := S₂) ((φ.comp (eval₂Hom f g) : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
      ((eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i) : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i)

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
x : R
⊢ Eq.{w + 1} (α := S₂) (((φ.comp (eval₂Hom f g)).comp C : (a : R) → S₂) x : S₂)
    ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i)) C :
          (a : R) → S₂)
        x :
      S₂)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
i : σ
⊢ Eq.{w + 1} (α := S₂) ((φ.comp (eval₂Hom f g) : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
    ((eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i) : (a : MvPolynomial σ R) → S₂) (X i) : S₂)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
rw :
  Eq.{w + 1} (α := S₂) ((φ : (a : S₁) → S₂) ((eval₂Hom f g : (a : MvPolynomial σ R) → S₁) p : S₁) : S₂)
    ((φ.comp (eval₂Hom f g) : (a : MvPolynomial σ R) → S₂) p : S₂)
⊢ Eq.{w + 1} (α := S₂) ((φ : (a : S₁) → S₂) ((eval₂Hom f g : (a : MvPolynomial σ R) → S₁) p : S₁) : S₂)
    ((eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i) : (a : MvPolynomial σ R) → S₂) p : S₂)

Tactic:
rw [← comp_eval₂Hom]

Premises used: MvPolynomial.comp_eval₂Hom
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ Eq.{w + 1} (α := S₂) ((φ : (a : S₁) → S₂) ((eval₂Hom f g : (a : MvPolynomial σ R) → S₁) p : S₁) : S₂)
    ((φ.comp (eval₂Hom f g) : (a : MvPolynomial σ R) → S₂) p : S₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
d : σ →₀ ℕ
r : R
⊢ (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) =
    HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) r : S₁) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S₁)

Tactic:
simp only [coe_eval₂Hom, eval₂_monomial]

Premises used: MvPolynomial.coe_eval₂Hom, MvPolynomial.eval₂_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
r : R
P : MvPolynomial σ R
⊢ (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) (r • P) =
    HSMul.hSMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) r : S₁) ((eval₂Hom f g : (a : MvPolynomial σ R) → S₁) P : S₁)

Tactic:
simp [smul_eq_C_mul]

Premises used: MvPolynomial.smul_eq_C_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
C :
  ∀ (a : R),
    (k : (a : S₁) → S₂) (eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p →
      (k : (a : S₁) → S₂) (eval₂ f g q) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) q →
        (k : (a : S₁) → S₂) (eval₂ f g (p + q)) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) (p + q)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p →
      (k : (a : S₁) → S₂) (eval₂ f g (p * X n)) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) (p * X n)
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R),
    (k : (a : S₁) → S₂) (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

Premises used: MvPolynomial.eval₂_add, MvPolynomial.eval₂_mul, RingHom.map_mul, RingHom.map_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p →
      (k : (a : S₁) → S₂) (eval₂ f g q) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) q →
        (k : (a : S₁) → S₂) (eval₂ f g (p + q)) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) (p + q)

Tactic:
simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

Premises used: MvPolynomial.eval₂_add, MvPolynomial.eval₂_mul, RingHom.map_mul, RingHom.map_add