feat(model_theory/semantics): A simp lemma for `Theory.model` (#13117)
feat(model_theory/semantics): A simp lemma for `Theory.model` (#13117)

Defines `Theory.model_iff` to make it easier to show when a structure models a theory.



Co-authored-by: Aaron Anderson <6a708ae528ec3e8bbcd87cbd53c0d4f4bab63d64@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib