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₁
p : MvPolynomial σ R
⊢ 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)

Tactic:
simp [map, MvPolynomial, Finsupp.sum_mapRange_index, mapRingHom]

Premises used: AddMonoidAlgebra.mapRingHom, MvPolynomial, MvPolynomial.map, Finsupp.sum_mapRange_index
-- 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 ((⇑k : (a : S₁) → S₂) ∘ g)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a))
add :
  ∀ (p q : MvPolynomial σ R),
    (k : (a : S₁) → S₂) (eval₂ f g p) =
        eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) →
      (k : (a : S₁) → S₂) (eval₂ f g q) =
          eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) →
        (k : (a : S₁) → S₂) (eval₂ f g (p + q)) =
          eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q))
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (k : (a : S₁) → S₂) (eval₂ f g p) =
        eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) →
      (k : (a : S₁) → S₂) (eval₂ f g (p * X n)) =
        eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n))
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) 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_1 p q : MvPolynomial σ R
hp :
  (k : (a : S₁) → S₂) (eval₂ f g p) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
hq :
  (k : (a : S₁) → S₂) (eval₂ f g q) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)
add :
  (k : (a : S₁) → S₂) (eval₂ f g p + eval₂ f g q) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q))
add₁ :
  HAdd.hAdd (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g q) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q))
add₂ :
  HAdd.hAdd (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g q) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g)
      (HAdd.hAdd (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁))
add₃ :
  HAdd.hAdd (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g q) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) +
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)
add₄ :
  HAdd.hAdd (β := S₂) (eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      ((k : (a : S₁) → S₂) (eval₂ f g q) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) +
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)
add₅ add₆ :
  eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) +
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) +
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)
⊢ (k : (a : S₁) → S₂) (eval₂ f g (p + q)) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q))

Tactic:
rw [eval₂_add, k.map_add, (map f).map_add, eval₂_add, hp, hq]

Premises used: MvPolynomial.eval₂_add, MvPolynomial.map, RingHom.map_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁)
          (eval₂ MvPolynomial.C g ((MvPolynomial.C : (a : R) → MvPolynomial S₂ R) a)) :
        MvPolynomial S₃ S₁)
      (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
          ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial S₂ R) a)) :
        MvPolynomial S₃ S₁)
add :
  ∀ (p q : MvPolynomial S₂ R),
    Eq (α := MvPolynomial S₃ S₁)
        ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ MvPolynomial.C g p) : MvPolynomial S₃ S₁)
        (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
            ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
          MvPolynomial S₃ S₁) →
      Eq (α := MvPolynomial S₃ S₁)
          ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ MvPolynomial.C g q) : MvPolynomial S₃ S₁)
          (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
              ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q) :
            MvPolynomial S₃ S₁) →
        Eq (α := MvPolynomial S₃ S₁)
          ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ MvPolynomial.C g (p + q)) : MvPolynomial S₃ S₁)
          (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
              ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q)) :
            MvPolynomial S₃ S₁)
mul_X :
  ∀ (p : MvPolynomial S₂ R) (n : S₂),
    Eq (α := MvPolynomial S₃ S₁)
        ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ MvPolynomial.C g p) : MvPolynomial S₃ S₁)
        (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
            ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
          MvPolynomial S₃ S₁) →
      Eq (α := MvPolynomial S₃ S₁)
        ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ MvPolynomial.C g (p * X n)) : MvPolynomial S₃ S₁)
        (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
            ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X n)) :
          MvPolynomial S₃ S₁)
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ MvPolynomial.C g p) : MvPolynomial S₃ S₁)
    (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
C :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial S₃ R) r) :
      MvPolynomial S₃ S₁)
    (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial S₂ R) r)) :
      MvPolynomial S₃ S₁)
C₁ :
  Eq (α := MvPolynomial S₃ S₁)
    ((MvPolynomial.C : (a : S₁) → MvPolynomial S₃ S₁) ((f : (a : R) → S₁) r) : MvPolynomial S₃ S₁)
    (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial S₂ R) r)) :
      MvPolynomial S₃ S₁)
C₂ :
  Eq (α := MvPolynomial S₃ S₁)
    ((MvPolynomial.C : (a : S₁) → MvPolynomial S₃ S₁) ((f : (a : R) → S₁) r) : MvPolynomial S₃ S₁)
    (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((MvPolynomial.C : (a : S₁) → MvPolynomial S₂ S₁) ((f : (a : R) → S₁) r)) :
      MvPolynomial S₃ S₁)
