L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
let S : L.Substructure M := ⟨range (Term.realize (L := L) ((↑) : s → M)), fun {n} f x hx => by
  simp only [mem_range] at *
  refine' ⟨func f fun i => Classical.choose (hx i), _⟩
  simp only [Term.realize, fun i => Classical.choose_spec (hx i)]⟩
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = ↑S
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
change _ = (S : Set M)
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ LowerAdjoint.toFun (closure L) s = S
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = ↑S
rw [← SetLike.ext'_iff]
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ LowerAdjoint.toFun (closure L) s = S
refine' closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => _)
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ ∃ y, Term.realize Subtype.val y = funMap f x
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)
⊢ funMap f x ∈ range (Term.realize Subtype.val)
simp only [mem_range] at *
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ Term.realize Subtype.val (func f fun i => Classical.choose (_ : ∃ y, Term.realize Subtype.val y = x i)) = funMap f x
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ ∃ y, Term.realize Subtype.val y = funMap f x
refine' ⟨func f fun i => Classical.choose (hx i), _⟩
no goals
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ Term.realize Subtype.val (func f fun i => Classical.choose (_ : ∃ y, Term.realize Subtype.val y = x i)) = funMap f x
simp only [Term.realize, fun i => Classical.choose_spec (hx i)]
case intro
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
t : Term L { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'
rintro _ ⟨t, rfl⟩
no goals
case intro
L : Language
M : Type w
N : Type ?u.30865
P : Type ?u.30868
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
t : Term L { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'
exact t.realize_mem _ fun i => hS' i.2