no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), Set.Nonempty a → ∃ M', M' ∈ a ∧ ∀ (I : Submodule R M), I ∈ a → ¬I < M') ↔ IsArtinian R M
rw [isArtinian_iff_wellFounded, WellFounded.wellFounded_iff_has_min]