-- Mathlib/ModelTheory/Substructures.lean
theorem coe_closure_eq_range_term_realize :
    (closure L s : Set M) = range (@Term.realize L _ _ _ ((↑) : s → M))

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)
⊢ funMap f x ∈ range (Term.realize Subtype.val)

Tactic:
simp only [mem_range] at *

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions 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

Proof state:
case intro
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
t : L.Term { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'

Tactic:
exact t.realize_mem _ fun i => hS' i.2

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ (closure L).toFun s = S

Tactic:
refine closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => ?_)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions 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 ⋯) = funMap f x

Tactic:
simp only [Term.realize, fun i => Classical.choose_spec (hx i)]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions 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

Tactic:
refine ⟨func f fun i => Classical.choose (hx i), ?_⟩

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions 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 ⋯) = funMap f x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = range (Term.realize Subtype.val)

Tactic:
change _ = (S : Set M)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = ↑S

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = ↑S

Tactic:
rw [← SetLike.ext'_iff]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ (closure L).toFun s = S

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ ↑((closure L).toFun s) = range (Term.realize Subtype.val)

Tactic:
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)]⟩

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = range (Term.realize Subtype.val)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'

Tactic:
rintro _ ⟨t, rfl⟩

Result:
case intro
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
t : L.Term { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'