[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
f : M → ι
i : ι
m : M
h : m ∈ 0.support
⊢ f m = i
[PROOFSTEP]
cases h
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
⊢ gradeBy R id = grade R
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
f : M → ι
i : ι
a : AddMonoidAlgebra R M
⊢ a ∈ gradeBy R f i ↔ ↑a.support ⊆ f ⁻¹' {i}
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ a ∈ grade R m ↔ a.support ⊆ {m}
[PROOFSTEP]
rw [← Finset.coe_subset, Finset.coe_singleton]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ a ∈ grade R m ↔ ↑a.support ⊆ {m}
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ a ∈ grade R m ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
[PROOFSTEP]
rw [mem_grade_iff, Finsupp.support_subset_singleton']
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ (∃ b, a = Finsupp.single m b) ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ ↑(Finsupp.lsingle m) a_1 = a
[PROOFSTEP]
intro r
[GOAL]
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
r : R
⊢ a = Finsupp.single m r ↔ ↑(Finsupp.lsingle m) r = a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
r : R
⊢ a = Finsupp.single m r → ↑(Finsupp.lsingle m) r = a
[PROOFSTEP]
exact Eq.symm
[GOAL]
case h.mpr
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
r : R
⊢ ↑(Finsupp.lsingle m) r = a → a = Finsupp.single m r
[PROOFSTEP]
exact Eq.symm
[GOAL]
M : Type u_1
ι : Type u_2
R✝ : Type u_3
inst✝² : DecidableEq M
inst✝¹ : CommSemiring R✝
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
⊢ Finsupp.single m r ∈ gradeBy R f (f m)
[PROOFSTEP]
intro x hx
[GOAL]
M : Type u_1
ι : Type u_2
R✝ : Type u_3
inst✝² : DecidableEq M
inst✝¹ : CommSemiring R✝
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ (Finsupp.single m r).support
⊢ f x = f m
[PROOFSTEP]
rw [Finset.mem_singleton.mp (Finsupp.support_single_subset hx)]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ 1.support
⊢ ↑f m = 0
[PROOFSTEP]
rw [one_def] at h 
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (single 0 1).support
⊢ ↑f m = 0
[PROOFSTEP]
by_cases H : (1 : R) = (0 : R)
[GOAL]
case pos
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (single 0 1).support
H : 1 = 0
⊢ ↑f m = 0
[PROOFSTEP]
rw [H, single, Finsupp.single_zero] at h 
[GOAL]
case pos
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ 0.support
H : 1 = 0
⊢ ↑f m = 0
[PROOFSTEP]
cases h
[GOAL]
case neg
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (single 0 1).support
H : ¬1 = 0
⊢ ↑f m = 0
[PROOFSTEP]
rw [Finsupp.support_single_ne_zero _ H, Finset.mem_singleton] at h 
[GOAL]
case neg
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m = 0
H : ¬1 = 0
⊢ ↑f m = 0
[PROOFSTEP]
rw [h, AddMonoidHom.map_zero]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : AddMonoidAlgebra R M
ha : a ∈ gradeBy R (↑f) i
hb : b ∈ gradeBy R (↑f) j
c : M
hc : c ∈ (a * b).support
⊢ ↑f c = i + j
[PROOFSTEP]
set h := support_mul a b hc
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : AddMonoidAlgebra R M
ha : a ∈ gradeBy R (↑f) i
hb : b ∈ gradeBy R (↑f) j
c : M
hc : c ∈ (a * b).support
h : c ∈ Finset.biUnion a.support fun a₁ => Finset.biUnion b.support fun a₂ => {a₁ + a₂} := support_mul a b hc
⊢ ↑f c = i + j
[PROOFSTEP]
simp only [Finset.mem_biUnion] at h 
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : AddMonoidAlgebra R M
ha : a ∈ gradeBy R (↑f) i
hb : b ∈ gradeBy R (↑f) j
c : M
hc : c ∈ (a * b).support
h : ∃ a_1, a_1 ∈ a.support ∧ ∃ a, a ∈ b.support ∧ c ∈ {a_1 + a}
⊢ ↑f c = i + j
[PROOFSTEP]
rcases h with ⟨ma, ⟨hma, ⟨mb, ⟨hmb, hmc⟩⟩⟩⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : AddMonoidAlgebra R M
ha : a ∈ gradeBy R (↑f) i
hb : b ∈ gradeBy R (↑f) j
c : M
hc : c ∈ (a * b).support
ma : M
hma : ma ∈ a.support
mb : M
hmb : mb ∈ b.support
hmc : c ∈ {ma + mb}
⊢ ↑f c = i + j
[PROOFSTEP]
rw [← ha ma hma, ← hb mb hmb, Finset.mem_singleton.mp hmc]
[GOAL]
case intro.intro.intro.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : DecidableEq M
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : AddMonoidAlgebra R M
ha : a ∈ gradeBy R (↑f) i
hb : b ∈ gradeBy R (↑f) j
c : M
hc : c ∈ (a * b).support
ma : M
hma : ma ∈ a.support
mb : M
hmb : mb ∈ b.support
hmc : c ∈ {ma + mb}
⊢ ↑f (ma + mb) = ↑f ma + ↑f mb
[PROOFSTEP]
apply AddMonoidHom.map_add
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : DecidableEq M
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
⊢ SetLike.GradedMonoid (grade R)
[PROOFSTEP]
apply gradeBy.gradedMonoid (AddMonoidHom.id _)
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ GradedMonoid.mk (↑f (↑Multiplicative.toAdd 1))
      { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
        property := (_ : Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
    GradedMonoid.mk 0 GradedMonoid.GOne.one
[PROOFSTEP]
congr 2
[GOAL]
case h.e_3.h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ ↑f (↑Multiplicative.toAdd 1) = 0
[PROOFSTEP]
simp
[GOAL]
case h.e_4.e_2.h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ (fun x => x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) = fun x => x ∈ (fun i => gradeBy R (↑f) i) 0
[PROOFSTEP]
simp
[GOAL]
case h.e_4.e_4
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ HEq (_ : Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1)))
    (_ : 1 ∈ gradeBy R (↑f) 0)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
⊢ OneHom.toFun
      {
        toFun := fun m =>
          ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
            { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
              property :=
                (_ : Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
        map_one' :=
          (_ :
            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                  property :=
                    (_ : Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
      (i * j) =
    OneHom.toFun
        {
          toFun := fun m =>
            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
              { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                property :=
                  (_ : Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
          map_one' :=
            (_ :
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                  { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                    property :=
                      (_ :
                        Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
        i *
      OneHom.toFun
        {
          toFun := fun m =>
            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
              { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                property :=
                  (_ : Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
          map_one' :=
            (_ :
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                  { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                    property :=
                      (_ :
                        Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
        j
[PROOFSTEP]
symm
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
⊢ OneHom.toFun
        {
          toFun := fun m =>
            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
              { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                property :=
                  (_ : Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
          map_one' :=
            (_ :
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                  { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                    property :=
                      (_ :
                        Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
        i *
      OneHom.toFun
        {
          toFun := fun m =>
            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
              { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                property :=
                  (_ : Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
          map_one' :=
            (_ :
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                  { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                    property :=
                      (_ :
                        Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
        j =
    OneHom.toFun
      {
        toFun := fun m =>
          ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
            { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
              property :=
                (_ : Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
        map_one' :=
          (_ :
            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                  property :=
                    (_ : Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
      (i * j)
[PROOFSTEP]
dsimp only [toAdd_one, Eq.ndrec, Set.mem_setOf_eq, ne_eq, OneHom.toFun_eq_coe, OneHom.coe_mk, toAdd_mul]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd i)))
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) } *
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd j)))
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)))
      { val := Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1,
        property :=
          (_ :
            Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 ∈
              gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j))) }
[PROOFSTEP]
convert DirectSum.of_mul_of (A := (fun i : ι => gradeBy R f i)) _ _
[GOAL]
case h.e'_3.h.e'_1.h.e'_1.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_1.h.e'_3.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_2.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_4.e'_2.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
repeat {rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_1.h.e'_1.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_1.h.e'_3.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_2.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_4.e'_2.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_1.h.e'_1.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_1.h.e'_3.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_2.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_4.e'_2.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_1.h.e'_3.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_2.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_4.e'_2.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_2.h.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_4.e'_4.e'_2.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_4.e'_4.e'_2.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_4.e'_6.e'_4.e'_2.e'_2.e'_8
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝² :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝¹ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_3✝ : HEq (fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) fun x => ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }
e_1✝¹ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
e_4✝ : HEq AddZeroClass.toAdd AddZeroClass.toAdd
e_1✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_5.e'_5
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_1✝ :
  ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i }) =
    ({ x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) } →+
      ⨁ (i : ι), { x // x ∈ gradeBy R (↑f) i })
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_6.e'_2.h.h.e'_5.h.e'_7
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
x✝ : AddMonoidAlgebra R M
⊢ ↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) = ↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
{rw [AddMonoidHom.map_add]
}
[GOAL]
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    ↑(GradedMonoid.GMul.mul
        { val := Finsupp.single (↑Multiplicative.toAdd i) 1,
          property := (_ : Finsupp.single (↑Multiplicative.toAdd i) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i))) }
        { val := Finsupp.single (↑Multiplicative.toAdd j) 1,
          property :=
            (_ : Finsupp.single (↑Multiplicative.toAdd j) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd j))) })
[PROOFSTEP]
simp only [SetLike.coe_gMul]
[GOAL]
case h.e'_3.h.e'_6.e'_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    Finsupp.single (↑Multiplicative.toAdd i) 1 * Finsupp.single (↑Multiplicative.toAdd j) 1
[PROOFSTEP]
refine Eq.trans (by rw [one_mul]) single_mul_single.symm
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : Multiplicative M
e_2✝ :
  { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j)) } =
    { x // x ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd i) + ↑f (↑Multiplicative.toAdd j)) }
⊢ Finsupp.single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) 1 =
    single (↑Multiplicative.toAdd i + ↑Multiplicative.toAdd j) (1 * 1)
[PROOFSTEP]
rw [one_mul]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ ↑(decomposeAux f) (Finsupp.single m r) =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
      { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }
[PROOFSTEP]
refine' (lift_single _ _ _).trans _
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ r •
      ↑{
            toOneHom :=
              {
                toFun := fun m =>
                  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
                    { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                      property :=
                        (_ :
                          Finsupp.single (↑Multiplicative.toAdd m) 1 ∈ gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
                map_one' :=
                  (_ :
                    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                        { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                          property :=
                            (_ :
                              Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈
                                gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) },
            map_mul' :=
              (_ :
                ∀ (i j : Multiplicative M),
                  OneHom.toFun
                      {
                        toFun := fun m =>
                          ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
                            { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                              property :=
                                (_ :
                                  Finsupp.single (↑Multiplicative.toAdd m) 1 ∈
                                    gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
                        map_one' :=
                          (_ :
                            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                                { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                                  property :=
                                    (_ :
                                      Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈
                                        gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
                      (i * j) =
                    OneHom.toFun
                        {
                          toFun := fun m =>
                            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
                              { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                                property :=
                                  (_ :
                                    Finsupp.single (↑Multiplicative.toAdd m) 1 ∈
                                      gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
                          map_one' :=
                            (_ :
                              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                                  { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                                    property :=
                                      (_ :
                                        Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈
                                          gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                                ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
                        i *
                      OneHom.toFun
                        {
                          toFun := fun m =>
                            ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd m)))
                              { val := Finsupp.single (↑Multiplicative.toAdd m) 1,
                                property :=
                                  (_ :
                                    Finsupp.single (↑Multiplicative.toAdd m) 1 ∈
                                      gradeBy R (↑f) (↑f (↑Multiplicative.toAdd m))) },
                          map_one' :=
                            (_ :
                              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f (↑Multiplicative.toAdd 1)))
                                  { val := Finsupp.single (↑Multiplicative.toAdd 1) 1,
                                    property :=
                                      (_ :
                                        Finsupp.single (↑Multiplicative.toAdd 1) 1 ∈
                                          gradeBy R (↑f) (↑f (↑Multiplicative.toAdd 1))) } =
                                ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) 0) GradedMonoid.GOne.one) }
                        j) }
        (↑Multiplicative.ofAdd m) =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
      { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }
[PROOFSTEP]
refine' (DirectSum.of_smul R _ _ _).symm.trans _
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ ↑(DirectSum.of (fun i => (fun i => { x // x ∈ gradeBy R (↑f) i }) i)
          (↑f (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m))))
      (r •
        { val := Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) 1,
          property :=
            (_ :
              Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) 1 ∈
                gradeBy R (↑f) (↑f (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)))) }) =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
      { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }
[PROOFSTEP]
apply DirectSum.of_eq_of_gradedMonoid_eq
[GOAL]
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ GradedMonoid.mk (↑f (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)))
      (r •
        { val := Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) 1,
          property :=
            (_ :
              Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) 1 ∈
                gradeBy R (↑f) (↑f (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)))) }) =
    GradedMonoid.mk (↑f m) { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }
[PROOFSTEP]
refine' Sigma.subtype_ext rfl _
[GOAL]
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ ↑(GradedMonoid.mk (↑f (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)))
          (r •
            { val := Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) 1,
              property :=
                (_ :
                  Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) 1 ∈
                    gradeBy R (↑f) (↑f (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)))) })).snd =
    ↑(GradedMonoid.mk (↑f m)
          { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }).snd
[PROOFSTEP]
refine' (Finsupp.smul_single' _ _ _).trans _
[GOAL]
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) (r * 1) =
    ↑(GradedMonoid.mk (↑f m)
          { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }).snd
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ Finsupp.single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m)) r =
    ↑(GradedMonoid.mk (↑f m)
          { val := Finsupp.single m r, property := (_ : Finsupp.single m r ∈ gradeBy R (↑f) (↑f m)) }).snd
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : { x // x ∈ gradeBy R (↑f) i }
⊢ ↑(decomposeAux f) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) x
[PROOFSTEP]
obtain ⟨x, hx⟩ := x
[GOAL]
case mk
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : x ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := x, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := x, property := hx }
[PROOFSTEP]
revert hx
[GOAL]
case mk
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (hx : x ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := x, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := x, property := hx }
[PROOFSTEP]
refine' Finsupp.induction x _ _
[GOAL]
case mk.refine'_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (hx : 0 ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := 0, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx }
[PROOFSTEP]
intro hx
[GOAL]
case mk.refine'_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : 0 ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := 0, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx }
[PROOFSTEP]
symm
[GOAL]
case mk.refine'_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : 0 ∈ gradeBy R (↑f) i
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx } =
    ↑(decomposeAux f) ↑{ val := 0, property := hx }
[PROOFSTEP]
exact AddMonoidHom.map_zero _
[GOAL]
case mk.refine'_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (a : M) (b : R) (f_1 : M →₀ R),
    ¬a ∈ f_1.support →
      b ≠ 0 →
        (∀ (hx : f_1 ∈ gradeBy R (↑f) i),
            ↑(decomposeAux f) ↑{ val := f_1, property := hx } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := f_1, property := hx }) →
          ∀ (hx : Finsupp.single a b + f_1 ∈ gradeBy R (↑f) i),
            ↑(decomposeAux f) ↑{ val := Finsupp.single a b + f_1, property := hx } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i)
                { val := Finsupp.single a b + f_1, property := hx }
[PROOFSTEP]
intro m b y hmy hb ih hmby
[GOAL]
case mk.refine'_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
have : Disjoint (Finsupp.single m b).support y.support := by
  simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
⊢ Disjoint (Finsupp.single m b).support y.support
[PROOFSTEP]
simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]
[GOAL]
case mk.refine'_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
this : Disjoint (Finsupp.single m b).support y.support
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff] at hmby 
[GOAL]
case mk.refine'_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby✝ : Finsupp.single m b + y ∈ gradeBy R (↑f) i
hmby : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {i} ∧ ↑y.support ⊆ ↑f ⁻¹' {i}
this : Disjoint (Finsupp.single m b).support y.support
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby✝ } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby✝ }
[PROOFSTEP]
cases' hmby with h1 h2
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
this : Disjoint (Finsupp.single m b).support y.support
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {i}
h2 : ↑y.support ⊆ ↑f ⁻¹' {i}
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
have : f m = i := by rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff] at h1 
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
this : Disjoint (Finsupp.single m b).support y.support
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {i}
h2 : ↑y.support ⊆ ↑f ⁻¹' {i}
⊢ ↑f m = i
[PROOFSTEP]
rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff] at h1 
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
this✝ : Disjoint (Finsupp.single m b).support y.support
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {i}
h2 : ↑y.support ⊆ ↑f ⁻¹' {i}
this : ↑f m = i
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
subst this
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.support
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) (↑f m)),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) (↑f m)
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {↑f m}
h2 : ↑y.support ⊆ ↑f ⁻¹' {↑f m}
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
simp only [AlgHom.map_add, Submodule.coe_mk, decomposeAux_single f m]
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.support
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) (↑f m)),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) (↑f m)
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {↑f m}
h2 : ↑y.support ⊆ ↑f ⁻¹' {↑f m}
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
let ih' := ih h2
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.support
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) (↑f m)),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) (↑f m)
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {↑f m}
h2 : ↑y.support ⊆ ↑f ⁻¹' {↑f m}
ih' : ↑(decomposeAux f) ↑{ val := y, property := h2 } =
  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
