awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid 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 (↑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 (↑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
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 (↑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 (↑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
⊢ ∃ (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 (↑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

Tactic:
rcases ihf with ⟨P, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
g : R[M]
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 (↑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
P : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hadd :
  ∀ (Q : 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 (↑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]) (β := R[M])
          (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' 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 (↑s : M) :
                  MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
                (a : MvPolynomial (↑S : Type u_2) R) → R[M])
              Q :
            R[M])
⊢ ∃ (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 (↑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 (↑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 ihg with ⟨Q, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
P Q : 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 (↑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]) (β := R[M])
        (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' 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 (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            Q :
          R[M])

Tactic:
⟨P + Q, map_add _ _ _⟩

Premises used: map_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
P Q : 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 (↑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]) (β := R[M])
        (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' 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 (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            Q :
          R[M])

Tactic:
exact ⟨P + Q, map_add _ _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
r : R
f : R[M]
ih :
  ∃ (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 (↑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
hsmul :
  ∀ (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 (↑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 =
        HSMul.hSMul (β := R[M]) r
          (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' 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])
⊢ ∃ (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 (↑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 =
      r • f

Tactic:
rcases ih with ⟨P, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
r : R
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 (↑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 =
      HSMul.hSMul (β := R[M]) r
        (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' 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])

Tactic:
⟨r • P, map_smul _ _ _⟩

Premises used: Exists.intro, HSMul.hSMul, map_smul
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
r : R
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 (↑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 =
      HSMul.hSMul (β := R[M]) r
        (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' 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])

Tactic:
exact ⟨r • P, map_smul _ _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
⊢ Membership.mem (γ := AddSubmonoid M) (closure S) m

Tactic:
have : m ∈ closure S := hS.symm ▸ mem_top _
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])

Tactic:
AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this

Premises used: AddSubmonoid.closure_induction
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m_1 : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m_1
m : M
hm : m ∈ S
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])

Tactic:
⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩

Premises used: FreeAlgebra.ι, FreeAlgebra.lift_ι_apply, Subtype.mk, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m_1 : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m_1
m : M
hm : m ∈ S
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])

Tactic:
exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) 0) : R[M])

Tactic:
⟨1, map_one _⟩

Premises used: map_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) 0) : R[M])

Tactic:
exact ⟨1, map_one _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := AddSubmonoid M) (closure S) m₁
hy : Membership.mem (γ := AddSubmonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₁) : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₂) : R[M])
rw :
  Eq (α := R[M])
    (single
      (HAdd.hAdd (α := M) (β := M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M)
            ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₁ : Multiplicative M) :
          M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M)
            ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₂ : Multiplicative M) :
          M))
      1)
    (single
      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
        ((Multiplicative.ofAdd : (a : M) → Multiplicative M) (m₁ + m₂) : Multiplicative M))
      1)
⊢ Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) (m₁ + m₂)) : R[M])

Tactic:
rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]

Premises used: AddMonoidAlgebra.of_apply, map_mul, AddMonoidAlgebra.single_mul_single, one_mul
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := AddSubmonoid M) (closure S) m₁
hy : Membership.mem (γ := AddSubmonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₁) : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₂) : R[M])
⊢ Eq (α := R[M])
    (single
      (HAdd.hAdd (α := M) (β := M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M)
            ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₁ : Multiplicative M) :
          M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M)
            ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₂ : Multiplicative M) :
          M))
      1)
    (single
      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
        ((Multiplicative.ofAdd : (a : M) → Multiplicative M) (m₁ + m₂) : Multiplicative M))
      1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := AddSubmonoid M) (closure S) m₁
hy : Membership.mem (γ := AddSubmonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₁) : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₂) : R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) (m₁ + m₂)) : R[M])

Tactic:
exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
f g : R[M]
ihf :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
ihg :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      g
hadd :
  ∀ (P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        HAdd.hAdd (α := R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              P :
            R[M])
          g
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f + g

Tactic:
rcases ihf with ⟨P, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
g : R[M]
ihg :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      g
P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hadd :
  ∀ (Q : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        HAdd.hAdd (α := R[M]) (β := R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              P :
            R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              Q :
            R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
P Q : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M]) (β := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            Q :
          R[M])

Tactic:
⟨P + Q, map_add _ _ _⟩

Premises used: map_add, HAdd.hAdd, Exists.intro