no goals
L : Language
L' : Language
M : Type w
N : Type ?u.819644
P : Type ?u.819647
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
⊢ M ⊨ nonemptyTheory L ↔ Nonempty M
simp only [nonemptyTheory, Theory.model_iff, Set.mem_singleton_iff, forall_eq,
  Sentence.realize_cardGe, Nat.cast_one, one_le_iff_ne_zero, mk_ne_zero_iff]