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₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (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)

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
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial σ R) (eval₂ MvPolynomial.C X ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a))
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    eval₂ MvPolynomial.C X p = p → eval₂ MvPolynomial.C X q = q → eval₂ MvPolynomial.C X (p + q) = p + q
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), eval₂ MvPolynomial.C X p = p → eval₂ MvPolynomial.C X (p * X n) = p * X n
⊢ eval₂ MvPolynomial.C X p = p

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Eq (α := MvPolynomial σ R) (eval₂ C X ((C : (a : R) → MvPolynomial σ R) a)) ((C : (a : R) → MvPolynomial σ R) a)

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

Premises used: MvPolynomial.eval₂_add, MvPolynomial.eval₂_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R), eval₂ C X p = p → eval₂ C X q = q → eval₂ C X (p + q) = p + q

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

Premises used: MvPolynomial.eval₂_add, MvPolynomial.eval₂_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), eval₂ C X p = p → eval₂ C X (p * X n) = p * X n

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

Premises used: MvPolynomial.eval₂_add, 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 : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
apply :
  ∀ x ∈ (AddMonoidAlgebra.coeff p).support,
    Eq.{v + 1} (α := S₁)
      ((fun (s : σ →₀ ℕ) (a : R) ↦
          HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (s.prod fun (n : σ) (e : ℕ) ↦ g₁ n ^ e : S₁))
        x ((AddMonoidAlgebra.coeff p : (a : σ →₀ ℕ) → R) x))
      ((fun (s : σ →₀ ℕ) (a : R) ↦
          HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (s.prod fun (n : σ) (e : ℕ) ↦ g₂ n ^ e : S₁))
        x ((AddMonoidAlgebra.coeff p : (a : σ →₀ ℕ) → R) x))
⊢ eval₂ f g₁ p = eval₂ f g₂ p

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
e_a : Eq.{v + 1} (α := S₁) (C.prod fun (n : σ) (e : ℕ) ↦ g₁ n ^ e) (C.prod fun (n : σ) (e : ℕ) ↦ g₂ n ^ e)
⊢ HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) ((AddMonoidAlgebra.coeff p : (a : σ →₀ ℕ) → R) C : R) : S₁)
      (C.prod fun (n : σ) (e : ℕ) ↦ g₁ n ^ e : S₁) =
    HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) ((AddMonoidAlgebra.coeff p : (a : σ →₀ ℕ) → R) C : R) : S₁)
      (C.prod fun (n : σ) (e : ℕ) ↦ g₂ n ^ e : S₁)

Tactic:
congr 1
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
e_a :
  ∀ x ∈ C.support,
    Eq.{v + 1} (α := S₁) ((fun (n : σ) (e : ℕ) ↦ g₁ n ^ e) x ((C : (a : σ) → ℕ) x))
      ((fun (n : σ) (e : ℕ) ↦ g₂ n ^ e) x ((C : (a : σ) → ℕ) x))
⊢ Eq.{v + 1} (α := S₁) (C.prod fun (n : σ) (e : ℕ) ↦ g₁ n ^ e) (C.prod fun (n : σ) (e : ℕ) ↦ g₂ n ^ e)