dsimp at ih' 
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.support
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) (↑f m)),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) (↑f m)
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {↑f m}
h2 : ↑y.support ⊆ ↑f ⁻¹' {↑f m}
ih' : ↑(decomposeAux f) y =
  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
rw [ih', ← AddMonoidHom.map_add]
[GOAL]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.support
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) (↑f m)),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) (↑f m)
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {↑f m}
h2 : ↑y.support ⊆ ↑f ⁻¹' {↑f m}
ih' : ↑(decomposeAux f) y =
  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
      ({ val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
        { val := y, property := h2 }) =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
apply DirectSum.of_eq_of_gradedMonoid_eq
[GOAL]
case mk.refine'_2.intro.h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra R M
m : M
b : R
y : M →₀ R
hmy : ¬m ∈ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.support
ih :
  ∀ (hx : y ∈ gradeBy R (↑f) (↑f m)),
    ↑(decomposeAux f) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) (↑f m)
h1 : ↑(Finsupp.single m b).support ⊆ ↑f ⁻¹' {↑f m}
h2 : ↑y.support ⊆ ↑f ⁻¹' {↑f m}
ih' : ↑(decomposeAux f) y =
  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ GradedMonoid.mk (↑f m)
      ({ val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
        { val := y, property := h2 }) =
    GradedMonoid.mk (↑f m) { val := Finsupp.single m b + y, property := hmby }
[PROOFSTEP]
congr 2
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ AlgHom.comp (coeAlgHom (gradeBy R ↑f)) (decomposeAux f) = AlgHom.id R (AddMonoidAlgebra R M)
[PROOFSTEP]
ext : 2
[GOAL]
case h.h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x✝ : Multiplicative M
⊢ ↑(MonoidHom.comp (↑(AlgHom.comp (coeAlgHom (gradeBy R ↑f)) (decomposeAux f))) (of R M)) x✝ =
    ↑(MonoidHom.comp (↑(AlgHom.id R (AddMonoidAlgebra R M))) (of R M)) x✝
[PROOFSTEP]
simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, AlgHom.coe_comp, Function.comp_apply, of_apply, AlgHom.coe_id, id_eq]
[GOAL]
case h.h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x✝ : Multiplicative M
⊢ ↑(coeAlgHom (gradeBy R ↑f)) (↑(decomposeAux f) (single (↑Multiplicative.toAdd x✝) 1)) =
    single (↑Multiplicative.toAdd x✝) 1
[PROOFSTEP]
rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : { x // x ∈ gradeBy R (↑f) i }
⊢ ↑(decomposeAux f) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) x
[PROOFSTEP]
rw [decomposeAux_coe f x]
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ Decomposition (gradeBy R ↑f)
[PROOFSTEP]
infer_instance
[GOAL]
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ Decomposition (grade R)
[PROOFSTEP]
infer_instance
