no goals
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(collectedBasis h v) a ∈ A a.fst
simp