L : Language
M : Type w
N : Type ?u.648999
P : Type ?u.649002
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ ∃ x_1, p x x_1
L : Language
M : Type w
N : Type ?u.648999
P : Type ?u.649002
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ p x hx
refine' Exists.elim _ fun (hx : x ∈ closure L s) (hc : p x hx) => hc
no goals
L : Language
M : Type w
N : Type ?u.648999
P : Type ?u.649002
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ ∃ x_1, p x x_1
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun