awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
⊢ a = Finsupp.single m r ↔ (Finsupp.lsingle m : (a : R) → R[M]) r = a
have h : a = Finsupp.single m r → (Finsupp.lsingle m : (a : R) → R[M]) r = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
h : a = Finsupp.single m r → (Finsupp.lsingle m : (a : R) → R[M]) r = a
⊢ a = Finsupp.single m r ↔ (Finsupp.lsingle m : (a : R) → R[M]) r = a
have h₁ : (Finsupp.lsingle m : (a : R) → R[M]) r = a → a = Finsupp.single m r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
ι : Type u_2
R : Type u_4
inst : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ Finsupp.support (single m r)
⊢ f x = f m
have rw : f m = f m
Tactic: rw [Finset.mem_singleton.mp (Finsupp.support_single_subset hx)]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (hypothesis)
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
m : M
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) 1) m
⊢ Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) m : ι) (0 : ι)
have h₁ : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) m
Tactic: rw [one_def] at h
Cleared hypotheses: h
-- 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 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
m : M
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) m
⊢ Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) m : ι) (0 : ι)
have obtain : ∀ (h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) 0),
  Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) 0 : ι) (0 : ι)
Tactic: obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h
Cleared hypotheses: m, h
-- 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 : 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
⊢ (f : (a : M) → ι) c = i + j
have 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
Tactic: obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c :=
      Finset.mem_add.1 <| support_mul a b hc
Cleared hypotheses: c, hc
-- 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 : 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
⊢ (f : (a : M) → ι) (ma + mb) = i + j
have rw : HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ma : ι) ((f : (a : M) → ι) mb : ι) = i + j
Tactic: rw [map_add, ha ma hma, hb mb hmb]
-- 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 : 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
⊢ (f : (a : M) → ι) (ma + mb) = i + j
have rw₁ : HAdd.hAdd (β := ι) i ((f : (a : M) → ι) mb : ι) = i + j
Tactic: rw [map_add, ha ma hma, hb mb hmb]
-- 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 : 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
⊢ (f : (a : M) → ι) (ma + mb) = i + j
have rw₂ : i + j = i + j
Tactic: rw [map_add, ha ma hma, hb mb hmb]
-- 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 : 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
⊢ (f : (a : M) → ι) c = i + j
have 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
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]
Cleared hypotheses: c, hc
-- 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 →+ ι
⊢ 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))
have h : Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι) (0 : ι)
Tactic: congr 2
-- 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 →+ ι
h : Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) 1 : M) : ι) (0 : ι)
⊢ 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))
have 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
Tactic: congr 2
-- 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 →+ ι
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
⊢ 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))
have 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))
  sorry (β := Membership.mem (γ := Submodule R R[M]) (gradeBy.{u_1, u_2, u_3} (ι := ι) R (⇑f : (a : M) → ι) 0) 1) sorry
Tactic: congr 2
-- 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 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) : ι)
have 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) : ι)
Tactic: rw [map_add]
-- 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 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) : ι)
have 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) : ι)
Tactic: rw [map_add]
-- 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 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) : ι)
have 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) : ι)
Tactic: rw [map_add]
-- 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 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) : ι)
have 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) : ι)
Tactic: rw [map_add]
-- 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 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) : ι)))
⊢ 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))
have 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)
Tactic: rw [one_mul]
-- 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 →+ ι
m : M
r : R
⊢ Eq (α := R[M])
    (single
        ((Multiplicative.toAdd : (a : Multiplicative M) → M)
          ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M))
        (r * 1) :
      R[M])
    ((↑(Sigma.snd (α := ι) (β := fun (a : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) a))
            (GradedMonoid.mk (A := fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) 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) → ι) m : ι)) x)
                  (Finsupp.single m r) ⋯) :
              GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))) :
        R[M]) :
      R[M])
have h : Eq (α := R[M])
  (single
      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
        ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M))
      r :
    R[M])
  ((↑(Sigma.snd (α := ι) (β := fun (a : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) a))
          (GradedMonoid.mk (A := fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) 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) → ι) m : ι)) x)
                (Finsupp.single m r) sorry) :
            GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))) :
      R[M]) :
    R[M])
Tactic: rw [mul_one]
-- 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: obtain ⟨x, hx⟩ := x
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 →+ ι
i : ι
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))
have revert : ∀ (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: revert hx
Cleared hypotheses: hx