From 11439d8ca1018f7b9242762c2c55aee379a16f84 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 4 Nov 2021 18:49:11 +0000
Subject: [PATCH] chore(algebra/direct_sum/internal): add missing simp lemmas
 (#10154)

These previously weren't needed when these were `@[reducible] def`s as `simp` saw right through them.
---
 src/algebra/direct_sum/internal.lean |  5 +++++
 src/algebra/graded_monoid.lean       | 11 +++++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/algebra/direct_sum/internal.lean b/src/algebra/direct_sum/internal.lean
index 8ca549b7c67b6..ab0e4e73c852a 100644
--- a/src/algebra/direct_sum/internal.lean
+++ b/src/algebra/direct_sum/internal.lean
@@ -141,6 +141,11 @@ instance galgebra [add_monoid ι]
     sigma.subtype_ext ((zero_add i).trans (add_zero i).symm) $ algebra.commutes _ _,
   smul_def := λ r ⟨i, xi⟩, sigma.subtype_ext (zero_add i).symm $ algebra.smul_def _ _ }
 
+@[simp] lemma set_like.coe_galgebra_to_fun [add_monoid ι]
+  [comm_semiring S] [semiring R] [algebra S R]
+  (A : ι → submodule S R) [h : set_like.graded_monoid A] (s : S) :
+    ↑(@direct_sum.galgebra.to_fun _ S (λ i, A i) _ _ _ _ _ _ _ s) = (algebra_map S R s : R) := rfl
+
 /-- A direct sum of powers of a submodule of an algebra has a multiplicative structure. -/
 instance nat_power_graded_monoid
   [comm_semiring S] [semiring R] [algebra S R] (p : submodule S R) :
diff --git a/src/algebra/graded_monoid.lean b/src/algebra/graded_monoid.lean
index b6e4b440b4c32..e9eda4abd2892 100644
--- a/src/algebra/graded_monoid.lean
+++ b/src/algebra/graded_monoid.lean
@@ -316,6 +316,9 @@ instance set_like.ghas_one {S : Type*} [set_like S R] [has_one R] [has_zero ι]
   [set_like.has_graded_one A] : graded_monoid.ghas_one (λ i, A i) :=
 { one := ⟨1, set_like.has_graded_one.one_mem⟩ }
 
+@[simp] lemma set_like.coe_ghas_one {S : Type*} [set_like S R] [has_one R] [has_zero ι] (A : ι → S)
+  [set_like.has_graded_one A] : ↑(@graded_monoid.ghas_one.one _ (λ i, A i) _ _) = (1 : R) := rfl
+
 /-- A version of `graded_monoid.ghas_one` for internally graded objects. -/
 class set_like.has_graded_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι]
   (A : ι → S) : Prop :=
@@ -326,6 +329,10 @@ instance set_like.ghas_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι] (
   graded_monoid.ghas_mul (λ i, A i) :=
 { mul := λ i j a b, ⟨(a * b : R), set_like.has_graded_mul.mul_mem a.prop b.prop⟩ }
 
+@[simp] lemma set_like.coe_ghas_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι] (A : ι → S)
+  [set_like.has_graded_mul A] {i j : ι} (x : A i) (y : A j) :
+    ↑(@graded_monoid.ghas_mul.mul _ (λ i, A i) _ _ _ _ x y) = (x * y : R) := rfl
+
 /-- A version of `graded_monoid.gmonoid` for internally graded objects. -/
 class set_like.graded_monoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
   (A : ι → S) extends set_like.has_graded_one A, set_like.has_graded_mul A : Prop
@@ -348,6 +355,10 @@ instance set_like.gmonoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
   ..set_like.ghas_one A,
   ..set_like.ghas_mul A }
 
+@[simp] lemma set_like.coe_gpow {S : Type*} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S)
+  [set_like.graded_monoid A] {i : ι} (x : A i) (n : ℕ) :
+    ↑(@graded_monoid.gmonoid.gnpow _ (λ i, A i) _ _ n _ x) = (x ^ n : R) := rfl
+
 /-- Build a `gcomm_monoid` instance for a collection of subobjects. -/
 instance set_like.gcomm_monoid {S : Type*} [set_like S R] [comm_monoid R] [add_comm_monoid ι]
   (A : ι → S) [set_like.graded_monoid A] :