L : Language
M : Type w
N : Type ?u.34066
P : Type ?u.34069
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#↑(range (Term.realize Subtype.val))) ≤ (#Term L ↑s)
L : Language
M : Type w
N : Type ?u.34066
P : Type ?u.34069
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#{ x // x ∈ LowerAdjoint.toFun (closure L) s }) ≤ (#Term L ↑s)
rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]
L : Language
M : Type w
N : Type ?u.34066
P : Type ?u.34069
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#↑(range (Term.realize Subtype.val))) ≤ lift (#Term L ↑s)
L : Language
M : Type w
N : Type ?u.34066
P : Type ?u.34069
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#↑(range (Term.realize Subtype.val))) ≤ (#Term L ↑s)
rw [← Cardinal.lift_id'.{w, max u w} (#L.Term s)]
no goals
L : Language
M : Type w
N : Type ?u.34066
P : Type ?u.34069
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#↑(range (Term.realize Subtype.val))) ≤ lift (#Term L ↑s)
exact Cardinal.mk_range_le_lift