Tactic:
apply Finset.prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
i : σ
hi : i ∈ C.support
e_a : g₁ i = g₂ i
⊢ HPow.hPow (β := ℕ) (g₁ i) ((C : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((C : (a : σ) → ℕ) i : ℕ)

Tactic:
congr 1
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
i : σ
hi : i ∈ C.support
e_a : coeff C p ≠ 0
⊢ g₁ i = g₂ i

Tactic:
apply h hi
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
i : σ
hi : i ∈ C.support
e_a e_a₁ e_a₂ e_a₃ :
  ∀ (hc : Ne.{u + 1} (α := R) ((AddMonoidAlgebra.coeff p : (a : σ →₀ ℕ) → R) C : R) (0 : R)) (i : σ)
    (hi : i ∈ C.support), coeff C p ≠ 0
⊢ coeff C p ≠ 0

Tactic:
rwa [Finsupp.mem_support_iff] at hc

Premises used: Finsupp.mem_support_iff
-- 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₁
f : R →+* S₁
g : σ → S₁
s : Finset S₂
p : S₂ → MvPolynomial σ R
⊢ eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, eval₂ f g (p x)

Tactic:
map_sum (eval₂Hom f g) _ s

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, map_sum, 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₁
f : R →+* S₁
g : σ → S₁
s : Finset S₂
p : S₂ → MvPolynomial σ R
⊢ eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, eval₂ f g (p x)

Tactic:
map_prod (eval₂Hom f g) _ s

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, map_prod, 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
change : eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p = (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) (eval₂ C q p)
⊢ eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)

Tactic:
change _ = eval₂Hom f g (eval₂ C q p)

Premises used: MvPolynomial.eval₂, MvPolynomial.eval₂Hom, MvPolynomial.C, DFunLike.coe
-- 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
rw :
  eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p =
    eval₂ ((eval₂Hom f g).comp C) ((⇑(eval₂Hom f g) : (a : MvPolynomial σ R) → S₁) ∘ q) p
⊢ eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p = (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) (eval₂ C q p)

Tactic:
rw [eval₂_comp_left (eval₂Hom f g)]

Premises used: MvPolynomial.eval₂Hom, MvPolynomial.eval₂_comp_left
-- 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
e_f : ∀ (a : R), Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) a : S₁) (((eval₂Hom f g).comp C : (a : R) → S₁) a : S₁)
⊢ eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p =
    eval₂ ((eval₂Hom f g).comp C) ((⇑(eval₂Hom f g) : (a : MvPolynomial σ R) → S₁) ∘ q) p

Tactic:
congr with a
-- 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) a : S₁) (((eval₂Hom f g).comp C : (a : R) → S₁) a : S₁)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
X : σ → R
f : MvPolynomial σ R
⊢ Eq.{u + 1} (α := R) ((eval X : (a : MvPolynomial σ R) → R) f : R)
    (∑ d ∈ f.support, coeff d f * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (X i) ((d : (a : σ) → ℕ) i : ℕ) : R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.coeff, Finset.sum, Finsupp.prod, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
X : σ → R
f : MvPolynomial σ R
⊢ Eq.{u + 1} (α := R) ((eval X : (a : MvPolynomial σ R) → R) f : R)
    (∑ d ∈ f.support, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (X i) ((d : (a : σ) → ℕ) i : ℕ) : R)

Tactic:
eval₂_eq' (RingHom.id R) X f

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_eq', MvPolynomial.coeff, RingHom.id, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
f : σ → R
⊢ (eval f : (a : MvPolynomial σ R) → R) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) =
    a * s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e

Tactic:
eval₂_monomial _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_monomial, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : σ → R
⊢ ∀ (a : R), (eval f : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) = a

Tactic:
eval₂_C _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_C, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : σ → R
⊢ ∀ (n : σ), (eval f : (a : MvPolynomial σ R) → R) (X n) = f n

Tactic:
eval₂_X _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : σ → R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R) ((eval f : (a : MvPolynomial σ R) → R) (OfNat.ofNat n) : R) (OfNat.ofNat n : R)

Tactic:
map_ofNat _ n

Premises used: map_ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
rw :
  (eval x : (a : MvPolynomial σ R) → R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p) =
    HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((eval x : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) : R)
      ((eval x : (a : MvPolynomial σ R) → R) p : R) =
    HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)
rw₂ rw₃ :
  HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R) =
    HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)
⊢ (eval x : (a : MvPolynomial σ R) → R) (s • p) = HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)

Tactic:
rw [smul_eq_C_mul, (eval x).map_mul, eval_C]

