R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(cast R M h) a.snd = b.snd
⊢ ↑(reindex R M (Equiv.cast (_ : Fin a.fst = Fin b.fst))) a.snd = b.snd
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(cast R M h) a.snd = b.snd
⊢ a = b
refine' gradedMonoid_eq_of_reindex_cast h _
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(reindex R M (Fin.cast h).toEquiv) a.snd = b.snd
⊢ ↑(reindex R M (Equiv.cast (_ : Fin a.fst = Fin b.fst))) a.snd = b.snd
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(cast R M h) a.snd = b.snd
⊢ ↑(reindex R M (Equiv.cast (_ : Fin a.fst = Fin b.fst))) a.snd = b.snd
rw [cast] at h2
no goals
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(reindex R M (Fin.cast h).toEquiv) a.snd = b.snd
⊢ ↑(reindex R M (Equiv.cast (_ : Fin a.fst = Fin b.fst))) a.snd = b.snd
rw [← Fin.cast_to_equiv, ← h2]