C₃ C₄ :
  Eq (α := MvPolynomial S₃ S₁)
    ((MvPolynomial.C : (a : S₁) → MvPolynomial S₃ S₁) ((f : (a : R) → S₁) r) : MvPolynomial S₃ S₁)
    ((MvPolynomial.C : (a : S₁) → MvPolynomial S₃ S₁) ((f : (a : R) → S₁) r) : MvPolynomial S₃ S₁)
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁)
        (eval₂ MvPolynomial.C g ((MvPolynomial.C : (a : R) → MvPolynomial S₂ R) r)) :
      MvPolynomial S₃ S₁)
    (eval₂ MvPolynomial.C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial S₂ R) r)) :
      MvPolynomial S₃ S₁)

Tactic:
rw [eval₂_C, map_C, map_C, eval₂_C]

Premises used: MvPolynomial.eval₂_C, MvPolynomial.map_C
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
C :
  ∀ (a : R),
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a) =
      eval₂ MvPolynomial.C h
        ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a))
add :
  ∀ (p q : MvPolynomial ι R),
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
        eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p) →
      eval₂ (RingHom.comp (map f) MvPolynomial.C) h q =
          eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) q) →
        eval₂ (RingHom.comp (map f) MvPolynomial.C) h (p + q) =
          eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p + q))
mul_X :
  ∀ (p : MvPolynomial ι R) (n : ι),
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
        eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p) →
      eval₂ (RingHom.comp (map f) MvPolynomial.C) h (p * X n) =
        eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p * X n))
⊢ eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
    eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p)

Tactic:
induction p using MvPolynomial.induction_on

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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
a : R
⊢ eval₂ (RingHom.comp (map f) C) h ((C : (a : R) → MvPolynomial ι R) a) =
    eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) ((C : (a : R) → MvPolynomial ι R) a))

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p q : MvPolynomial ι R
h_1 : eval₂ (RingHom.comp (map f) C) h p = eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p)
h_2 : eval₂ (RingHom.comp (map f) C) h q = eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) q)
⊢ eval₂ (RingHom.comp (map f) C) h (p + q) = eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p + q))

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
n : ι
h_1 : eval₂ (RingHom.comp (map f) C) h p = eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p)
⊢ eval₂ (RingHom.comp (map f) C) h (p * X n) =
    eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p * X n))

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
S₂ : Type u_2
inst_1 : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
rw : (q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
rw₁ : (q : (a : S₁) → S₂) (eval₂ (RingHom.id S₁) g p) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
rw₂ :
  eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) ((map (RingHom.id S₁) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) p) =
    eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
rw₃ rw₄ : eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
⊢ Eq.{u_2 + 1} (α := S₂) ((q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) : S₂)
    ((eval ((⇑q : (a : S₁) → S₂) ∘ g) : (a : MvPolynomial σ S₂) → S₂)
        ((map q : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)

Tactic:
rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]

Premises used: MvPolynomial.eval₂_id, MvPolynomial.eval₂_eq_eval_map, MvPolynomial.eval₂_comp_right, MvPolynomial.map_id
-- 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₁
p : MvPolynomial σ R
C :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)

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₁
f : R →+* S₁
r : R
m : σ →₀ ℕ
C :
  Eq.{v + 1} (α := S₁) (coeff m ((MvPolynomial.C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r)) : S₁)
    ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) : S₁)
C₁ :
  Eq.{v + 1} (α := S₁) (if 0 = m then (f : (a : R) → S₁) r else 0 : S₁)
    ((f : (a : R) → S₁) (if 0 = m then r else 0) : S₁)
C₂ :
  Eq.{v + 1} (α := S₁) (if 0 = m then (f : (a : R) → S₁) r else 0 : S₁)
    (if 0 = m then (f : (a : R) → S₁) r else (f : (a : R) → S₁) 0 : S₁)
⊢ Eq.{v + 1} (α := S₁)
    (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) :
      S₁)
    ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) : S₁)

Tactic:
simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]

