∀ {R : Type u_3} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_1}
  (S : ι → Submodule R M) (x : M) (motive : (∃ i, x ∈ ↑(S i).toAddSubmonoid) → Prop)
  (x_1 : ∃ i, x ∈ ↑(S i).toAddSubmonoid), (∀ (i : ι) (hi : x ∈ ↑(S i).toAddSubmonoid), motive ⋯) → motive x_1