R : Type u_4
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_1
ι : ιι → Type u_2
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : ↑(reindex R M (Equiv.cast (_ : ι { fst := ai, snd := a }.fst = ι { fst := ai, snd := b }.fst))) a = b
⊢ { fst := ai, snd := a } = { fst := ai, snd := b }
R : Type u_4
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_1
ι : ιι → Type u_2
ai : ιι
a : ⨂[R] (x : ι ai), M
bi : ιι
b : ⨂[R] (x : ι bi), M
hi : ai = bi
h : ↑(reindex R M (Equiv.cast (_ : ι { fst := ai, snd := a }.fst = ι { fst := bi, snd := b }.fst))) a = b
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
subst hi
no goals
R : Type u_4
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_1
ι : ιι → Type u_2
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : ↑(reindex R M (Equiv.cast (_ : ι { fst := ai, snd := a }.fst = ι { fst := ai, snd := b }.fst))) a = b
⊢ { fst := ai, snd := a } = { fst := ai, snd := b }
simp_all