Premises used: MvPolynomial.eval, MvPolynomial.eval_C, MvPolynomial.smul_eq_C_mul, RingHom.map_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
f : σ → R
⊢ (eval f : (a : MvPolynomial σ R) → R) (p + q) =
    HAdd.hAdd (α := R) (β := R) ((eval f : (a : MvPolynomial σ R) → R) p : R)
      ((eval f : (a : MvPolynomial σ R) → R) q : R)

Tactic:
eval₂_add _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_add, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
f : σ → R
⊢ (eval f : (a : MvPolynomial σ R) → R) (p * q) =
    HMul.hMul (α := R) (β := R) ((eval f : (a : MvPolynomial σ R) → R) p : R)
      ((eval f : (a : MvPolynomial σ R) → R) q : R)

Tactic:
eval₂_mul _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_mul, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → R
⊢ ∀ (n : ℕ),
    (eval f : (a : MvPolynomial σ R) → R) (p ^ n) = HPow.hPow (α := R) ((eval f : (a : MvPolynomial σ R) → R) p : R) n

Tactic:
fun _ => eval₂_pow _ _

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.eval₂_pow, Finsupp.sum, MvPolynomial.eval₂, RingHom.id, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → MvPolynomial σ R
g : σ → R
⊢ Eq.{u + 1} (α := R) ((eval g : (a : MvPolynomial σ R) → R) (∑ i ∈ s, f i) : R)
    (∑ i ∈ s, (eval g : (a : MvPolynomial σ R) → R) (f i) : R)

Tactic:
map_sum (eval g) _ _

Premises used: map_sum, MvPolynomial.eval
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → MvPolynomial σ R
g : σ → R
⊢ Eq.{u + 1} (α := R) ((eval g : (a : MvPolynomial σ R) → R) (∏ i ∈ s, f i) : R)
    (∏ i ∈ s, (eval g : (a : MvPolynomial σ R) → R) (f i) : R)

Tactic:
map_prod (eval g) _ _

Premises used: map_prod, MvPolynomial.eval
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
rw :
  (eval ((⇑(eval g) : (a : MvPolynomial τ R) → R) ∘ f) : (a : MvPolynomial σ R) → R) p =
    eval₂ (RingHom.comp (eval g) C) ((⇑(eval g) : (a : MvPolynomial τ R) → R) ∘ f) p
⊢ Eq.{u + 1} (α := R) ((eval ((⇑(eval g) : (a : MvPolynomial τ R) → R) ∘ f) : (a : MvPolynomial σ R) → R) p : R)
    ((eval g : (a : MvPolynomial τ R) → R) (eval₂ C f p) : R)

Tactic:
rw [eval₂_comp_left (eval g)]

Premises used: MvPolynomial.eval, MvPolynomial.eval₂_comp_left
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
unfold :
  (eval₂Hom (RingHom.id R) ((⇑(eval₂Hom (RingHom.id R) g) : (a : MvPolynomial τ R) → R) ∘ f) :
        (a : MvPolynomial σ R) → R)
      p =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id R) g) C) ((⇑(eval₂Hom (RingHom.id R) g) : (a : MvPolynomial τ R) → R) ∘ f)
      p
⊢ (eval ((⇑(eval g) : (a : MvPolynomial τ R) → R) ∘ f) : (a : MvPolynomial σ R) → R) p =
    eval₂ (RingHom.comp (eval g) C) ((⇑(eval g) : (a : MvPolynomial τ R) → R) ∘ f) p

Tactic:
unfold eval

Premises used: MvPolynomial.eval
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
simp :
  eval₂ (RingHom.id R) (eval₂ (RingHom.id R) g ∘ f) p =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id R) g) C) (eval₂ (RingHom.id R) g ∘ f) p
