L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
intro a ha
L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
simp only [SetLike.mem_coe]
L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
a' : Language.Constants (L[[↑A]]) := Sum.inr { val := a, property := ha }
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
let a' : L[[A]].Constants := Sum.inr ⟨a, ha⟩
no goals
L : Language
M : Type w
N : Type ?u.681989
P : Type ?u.681992
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
a' : Language.Constants (L[[↑A]]) := Sum.inr { val := a, property := ha }
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
exact constants_mem a'