awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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)
⊢ 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))
have obtain : ∀ (x : R[M]) (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x),
  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)
              x 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) x
          hx) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
Tactic: classical
  obtain ⟨x, hx⟩ := x
  revert hx
  refine Finsupp.induction x ?_ ?_
  · intro hx
    symm
    exact map_zero _
  · intro m b y hmy hb ih hmby
    have : Disjoint (Finsupp.single m b).support y.support := by
      simpa only [Finsupp.support_single _ hb, Finset.disjoint_singleton_left]
    rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff]
      at hmby
    obtain ⟨h1, h2⟩ := hmby
    have : f m = i := by
      rwa [Finsupp.support_single _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
        at h1
    subst this
    simp only [map_add, decomposeAux_single f m]
    let ih' := ih h2
    dsimp at ih'
    rw [ih', ← map_add]
    apply DirectSum.of_eq_of_gradedMonoid_eq
    congr 2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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 →+ ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext : 4
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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])
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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
⊢ 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])
have 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) sorry)) :
    R[M])
  (single x 1 : R[M])
Tactic: rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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])
⊢ 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])
have 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) sorry) :
    R[M])
  (single x 1)
Tactic: rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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)
⊢ 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])
have h₂ : Eq (α := R[M]) (Finsupp.single x 1) (single x 1)
Tactic: rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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)
⊢ 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))
have 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))
Tactic: rw [decomposeAux_coe f x]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (hypothesis)
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
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'
have 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
Tactic: simp only [smul_eq_mul, mul_def] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
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
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'
have 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'
Tactic: obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
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
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'
have 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'
Tactic: obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
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)))
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'
have 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'
Tactic: obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
Cleared hypotheses: m, hm_1, hm_2, hm
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
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'
have refine : ∀ (sm : G) (p : sm ∈ s ∧ ∃ (d : G), ym = d * sm), (∃ (d : G), ym = d * sm) → ∃ (d : G), xm * ym = d * sm
Tactic: refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
have change : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
Tactic: change _ ↔ x ∈ RHS
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
have mp : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
mp : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
have mpr : x ∈ RHS → Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x → x ∈ RHS
have mp : Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s) ≤ RHS
Tactic: suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s) ≤ RHS
have mp : (⇑(of k G) : (a : G) → k[G]) '' s ⊆ (↑RHS : Set k[G])
Tactic: rw [Ideal.span_le]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : Membership.mem (γ := Finset G) (Finsupp.support.{u_3, u_1} (M := k) ((of k G : (a : G) → k[G]) i)) m
⊢ ∃ m' ∈ s, ∃ (d : G), m = d * m'
have mp : m = 1 * i
Tactic: refine ⟨_, hi, 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x
have mpr : Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) (Finsupp.sum x Finsupp.single)
Tactic: rw [← Finsupp.sum_single x]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) (Finsupp.sum x Finsupp.single)
have apply : ∀ (i : G) (hi : i ∈ x.support),
  Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
    (Finsupp.single i ((x : (a : G) → k) i) : G →₀ k)
Tactic: apply Ideal.sum_mem _ fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
hx : x ∈ RHS
i : G
hi : i ∈ x.support
⊢ Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
    (Finsupp.single i ((x : (a : G) → k) i) : G →₀ k)
have obtain : ∀ (d : G) (hd : d ∈ s) (d2 : G) (hi : d2 * d ∈ x.support),
  Membership.mem (α := k[G]) (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s))
    (Finsupp.single (d2 * d) ((x : (a : G) → k) (d2 * d)) : G →₀ k)
Tactic: obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Ideal (goal)
Goal:
k : Type u_1
G : Type u_3
inst : Monoid G
inst_1 : Semiring k
s : Set G
x : k[G]
let let₁ let₂ :
  Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
⊢ Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔
    ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
have let₃ : let RHS : Ideal k[G] :=
  { carrier := {p : k[G] | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'}, add_mem' := sorry, zero_mem' := sorry,
    smul_mem' := sorry };
Membership.mem (γ := Ideal k[G]) (Ideal.span ((⇑(of k G) : (a : G) → k[G]) '' s)) x ↔ x ∈ RHS
Tactic: classical
  let RHS : Ideal (MonoidAlgebra k G) :=
    { carrier := { p | ∀ m : G, m ∈ p.support → ∃ m' ∈ s, ∃ d, m = d * m' }
      add_mem' {x y} hx hy m hm := (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
      zero_mem' := by simp
      smul_mem' x y hy m hm := by
        simp only [smul_eq_mul, mul_def] at hm
        obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
        refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
        rintro ⟨d, rfl⟩
        exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }
  change _ ↔ x ∈ RHS
  constructor
  · suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
    rw [Ideal.span_le]
    rintro _ ⟨i, hi, rfl⟩ m hm
    refine ⟨_, hi, 1, ?_⟩
    simpa using Finsupp.support_single_subset hm
  · intro hx
    rw [← Finsupp.sum_single x]
    apply Ideal.sum_mem _ fun i hi ↦ ?_
    obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
    simpa using Ideal.mul_mem_left _ (.single d2 <| x (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)