Premises used: MvPolynomial.coeff_C, apply_ite, MvPolynomial.map_C, RingHom.map_zero, DFunLike.coe
-- 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₁
p q : MvPolynomial σ R
hp :
  ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
hq :
  ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
      ((f : (a : R) → S₁) (coeff m q) : S₁)
m : σ →₀ ℕ
⊢ Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
    ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)

Tactic:
simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]

Premises used: MvPolynomial.coeff_add, MvPolynomial.map, 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₁
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp :
  ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
m : σ →₀ ℕ
⊢ Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X i)) : S₁)
    ((f : (a : R) → S₁) (coeff m (p * X i)) : S₁)

Tactic:
simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]

Premises used: apply_ite, MvPolynomial.coeff_mul_X', RingHom.map_zero, MvPolynomial.map, RingHom.map_mul, DFunLike.coe, MvPolynomial.map_X
-- 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₁
hC :
  ∀ (a : R) (x : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff x ((RingHom.comp (map f) C : (a : R) → MvPolynomial σ S₁) a))
      (coeff x ((RingHom.comp (eval₂Hom (RingHom.comp C f) X) C : (a : R) → MvPolynomial σ S₁) a))
hX :
  ∀ (a : σ) (x : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X a)))
      (coeff x ((eval₂Hom (RingHom.comp C f) X : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X a)))
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ S₁) (map f) (eval₂Hom (RingHom.comp C f) X)

Tactic:
ext a x
-- 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
x : σ →₀ ℕ
⊢ Eq.{v + 1} (α := S₁) (coeff x ((RingHom.comp (map f) C : (a : R) → MvPolynomial σ S₁) a))
    (coeff x ((RingHom.comp (eval₂Hom (RingHom.comp C f) X) C : (a : R) → MvPolynomial σ S₁) a))

Tactic:
simp
-- 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 : σ
x : σ →₀ ℕ
⊢ Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X a)))
    (coeff x ((eval₂Hom (RingHom.comp C f) X : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X a)))

Tactic:
simp
-- 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₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
simp :
  ∀
    (h :
      ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff m p) : S₁) ((f : (a : R) → S₁) (coeff m q) : S₁))
    (m : σ →₀ ℕ), coeff m p = coeff m q
⊢ p = q

Tactic:
simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢

Premises used: MvPolynomial.ext_iff, MvPolynomial.coeff_map
-- 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₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff m p) : S₁) ((f : (a : R) → S₁) (coeff m q) : S₁)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q

Tactic:
hf (h m)
-- 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₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff m p) : S₁) ((f : (a : R) → S₁) (coeff m q) : S₁)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q

Tactic:
exact hf (h m)
-- 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₁
h : Injective (α := MvPolynomial σ R) (β := MvPolynomial σ S₁) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
r r' : R
eq : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) r : S₁) ((f : (a : R) → S₁) r' : S₁)
⊢ Eq (α := MvPolynomial σ S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) r') : MvPolynomial σ S₁)

Tactic:
simpa
-- 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₁
h : Injective (α := MvPolynomial σ R) (β := MvPolynomial σ S₁) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
r r' : R
eq : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) r : S₁) ((f : (a : R) → S₁) r' : S₁)
⊢ r = r'

Tactic:
simpa using h (a₁ := C r) (a₂ := C r') (by simpa)
-- 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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
i : σ →₀ ℕ
fr : S₁
monomial :
  ∀ (r : R),
    ∃ (a : MvPolynomial σ R),
      Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
        ((MvPolynomial.monomial i : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r) : MvPolynomial σ S₁)
⊢ ∃ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
      ((MvPolynomial.monomial i : (a : S₁) → MvPolynomial σ S₁) fr : MvPolynomial σ S₁)

Tactic:
obtain ⟨r, rfl⟩ := hf fr

Premises used: 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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
i : σ →₀ ℕ
r : R
⊢ ∃ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
      ((monomial i : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r) : MvPolynomial σ S₁)

Tactic:
⟨monomial i r, map_monomial _ _ _⟩

Premises used: MvPolynomial.monomial, MvPolynomial.map_monomial, Exists.intro, DFunLike.coe
-- 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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
i : σ →₀ ℕ
r : R
⊢ ∃ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
      ((monomial i : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r) : MvPolynomial σ S₁)

Tactic:
exact ⟨monomial i r, map_monomial _ _ _⟩