awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ ∀ {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
have 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
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ ∀ {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
have 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
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)) =
    eval₂ f g
      (HMul.hMul (β := MvPolynomial σ R) p
        ((monomial (Finsupp.single n 1 + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R))
have 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))
Tactic: rw [monomial_single_add, pow_one, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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))
⊢ 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))
have 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))
Tactic: rw [monomial_single_add, pow_one, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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))
⊢ 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))
have 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))
Tactic: rw [monomial_single_add, pow_one, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₁
⊢ ∀ {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
have C : ∀ (a : R) {s : σ →₀ ℕ} {a_1 : 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_1 : MvPolynomial σ R)) =
    HMul.hMul (β := S₁) (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)) ((f : (a : R) → S₁) a_1 : S₁) *
      s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
Tactic: classical
  apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ ∀ {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
have 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
Tactic: classical
  apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ ∀ {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
have 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
Tactic: classical
  apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q
have C : ∀ (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: apply MvPolynomial.induction_on q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q
have 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)
Tactic: apply MvPolynomial.induction_on q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q
have 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)
Tactic: apply MvPolynomial.induction_on q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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 (HPow.hPow (β := ℕ) p 0) = HPow.hPow (β := ℕ) (eval₂ f g p) 0
have rw : eval₂ f g 1 = 1
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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 : ℕ
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
have rw : eval₂ f g (p ^ n * HPow.hPow (β := ℕ) p 1) = eval₂ f g p ^ (n + 1)
Tactic: rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
have rw₁ : eval₂ f g (p ^ n * p) = eval₂ f g p ^ (n + 1)
Tactic: rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
have rw₂ : eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * HPow.hPow (β := ℕ) (eval₂ f g p) 1
Tactic: rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
have rw₃ : eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * eval₂ f g p
Tactic: rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
have rw₄ : eval₂ f g (p ^ n) * eval₂ f g p = eval₂ f g p ^ n * eval₂ f g p
Tactic: rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
have rw₅ : eval₂ f g p ^ n * eval₂ f g p = eval₂ f g p ^ n * eval₂ f g p
Tactic: rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₂
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i)
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₂)
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i)
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₂)
    ((eval₂Hom (φ.comp f) fun (i : σ) ↦ (φ : (a : S₁) → S₂) (g i) : (a : MvPolynomial σ R) → S₂) p : S₂)
have 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₂)
Tactic: rw [← comp_eval₂Hom]