awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
        (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) Polynomial.X) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw₂ : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
    (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
      HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
        (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) Polynomial.X) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₂ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw₃ : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
    (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) n : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1))) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
        (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) Polynomial.X) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₂ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₃ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) n : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw₄ : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) n) *
    eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
        (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) Polynomial.X) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₂ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₃ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) n : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₄ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) n) *
      eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw₅ : HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
    (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1))) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
n : ℕ
d : σ →₀ ℕ
r : R
⊢ Eq.{u + 1} (α := R)
    (Polynomial.coeff
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) ((monomial d : (a : R) → MvPolynomial σ R) r)) n)
    (coeff.{u, u_1} (σ := σ) (Finsupp.single default n) ((monomial d : (a : R) → MvPolynomial σ R) r))
have monomial : Eq.{u + 1} (α := R)
  (Polynomial.coeff
    ((Polynomial.monomial (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default) :
        (a : R) → R[X])
      r)
    n)
  (coeff.{u, u_1} (σ := σ) (Finsupp.single default n)
    ((monomial (Finsupp.single default ((d : (a : σ) → ℕ) default)) : (a : R) → MvPolynomial σ R) r))
Tactic: rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : MvPolynomial σ R
n : ℕ
⊢ Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) P) n = coeff (Finsupp.single default n) P
have monomial : ∀ (d : σ →₀ ℕ) (r : R),
  Eq.{u + 1} (α := R)
    (Polynomial.coeff
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) ((monomial d : (a : R) → MvPolynomial σ R) r)) n)
    (coeff.{u, u_1} (σ := σ) (Finsupp.single default n) ((monomial d : (a : R) → MvPolynomial σ R) r))
Tactic: induction P using induction_on' with
  | monomial d r =>
      rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]
      simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]
  | add P Q hP hQ =>
      simpa using congrArg₂ (· + ·) hP hQ
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : MvPolynomial σ R
n : ℕ
monomial :
  ∀ (d : σ →₀ ℕ) (r : R),
    Eq.{u + 1} (α := R)
      (Polynomial.coeff
        ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
          ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r))
        n)
      (coeff.{u, u_1} (σ := σ) (Finsupp.single default n) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r))
⊢ Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) P) n = coeff (Finsupp.single default n) P
have add : ∀ (P Q : MvPolynomial σ R)
  (hP :
    Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) P) n = coeff (Finsupp.single default n) P)
  (hQ :
    Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) Q) n = coeff (Finsupp.single default n) Q),
  Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) (P + Q)) n =
    coeff (Finsupp.single default n) (P + Q)
Tactic: induction P using induction_on' with
  | monomial d r =>
      rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]
      simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]
  | add P Q hP hQ =>
      simpa using congrArg₂ (· + ·) hP hQ
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ coeff d ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) = P.coeff ((d : (a : σ) → ℕ) default)
have rw : coeff.{u, u_1} (σ := σ) (Finsupp.single default ((d : (a : σ) → ℕ) default))
    ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) =
  P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
Tactic: rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : R[X]
d : σ →₀ ℕ
rw :
  coeff.{u, u_1} (σ := σ) (Finsupp.single default ((d : (a : σ) → ℕ) default))
      ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
⊢ coeff d ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) = P.coeff ((d : (a : σ) → ℕ) default)
have rw₁ : Polynomial.coeff
    ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
      ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P))
    ((d : (a : σ) → ℕ) default) =
  P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
Tactic: rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : R[X]
d : σ →₀ ℕ
rw :
  coeff.{u, u_1} (σ := σ) (Finsupp.single default ((d : (a : σ) → ℕ) default))
      ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
rw₁ :
  Polynomial.coeff
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
        ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P))
      ((d : (a : σ) → ℕ) default) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
⊢ coeff d ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) = P.coeff ((d : (a : σ) → ℕ) default)
have rw₂ : P.coeff ((d : (a : σ) → ℕ) default) =
  P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
Tactic: rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : R[X]
d : σ →₀ ℕ
rw :
  coeff.{u, u_1} (σ := σ) (Finsupp.single default ((d : (a : σ) → ℕ) default))
      ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
