Theorem: Submodule.iSup_eq_span' (DividedPowers/SubDPIdeal.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
p : ι → Submodule R M
h : ι → Prop
⊢ ⨆ i, ⨆ (_ : h i), p i = span R (⋃ i, ⋃ (_ : h i), ↑(p i))
Tactic:
simp_rw [← Submodule.iSup_span, Submodule.span_eq]
State after:
no goals