no goals
L : Language
M : Type w
N : Type ?u.33484
P : Type ?u.33487
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
x : M
⊢ x ∈ LowerAdjoint.toFun (closure L) s ↔ ∃ t, Term.realize Subtype.val t = x
rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]