⊢ (eval₂Hom (RingHom.id R) ((⇑(eval₂Hom (RingHom.id R) g) : (a : MvPolynomial τ R) → R) ∘ f) :
        (a : MvPolynomial σ R) → R)
      p =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id R) g) C) ((⇑(eval₂Hom (RingHom.id R) g) : (a : MvPolynomial τ R) → R) ∘ f)
      p

Tactic:
simp only [coe_eval₂Hom]

Premises used: MvPolynomial.coe_eval₂Hom
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
e_f :
  ∀ (a : R),
    Eq (α := R) ((RingHom.id R : (a : R) → R) a : R) ((RingHom.comp (eval₂Hom (RingHom.id R) g) C : (a : R) → R) a : R)
⊢ eval₂ (RingHom.id R) (eval₂ (RingHom.id R) g ∘ f) p =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id R) g) C) (eval₂ (RingHom.id R) g ∘ f) p

Tactic:
congr with a
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
a : R
⊢ Eq (α := R) ((RingHom.id R : (a : R) → R) a : R) ((RingHom.comp (eval₂Hom (RingHom.id R) g) C : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
g : σ → R
p : MvPolynomial σ R
⊢ eval₂ (RingHom.id R) g p = (eval g : (a : MvPolynomial σ R) → R) p

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst_1 : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s))
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g p) =
        eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) p →
      (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g q) =
          eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) q →
        (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g (p + q)) =
          eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) (p + q)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g p) =
        eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) p →
      (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g (p * X n)) =
        eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) (p * X n)
⊢ (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g p) =
    eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) p

Tactic:
apply induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst_1 : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s))
        ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst_1 : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p_1 p q : MvPolynomial σ R
hp :
  (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g p) =
    eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) p
hq :
  (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g q) =
    eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) q
⊢ (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g (p + q)) =
    eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) (p + q)

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst_1 : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p_1 p : MvPolynomial σ R
n : σ
hp :
  (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g p) =
    eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) p
⊢ (eval x : (a : MvPolynomial τ S) → S) (eval₂ f g (p * X n)) =
    eval₂ (RingHom.comp (eval x) f) (fun (s : σ) ↦ (eval x : (a : MvPolynomial τ S) → S) (g s)) (p * X n)

Tactic:
simp [hp]
-- 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₁
s : σ →₀ ℕ
a : R
⊢ Eq (α := MvPolynomial σ S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ S₁)
    ((monomial s : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) a) : MvPolynomial σ S₁)

Tactic:
AddMonoidAlgebra.map_single ..

Premises used: AddMonoidAlgebra.map_single, Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, Finsupp.mapRange, 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₁
⊢ ∀ (a : R),
    Eq (α := MvPolynomial σ S₁)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a) : MvPolynomial σ S₁)
      ((C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) a) : MvPolynomial σ S₁)

Tactic:
map_monomial _ _

Premises used: MvPolynomial.map_monomial, 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₁
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
_root_.map_ofNat _ _

Premises used: map_ofNat
-- 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₁
n : σ
⊢ Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X n) : MvPolynomial σ S₁)
    (X n : MvPolynomial σ S₁)

Tactic:
simp [X]

Premises used: MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ ∀ (p : MvPolynomial σ R), (map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
AddMonoidAlgebra.map_id

Premises used: AddMonoidAlgebra.map_id, Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, Finsupp.mapRange
-- 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₁
f : R →+* S₁
inst_2 : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ S₂)
    ((map g : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
      MvPolynomial σ S₂)
    ((map (g.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂)

Tactic:
AddMonoidAlgebra.map_map ..

Premises used: AddMonoidAlgebra.map_map, Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, Finsupp.mapRange
-- 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
simp :
  Eq.{v + 1} (α := S₁)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁))
    (sum (AddMonoidAlgebra.coeff ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) fun (s : σ →₀ ℕ) (a : S₁) ↦
      a * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e)
⊢ eval₂ f g p =
    (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)

Tactic:
simp [eval₂, eval]

Premises used: MvPolynomial.eval₂, MvPolynomial.eval