awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
hf : f.FiniteType
hg : Surjective.{u_3 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
⊢ (g.comp f).FiniteType

Tactic:
RingHom.FiniteType.comp_surjective hf hg

Premises used: AlgHom.FiniteType, RingHom.FiniteType.comp_surjective
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ f.FiniteType

Tactic:
RingHom.FiniteType.of_surjective f.toRingHom hf

Premises used: AlgHom.FiniteType, AlgHom.toRingHom, RingHom.FiniteType.of_surjective
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
h : (g.comp f).FiniteType
⊢ g.FiniteType

Tactic:
RingHom.FiniteType.of_comp_finiteType h

Premises used: AlgHom.FiniteType, RingHom.FiniteType.of_comp_finiteType
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
this :
  LE.le (α := Submodule R R[M]) (span R (of' R M '' (↑f.support : Set M)))
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))))
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))) f

Tactic:
this (mem_span_support f)

Premises used: iInf, Set.Mem, Set.iInter, setOf, AddMonoidAlgebra.mem_span_support
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
this :
  LE.le (α := Submodule R R[M]) (span R (of' R M '' (↑f.support : Set M)))
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))))
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))) f

Tactic:
exact this (mem_span_support f)

Premises used: AddMonoidAlgebra.mem_span_support
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
suffices :
  LE.le (α := Submodule R R[M]) (span R (of' R M '' (↑f.support : Set M)))
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))))
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))) f

Tactic:
suffices span R (of' R M '' f.support) ≤
      Subalgebra.toSubmodule (adjoin R (of' R M '' f.support)) by
    exact this (mem_span_support f)
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
rw :
  of' R M '' (↑f.support : Set M) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
            (adjoin R (of' R M '' (↑f.support : Set M))) :
          Submodule R R[M]) :
      Set R[M])
⊢ LE.le (α := Submodule R R[M]) (span R (of' R M '' (↑f.support : Set M)))
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
⊢ of' R M '' (↑f.support : Set M) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
            (adjoin R (of' R M '' (↑f.support : Set M))) :
          Submodule R R[M]) :
      Set R[M])

Tactic:
subset_adjoin

Premises used: iInf, Set.iInter, Algebra.subset_adjoin, setOf
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
⊢ of' R M '' (↑f.support : Set M) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
            (adjoin R (of' R M '' (↑f.support : Set M))) :
          Submodule R R[M]) :
      Set R[M])

Tactic:
exact subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤

Tactic:
le_antisymm le_top ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
refine : LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M)))
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤

Tactic:
refine le_antisymm le_top ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
rw : S ⊆ (↑(adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) : Set R[M])
⊢ LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M)))

Tactic:
rw [← hS, adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
s : R[M]
hs : Membership.mem (γ := Set R[M]) (of' R M '' (↑f.support : Set M)) s
⊢ Membership.mem (γ := Set R[M]) (⋃ g ∈ S, of' R M '' (↑g.support : Set M)) s

Tactic:
Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
s : R[M]
hs : Membership.mem (γ := Set R[M]) (of' R M '' (↑f.support : Set M)) s
⊢ Membership.mem (γ := Set R[M]) (⋃ g ∈ S, of' R M '' (↑g.support : Set M)) s

Tactic:
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
⊢ Subset (α := Set R[M]) (of' R M '' (↑f.support : Set M)) (⋃ g ∈ S, of' R M '' (↑g.support : Set M))

Tactic:
have hincl :
    of' R M '' f.support ⊆ ⋃ (g : R[M]) (_ : g ∈ S), of' R M '' g.support := by
    intro s hs
    exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
hincl : Subset (α := Set R[M]) (of' R M '' (↑f.support : Set M)) (⋃ g ∈ S, of' R M '' (↑g.support : Set M))
⊢ f ∈ (↑(adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) : Set R[M])

Tactic:
adjoin_mono hincl (mem_adjoin_support f)

Premises used: Set.Mem, setOf, AddMonoidAlgebra.mem_adjoin_support, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
hincl : Subset (α := Set R[M]) (of' R M '' (↑f.support : Set M)) (⋃ g ∈ S, of' R M '' (↑g.support : Set M))
⊢ f ∈ (↑(adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) : Set R[M])

Tactic:
exact adjoin_mono hincl (mem_adjoin_support f)

Premises used: AddMonoidAlgebra.mem_adjoin_support, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
this : Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))
rw : Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
this : Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤

Tactic:
support_gen_of_gen hS

Premises used: AddMonoidAlgebra.support_gen_of_gen
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
this : Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤

Tactic:
exact support_gen_of_gen hS

Premises used: AddMonoidAlgebra.support_gen_of_gen
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
suffices : Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤

Tactic:
suffices (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of' R M '' (f.support : Set M) by
    rw [this]
    exact support_gen_of_gen hS
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))

Tactic:
simp only [Set.image_iUnion]

Premises used: Set.image_iUnion
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
h : FiniteType R R[M]
obtain :
  ∀ (S : Finset R[M]) (hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤),
    ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑G : Set M))) ⊤
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑G : Set M))) ⊤

Tactic:
obtain ⟨S, hS⟩ := h
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
h : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑G : Set M))) ⊤

Tactic:
use Finset.biUnion S fun f => f.support

Premises used: Finsupp.support, Finset.biUnion
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
⊢ (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)

Tactic:
simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]

Premises used: Finset.coe_biUnion, Finset.set_biUnion_coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
⊢ (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)

Tactic:
have : (Finset.biUnion S fun f => f.support : Set M) = ⋃ f ∈ S, (f.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this_1 : DecidableEq M := Classical.decEq M
this : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
h : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this_1 : DecidableEq M := Classical.decEq M
this : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤

Tactic:
support_gen_of_gen' hS

Premises used: AddMonoidAlgebra.support_gen_of_gen'
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this_1 : DecidableEq M := Classical.decEq M
this : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤

Tactic:
exact support_gen_of_gen' hS

Premises used: AddMonoidAlgebra.support_gen_of_gen'
-- 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) ⊤
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 : AddCommMonoid 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 : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := 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])
          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 : AddCommMonoid 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 : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := 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])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])

Tactic:
⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩

Premises used: MvPolynomial.aeval_X, MvPolynomial.X, Subtype.mk, 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) ⊤
m_1 : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m_1
m : M
hm : m ∈ S
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := 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])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])

Tactic:
exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
-- 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) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := 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])
          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 : AddCommMonoid 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 : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := 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])
          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 : AddCommMonoid 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₁ : 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 (↑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 : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative 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 (↑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 : 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])
    (((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₁ * 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 : AddCommMonoid 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₁ : 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 (↑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 : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative 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 (↑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 : 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 : AddCommMonoid 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₁ : 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 (↑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 : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative 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 (↑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 : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m₂) : R[M])
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := 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])
          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⟩