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₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p
have C : ∀ (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: 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₁
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)
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p
have 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)
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₁
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)
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) = eval₂ (k.comp f) ((⇑k : (a : S₁) → S₂) ∘ g) p
have 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)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ eval₂ C X p = p
have C : ∀ (a : R),
  Eq (α := MvPolynomial σ R) (eval₂ C X ((C : (a : R) → MvPolynomial σ R) a)) ((C : (a : R) → MvPolynomial σ R) a)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ eval₂ MvPolynomial.C X p = p
have 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
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ eval₂ MvPolynomial.C X p = p
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ), eval₂ MvPolynomial.C X p = p → eval₂ MvPolynomial.C X (p * X n) = p * X n
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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
⊢ eval₂ f g₁ p = eval₂ f g₂ p
have 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))
Tactic: apply Finset.sum_congr rfl
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
⊢ 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₁)
have e_a : Eq.{v + 1} (α := S₁) (C.prod fun (n : σ) (e : ℕ) ↦ g₁ n ^ e) (C.prod fun (n : σ) (e : ℕ) ↦ g₂ n ^ e)
Tactic: congr 1
-- 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₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ (AddMonoidAlgebra.coeff p).support
⊢ Eq.{v + 1} (α := S₁) (C.prod fun (n : σ) (e : ℕ) ↦ g₁ n ^ e) (C.prod fun (n : σ) (e : ℕ) ↦ g₂ n ^ e)
have 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))
Tactic: apply Finset.prod_congr rfl
-- 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₁ 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
⊢ HPow.hPow (β := ℕ) (g₁ i) ((C : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((C : (a : σ) → ℕ) i : ℕ)
have e_a : g₁ i = g₂ i
Tactic: congr 1
-- 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₁ 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
⊢ g₁ i = g₂ i
have e_a : coeff C p ≠ 0
Tactic: apply h hi
-- 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₁ 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
⊢ coeff C p ≠ 0
have 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
Tactic: rwa [Finsupp.mem_support_iff] at hc
Cleared hypotheses: hc, i, hi
-- 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)
have change : eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p = (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) (eval₂ C q p)
Tactic: change _ = eval₂Hom f g (eval₂ C q p)
-- 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun (t : S₂) ↦ eval₂ f g (q t)) p = (eval₂Hom f g : (a : MvPolynomial σ R) → S₁) (eval₂ C q p)
have 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
Tactic: rw [eval₂_comp_left (eval₂Hom f g)]
-- 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ 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
have 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₁)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
⊢ (eval x : (a : MvPolynomial σ R) → R) (s • p) = HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)
have 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)
Tactic: rw [smul_eq_C_mul, (eval x).map_mul, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ (eval x : (a : MvPolynomial σ R) → R) (s • p) = HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)
have 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)
Tactic: rw [smul_eq_C_mul, (eval x).map_mul, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ (eval x : (a : MvPolynomial σ R) → R) (s • p) = HMul.hMul (β := R) s ((eval x : (a : MvPolynomial σ R) → R) p : R)
have 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)
Tactic: rw [smul_eq_C_mul, (eval x).map_mul, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ 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)
have 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
Tactic: rw [eval₂_comp_left (eval g)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (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
have 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
Tactic: unfold eval
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (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
have 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
Tactic: simp only [coe_eval₂Hom]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ 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
have 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)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ (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
have C : ∀ (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: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ (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
have 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)
Tactic: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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)
⊢ (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
have 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)
Tactic: apply 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₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p =
    (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)
have 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)
Tactic: simp [eval₂, eval]
-- 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₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : 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)
have C : ∀ (a : R),
  (k : (a : S₁) → S₂) (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a))
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₁
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))
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
have 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))
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₁
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))
⊢ (k : (a : S₁) → S₂) (eval₂ f g p) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
have 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))
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₁
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)
⊢ (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))
have 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))
Tactic: rw [eval₂_add, k.map_add, (map f).map_add, eval₂_add, hp, hq]
-- 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₁
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))
⊢ (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))
have 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))
Tactic: rw [eval₂_add, k.map_add, (map f).map_add, eval₂_add, hp, hq]