rw₁ :
  Polynomial.coeff
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
        ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P))
      ((d : (a : σ) → ℕ) default) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
rw₂ :
  P.coeff ((d : (a : σ) → ℕ) default) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
⊢ coeff d ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) = P.coeff ((d : (a : σ) → ℕ) default)
have rw₃ : P.coeff ((d : (a : σ) → ℕ) default) = P.coeff ((d : (a : σ) → ℕ) default)
Tactic: rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f) = eval₂ φ a f
have simp : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f
Tactic: simp only [MvPolynomial.uniqueAlgEquiv_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default)
      (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((monomial d : (a : R) → MvPolynomial σ R) r)) =
    eval₂ φ a ((monomial d : (a : R) → MvPolynomial σ R) r)
have monomial : Polynomial.eval₂ φ (a default) ((Polynomial.monomial ((d : (a : σ) → ℕ) default) : (a : R) → R[X]) r) =
  eval₂ φ a ((monomial d : (a : R) → MvPolynomial σ R) r)
Tactic: rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default) ((Polynomial.monomial ((d : (a : σ) → ℕ) default) : (a : R) → R[X]) r) =
    eval₂ φ a ((monomial d : (a : R) → MvPolynomial σ R) r)
have monomial : HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ)) =
  HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) r : S) (d.prod fun (n : σ) (e : ℕ) ↦ a n ^ e : S)
Tactic: simp only [Polynomial.eval₂_monomial, eval₂_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) r : S) (d.prod fun (n : σ) (e : ℕ) ↦ a n ^ e : S)
have monomial : HMul.hMul (α := S) ((φ : (a : R) → S) r : S)
    (HPow.hPow (β := ℕ) (a default)
      (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default : ℕ)) =
  HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ))
Tactic: rw [Finsupp.unique_single d, Finsupp.prod_single_index]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
monomial :
  HMul.hMul (α := S) ((φ : (a : R) → S) r : S)
      (HPow.hPow (β := ℕ) (a default)
        (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ))
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) r : S) (d.prod fun (n : σ) (e : ℕ) ↦ a n ^ e : S)
have monomial₁ : HPow.hPow (β := ℕ) (a default) 0 = 1
Tactic: rw [Finsupp.unique_single d, Finsupp.prod_single_index]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f
have monomial : ∀ (d : σ →₀ ℕ) (r : R),
  Polynomial.eval₂ φ (a default)
      (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((monomial d : (a : R) → MvPolynomial σ R) r)) =
    eval₂ φ a ((monomial d : (a : R) → MvPolynomial σ R) r)
Tactic: induction f using MvPolynomial.induction_on' with
  | monomial d r =>
    rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
    simp only [Polynomial.eval₂_monomial, eval₂_monomial]
    rw [Finsupp.unique_single d, Finsupp.prod_single_index]
    · simp
    · simp only [pow_zero]
  | add f g hf hg => simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : σ → S
monomial :
  ∀ (d : σ →₀ ℕ) (r : R),
    Polynomial.eval₂ φ (a default)
        (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)) =
      eval₂ φ a ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f
have add : ∀ (f g : MvPolynomial σ R)
  (hf : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f)
  (hg : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) g) = eval₂ φ a g),
  Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (f + g)) = eval₂ φ a (f + g)
Tactic: induction f using MvPolynomial.induction_on' with
  | monomial d r =>
    rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
    simp only [Polynomial.eval₂_monomial, eval₂_monomial]
    rw [Finsupp.unique_single d, Finsupp.prod_single_index]
    · simp
    · simp only [pow_zero]
  | add f g hf hg => simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ eval₂ φ a ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f) = Polynomial.eval₂ φ (a default) f
have rw : Polynomial.eval₂ φ (a default)
    ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
      ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f)) =
  Polynomial.eval₂ φ (a default) f
Tactic: rw [(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
    (φ := φ) (a := a)).symm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default)
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
        ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f)) =
    Polynomial.eval₂ φ (a default) f
have rw : Polynomial.eval₂ φ (a default) f = Polynomial.eval₂ φ (a default) f
Tactic: rw [AlgEquiv.apply_symm_apply]