awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih :
  ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) y),
    Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (↑(Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) y hx) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
              ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
            y hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
hmby_1 : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) (Finsupp.single m b + y)
hmby :
  (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i} ∧
    (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
this : Disjoint (Finsupp.support (Finsupp.single m b)) y.support
⊢ (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}

Tactic:
obtain ⟨h1, h2⟩ := hmby
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih :
  ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) y),
    Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (↑(Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) y hx) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
              ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
            y hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
hmby_1 : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) (Finsupp.single m b + y)
hmby :
  (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i} ∧
    (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
this : Disjoint (Finsupp.support (Finsupp.single m b)) y.support
h1 : (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
⊢ (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}

Tactic:
obtain ⟨h1, h2⟩ := hmby
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih :
  ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) y),
    Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (↑(Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) y hx) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
              ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
            y hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
hmby : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) (Finsupp.single m b + y)
this : Disjoint (Finsupp.support (Finsupp.single m b)) y.support
h1 : (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
h2 : (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
rwa :
  ∀ (h1 : (↑{m} : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i})
    (h2 : (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}), (f : (a : M) → ι) m = i
rwa₁ :
  ∀ (h1 : Subset (α := Set M) {m} (Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}))
    (h2 : (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}), (f : (a : M) → ι) m = i
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (h1 : Membership.mem (γ := Set M) (Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}) m)
    (h2 : (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}), (f : (a : M) → ι) m = i
⊢ (f : (a : M) → ι) m = i

Tactic:
rwa [Finsupp.support_single _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
        at h1

Premises used: Set.singleton_subset_iff, Finsupp.support_single, Finset.coe_singleton
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih :
  ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) y),
    Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (↑(Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) y hx) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
              ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
            y hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
hmby : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) (Finsupp.single m b + y)
this : Disjoint (Finsupp.support (Finsupp.single m b)) y.support
h1 : (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
h2 : (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
⊢ (f : (a : M) → ι) m = i

Tactic:
have : f m = i := by
      rwa [Finsupp.support_single _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
        at h1
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext : 4
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
x : M
h :
  Eq (α := R[M])
    (((coeAlgHom (ι := ι) (S := R) (R := R[M]) (gradeBy R (⇑f : (a : M) → ι)) :
            (⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) →ₐ[R] R[M]) :
          (a : ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) → R[M])
        ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) (single x 1)) :
      R[M])
    (single x 1 : R[M])
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
x : M
h :
  Eq (α := R[M])
    (((coeAlgHom (ι := ι) (S := R) (R := R[M]) (gradeBy R (⇑f : (a : M) → ι)) :
            (⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) →ₐ[R] R[M]) :
          (a : ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) → R[M])
        (((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) x : ι) :
              ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) x : ι)) →+
                ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) ((f : (a : M) → ι) x))) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x_1 : R[M]) ↦
            Membership.mem (γ := Submodule R R[M])
              (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) x : ι)) x_1)
            (Finsupp.single x 1) ⋯)) :
      R[M])
    (single x 1 : R[M])
h₁ :
  Eq (α := R[M])
    (↑(Subtype.mk (p := fun (x_1 : R[M]) ↦
          Membership.mem (γ := Submodule R R[M])
            (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) x : ι)) x_1)
          (Finsupp.single x 1) ⋯) :
      R[M])
    (single x 1)
h₂ h₃ : Eq (α := R[M]) (Finsupp.single x 1) (single x 1)
⊢ Eq (α := R[M])
    (((coeAlgHom (ι := ι) (S := R) (R := R[M]) (gradeBy R (⇑f : (a : M) → ι)) :
            (⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) →ₐ[R] R[M]) :
          (a : ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) → R[M])
        ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) (single x 1)) :
      R[M])
    (single x 1 : R[M])

Tactic:
rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk]

Premises used: Subtype.coe_mk, DirectSum.coeAlgHom_of, AddMonoidAlgebra.decomposeAux_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
i : ι
x : ↥(gradeBy R (⇑f : (a : M) → ι) i)
rw rw₁ :
  Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
            ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
          (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        x :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
            ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
          (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        x :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
⊢ Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) (↑x : R[M]) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
            ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
          (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        x :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))

Tactic:
rw [decomposeAux_coe f x]

Premises used: AddMonoidAlgebra.decomposeAux_coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
⊢ Eq (α := (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (⇑(decomposeAux f) : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (⇑(decompose (gradeBy R (⇑f : (a : M) → ι))) : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, AddMonoidAlgebra, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    ((decompose (gradeBy R (⇑f : (a : M) → ι)) : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        (Finsupp.single m r) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) m : ι) :
            ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) →+
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
          (a : ↥(gradeBy R (⇑f : (a : M) → ι) ((f : (a : M) → ι) m))) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        (Subtype.mk (p := fun (x : R[M]) ↦
          Membership.mem (γ := Submodule R R[M])
            (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) x)
          (Finsupp.single m r) ⋯) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))

Tactic:
decomposeAux_single _ _ _

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, Finsupp.sum, AddMonoidAlgebra.decomposeAux_single, Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
ι : Type u_2
R : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
i : ι
r : R
⊢ Eq (α := ⨁ (i : ι), ↥(grade R i))
    ((decompose (grade R) : (a : R[ι]) → ⨁ (i : ι), ↥(grade R i)) (Finsupp.single i r) : ⨁ (i : ι), ↥(grade R i))
    (((DirectSum.of (fun (i : ι) ↦ ↥(grade R i)) i : ↥(grade R i) →+ ⨁ (i : ι), ↥(grade R i)) :
          (a : ↥(grade R i)) → ⨁ (i : ι), ↥(grade R i))
        (Subtype.mk (p := fun (x : R[ι]) ↦ Membership.mem (γ := Submodule R R[ι]) (grade R i) x) (Finsupp.single i r)
          ⋯) :
      ⨁ (i : ι), ↥(grade R i))

Tactic:
decomposeAux_single _ _ _

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, setOf, Finsupp.sum, AddMonoidAlgebra.decomposeAux_single, Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
⊢ IsInternal (ι := ι) (S := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι))

Tactic:
DirectSum.Decomposition.isInternal _

Premises used: DirectSum.Decomposition.isInternal
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
ι : Type u_2
R : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
⊢ IsInternal (ι := ι) (S := Submodule R R[ι]) (grade R)

Tactic:
DirectSum.Decomposition.isInternal _

Premises used: DirectSum.Decomposition.isInternal
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
⊢ Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} 0

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
m : G
hm : m ∈ (x • y).support
⊢ Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    m

Tactic:
simp only [smul_eq_mul, mul_def] at hm

Premises used: MonoidAlgebra.mul_def, smul_eq_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
m : G
hm :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    m
obtain :
  ∀ (xm : G)
    (hm :
      Membership.mem (γ := Finset G)
        (Finsupp.support.{u_3, u_1} (M := k)
          (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
        m),
    ∃ m' ∈ s, ∃ (d : G), m = d * m'
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)

Premises used: Finsupp.support_sum, Iff.mp, Finset.mem_biUnion
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
m : G
hm_1 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    m
xm : G
hm :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
    m
obtain :
  ∀ (ym : G) (hym : ym ∈ y.support)
    (hm :
      m ∈
        Finsupp.support
          (single (xm * ym) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) ym : k)))),
    ∃ m' ∈ s, ∃ (d : G), m = d * m'
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)

Premises used: Finsupp.support_sum, Iff.mp, Finset.mem_biUnion
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
m : G
hm_1 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    m
xm : G
hm_2 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
    m
ym : G
hym : ym ∈ y.support
hm :
  m ∈
    Finsupp.support
      (single (xm * ym) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) ym : k)))
obtain :
  ∀
    (hm :
      Membership.mem (γ := Finset G)
        (Finsupp.support.{u_3, u_1} (M := k)
          (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
        (xm * ym))
    (hm :
      Membership.mem (γ := Finset G)
        (Finsupp.support.{u_3, u_1} (M := k)
          (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
        (xm * ym))
    (hm :
      xm * ym ∈
        Finsupp.support
          (single (xm * ym) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) ym : k)))),
    ∃ m' ∈ s, ∃ (d : G), xm * ym = d * m'
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'

Tactic:
obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)

Premises used: Finset.mem_singleton, Iff.mp, Finsupp.support_single_subset, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
xm ym : G
hym : ym ∈ y.support
hm_1 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    (xm * ym)
hm_2 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
    (xm * ym)
hm :
  xm * ym ∈
    Finsupp.support
      (single (xm * ym) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) ym : k)))
⊢ ∃ m' ∈ s, ∃ (d : G), xm * ym = d * m'

Tactic:
(hy _ hym).imp fun sm p => And.imp_right ?_ p

Premises used: Exists.imp, And.imp_right
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
xm ym : G
hym : ym ∈ y.support
hm_1 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    (xm * ym)
hm_2 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
    (xm * ym)
hm :
  xm * ym ∈
    Finsupp.support
      (single (xm * ym) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) ym : k)))
refine : ∀ (sm : G) (p : sm ∈ s ∧ ∃ (d : G), ym = d * sm), (∃ (d : G), ym = d * sm) → ∃ (d : G), xm * ym = d * sm
⊢ ∃ m' ∈ s, ∃ (d : G), xm * ym = d * m'

Tactic:
refine (hy _ hym).imp fun sm p => And.imp_right ?_ p

Premises used: Exists.imp, And.imp_right
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
xm sm d : G
hym : d * sm ∈ y.support
hm_1 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    (xm * (d * sm))
hm_2 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
    (xm * (d * sm))
hm :
  xm * (d * sm) ∈
    Finsupp.support
      (single (xm * (d * sm)) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) (d * sm) : k)))
p : sm ∈ s ∧ ∃ (d_1 : G), d * sm = d_1 * sm
⊢ ∃ (d_1 : G), xm * (d * sm) = d_1 * sm

Tactic:
⟨xm * d, (mul_assoc _ _ _).symm⟩

Premises used: HMul.hMul, mul_assoc, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Ideal
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x_1 x y : k[G]
hy : Membership.mem (γ := Set k[G]) {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'} y
xm sm d : G
hym : d * sm ∈ y.support
hm_1 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum x fun (m₁ : G) (r₁ : k) ↦ Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)))
    (xm * (d * sm))
hm_2 :
  Membership.mem (γ := Finset G)
    (Finsupp.support.{u_3, u_1} (M := k)
      (Finsupp.sum y fun (m₂ : G) (r₂ : k) ↦ single (xm * m₂) (HMul.hMul (α := k) ((x : (a : G) → k) xm : k) r₂)))
    (xm * (d * sm))
hm :
  xm * (d * sm) ∈
    Finsupp.support
      (single (xm * (d * sm)) (HMul.hMul (α := k) (β := k) ((x : (a : G) → k) xm : k) ((y : (a : G) → k) (d * sm) : k)))
p : sm ∈ s ∧ ∃ (d_1 : G), d * sm = d_1 * sm
⊢ ∃ (d_1 : G), xm * (d * sm) = d_1 * sm

Tactic:
exact ⟨xm * d, (mul_assoc _ _ _).symm⟩