awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
have C : ∀ (a : R),
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g ((C : (a : R) → MvPolynomial S₂ R) a)) :
      MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((C : (a : R) → MvPolynomial S₂ R) a)) :
      MvPolynomial S₃ S₁)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₁)
⊢ 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₁)
have 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₁)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₁)
⊢ 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₁)
have 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₁)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g ((C : (a : R) → MvPolynomial S₂ R) r)) :
      MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((C : (a : R) → MvPolynomial S₂ R) r)) :
      MvPolynomial S₃ S₁)
have C : Eq (α := MvPolynomial S₃ S₁)
  ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ((C : (a : R) → MvPolynomial S₃ R) r) : MvPolynomial S₃ S₁)
  (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) ((C : (a : R) → MvPolynomial S₂ R) r)) :
    MvPolynomial S₃ S₁)
Tactic: rw [eval₂_C, map_C, map_C, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₁)
⊢ 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₁)
have 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₁)
Tactic: rw [eval₂_C, map_C, map_C, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₁)
⊢ 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₁)
have 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₁)
Tactic: rw [eval₂_C, map_C, map_C, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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₁)
⊢ 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₁)
have 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₁)
Tactic: rw [eval₂_C, map_C, map_C, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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_1 p q : MvPolynomial S₂ R
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
hq :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ 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₂ C g (p + q)) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
have add : Eq (α := MvPolynomial S₃ S₁)
  ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p + eval₂ C g q) : MvPolynomial S₃ S₁)
  (eval₂ 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₁)
Tactic: rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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_1 p q : MvPolynomial S₂ R
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
hq :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q) :
      MvPolynomial S₃ S₁)
add :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p + eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p + q)) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
have add₁ : HAdd.hAdd (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁) =
  eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
    ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
Tactic: rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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_1 p q : MvPolynomial S₂ R
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
hq :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q) :
      MvPolynomial S₃ S₁)
add :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p + eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
add₁ :
  HAdd.hAdd (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p + q)) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
have add₂ : HAdd.hAdd (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁) =
  eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
    ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
Tactic: rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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_1 p q : MvPolynomial S₂ R
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
hq :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q) :
      MvPolynomial S₃ S₁)
add :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p + eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
add₁ :
  HAdd.hAdd (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
add₂ :
  HAdd.hAdd (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p + q)) : MvPolynomial S₃ S₁)
    (eval₂ 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₁)
have add₃ : HAdd.hAdd (α := MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q)) =
  eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
    ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
Tactic: rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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_1 p : MvPolynomial S₂ R
s : S₂
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ 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₂ C g (p * X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
have mul_X : Eq (α := MvPolynomial S₃ S₁)
  ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p * eval₂ C g (X s)) : MvPolynomial S₃ S₁)
  (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
    MvPolynomial S₃ S₁)
Tactic: rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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_1 p : MvPolynomial S₂ R
s : S₂
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
mul_X :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p * eval₂ C g (X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p * X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
have mul_X₁ : HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
  eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
    ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
Tactic: rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]