R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ↑(cast R M (_ : i = i)) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^i) M)
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
h : i = j
⊢ ↑(cast R M h) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^j) M)
subst h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ↑(LinearEquiv.refl R ((⨂[R]^i) M)) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^i) M)
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ↑(cast R M (_ : i = i)) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^i) M)
rw [cast_refl]
no goals
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ↑(LinearEquiv.refl R ((⨂[R]^i) M)) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^i) M)
rfl