-- Mathlib/Algebra/MonoidAlgebra/Grading.lean
theorem decomposeAux_single (m : M) (r : R) :
    decomposeAux f (Finsupp.single m r) =
      DirectSum.of (fun i : ι => gradeBy R f i) (f m)
        ⟨Finsupp.single m r, single_mem_gradeBy _ _ _⟩

Proof state:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
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 • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩

Tactic:
refine Sigma.subtype_ext rfl ?_

Result:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
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 • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩)).snd =
    ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd

Proof state:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m)) (r * 1) = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd

Tactic:
rw [mul_one]

Result:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m)) r = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd

Proof state:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ r •
      {
          toFun := fun m =>
            (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd m)))
              ⟨Finsupp.single (Multiplicative.toAdd m) 1, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯ }
        (Multiplicative.ofAdd m) =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩

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

Result:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd (Multiplicative.ofAdd m))))
      (r • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩

Proof state:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
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 • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩)).snd =
    ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd

Tactic:
refine (smul_single' _ _ _).trans ?_

Result:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m)) (r * 1) = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd

Proof state:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m)) r = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd (Multiplicative.ofAdd m))))
      (r • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Result:
case h
M : Type u_1
ι : Type u_2
R : Type u_3
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 • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩

Proof state:
M : Type u_1
ι : Type u_2
R : Type u_3
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 => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩

Tactic:
refine (lift_single _ _ _).trans ?_

Result:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ r •
      {
          toFun := fun m =>
            (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd m)))
              ⟨Finsupp.single (Multiplicative.toAdd m) 1, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯ }
        (Multiplicative.ofAdd m) =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