awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₁ : HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M]) =
  (of R M : (a : M) → R[M]) (m₁ * m₂)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₂ : HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
  (of R M : (a : M) → R[M]) (m₁ * m₂)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₃ : HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
  (of R M : (a : M) → R[M]) (m₁ * m₂)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₆ : Eq (α := R[M]) (single (m₁ * m₂) (HMul.hMul (α := R) 1 1)) (single (m₁ * m₂) 1)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₁ :
        R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
rw₆ : Eq (α := R[M]) (single (m₁ * m₂) (HMul.hMul (α := R) 1 1)) (single (m₁ * m₂) 1)
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw₇ : Eq (α := R[M]) (single (m₁ * m₂) 1) (single (m₁ * m₂) 1)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
f g : R[M]
ihf :
  ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        a =
      f
ihg :
  ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        a =
      g
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        a =
      f + g
have hadd : ∀ (P : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
  ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        a =
      HAdd.hAdd (α := R[M])
        (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            P :
          R[M])
        g
Tactic: rcases ihf with ⟨P, rfl⟩
Cleared hypotheses: f, ihf