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 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) a
hb : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) j) b
ma : M
hma : ma ∈ a.support
mb : M
hmb : mb ∈ b.support
hc : ma + mb ∈ (a * b).support
rw : HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ma : ι) ((f : (a : M) → ι) mb : ι) = i + j
rw₁ : HAdd.hAdd (β := ι) i ((f : (a : M) → ι) mb : ι) = i + j
rw₂ rw₃ : i + j = i + j
⊢ (f : (a : M) → ι) (ma + mb) = i + j

Tactic:
rw [map_add, ha ma hma, hb mb hmb]

Premises used: map_add
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) a
hb : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) j) b
c : M
hc : c ∈ (a * b).support
obtain :
  ∀ (ma : M) (hma : ma ∈ a.support) (mb : M) (hmb : mb ∈ b.support) (hc : ma + mb ∈ (a * b).support),
    (f : (a : M) → ι) (ma + mb) = i + j
⊢ (f : (a : M) → ι) c = i + j

Tactic:
classical
    obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c :=
      Finset.mem_add.1 <| support_mul a b hc
    rw [map_add, ha ma hma, hb mb hmb]

Premises used: Finsupp.support, map_add, Finset.mem_add, Iff.mp, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : CommSemiring R
⊢ SetLike.GradedMonoid (ι := M) (S := Submodule R R[M]) (grade R)

Tactic:
apply gradeBy.gradedMonoid (AddMonoidHom.id _)

Premises used: AddMonoidHom.id, AddMonoidAlgebra.gradeBy.gradedMonoid
-- 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 : Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι) (0 : ι)
h₁ :
  Eq (α := R[M] → Prop)
    (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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι))
        x)
    fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy.{u_1, u_2, u_3} (ι := ι) R (⇑f : (a : M) → ι) 0) x
h₂ :
  HEq (α :=
    Membership.mem (α := R[M]) (γ := Submodule R R[M])
      (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι))
      (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1) 1 : M →₀ R))
    ⋯ (β := Membership.mem (γ := Submodule R R[M]) (gradeBy.{u_1, u_2, u_3} (ι := ι) R (⇑f : (a : M) → ι) 0) 1) ⋯
⊢ Eq (α := GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (GradedMonoid.mk (A := fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
        ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M))
        (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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι))
            x)
          (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1) 1) ⋯) :
      GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (GradedMonoid.mk (A := fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) 0
        (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) AddZero.toZero _) :
      GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))

Tactic:
congr 2
-- 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.{u_2 + 1} (α := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι) (0 : ι)

Tactic:
simp
-- 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 (α := R[M] → Prop)
    (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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι))
        x)
    fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy.{u_1, u_2, u_3} (ι := ι) R (⇑f : (a : M) → ι) 0) x

Tactic:
simp
-- 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 →+ ι
⊢ HEq (α :=
    Membership.mem (α := R[M]) (γ := Submodule R R[M])
      (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι))
      (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1) 1 : M →₀ R))
    ⋯ (β := Membership.mem (γ := Submodule R R[M]) (gradeBy.{u_1, u_2, u_3} (ι := ι) R (⇑f : (a : M) → ι) 0) 1) ⋯

Tactic:
simp
-- 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 j : Multiplicative M
x : R[M]
h h₁ :
  HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
rw [map_add]

Premises used: map_add
-- 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 j : Multiplicative M
x : R[M]
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
{ rw [map_add] }

Premises used: map_add
-- 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 j : Multiplicative M
e_1 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
h h₁ :
  HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
rw [map_add]

Premises used: map_add
-- 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 j : Multiplicative M
e_1 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
{ rw [map_add] }

Premises used: map_add
-- 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 j : Multiplicative M
e_1 :
  (↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
          ((f : (a : M) → ι)
              (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
            ι)) →+
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) =
    (↥(gradeBy R (⇑f : (a : M) → ι)
          (HAdd.hAdd (α := ι) (β := ι)
            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι))) →+
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
h h₁ :
  HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
rw [map_add]

Premises used: map_add
-- 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 j : Multiplicative M
e_1 :
  (↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
          ((f : (a : M) → ι)
              (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
            ι)) →+
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) =
    (↥(gradeBy R (⇑f : (a : M) → ι)
          (HAdd.hAdd (α := ι) (β := ι)
            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι))) →+
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
{ rw [map_add] }

Premises used: map_add
-- 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 j : Multiplicative M
e_2 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
x : R[M]
h h₁ :
  HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
rw [map_add]

Premises used: map_add
-- 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 j : Multiplicative M
e_2 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
x : R[M]
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
{ rw [map_add] }

Premises used: map_add
-- 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 j : Multiplicative M
e_2 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
rw rw₁ :
  Eq (α := R[M])
    (Finsupp.single
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M))
      1)
    (single
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M))
      1)
⊢ Eq (α := R[M])
    (Finsupp.single
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M))
      1)
    (single
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M))
      (HMul.hMul (α := R) 1 1))

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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 j : Multiplicative M
e_2 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
⊢ Finsupp.single
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M))
      1 =
    HMul.hMul (α := R[M]) (β := R[M])
      (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) i) 1 : M →₀ R)
      (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) j) 1 : M →₀ R)

Tactic:
exact Eq.trans (by rw [one_mul]) (single_mul_single ..).symm

Premises used: AddMonoidAlgebra.single_mul_single, Eq.symm, Eq.trans
-- 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))
    ((decomposeAux f : (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:
(lift_single _ _ _).trans ?_

Premises used: AddMonoidAlgebra.lift_single, Eq.trans
-- 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
⊢ HSMul.hSMul (β := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) r
      (({
              toFun := fun (m : Multiplicative M) ↦
                ((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
                        ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) m : M) : ι) :
                      ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) m : M) : ι)) →+
                        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
                    (a :
                        ↥(gradeBy R (⇑f : (a : M) → ι)
                            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → 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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) m : M) : ι))
                      x)
                    (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) m) 1) ⋯),
              map_one' := ⋯, map_mul' := ⋯ : Multiplicative M →* ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i) } :
            (a : Multiplicative M) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) :
        ⨁ (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) ⋯)

Tactic:
(DirectSum.of_smul R _ _ _).symm.trans ?_

Premises used: DirectSum.of_smul, DFinsupp.single, Eq.symm, Eq.trans