awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ ℵ₀ ≤ #(↑s' : Type (max w w'))

Tactic:
exact h1
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
⊢ ClosedUnder.{u, v, w} (M := M) f Set.univ

Tactic:
fun _ _ => mem_univ _

Premises used: FirstOrder.Language.ClosedUnder, Set.mem_univ, FirstOrder.Language.Structure.funMap
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
s t : Set M
hs : ClosedUnder f s
ht : ClosedUnder f t
⊢ ClosedUnder f (s ∩ t)

Tactic:
fun x h =>
  mem_inter (hs x fun i => mem_of_mem_inter_left (h i)) (ht x fun i => mem_of_mem_inter_right (h i))

Premises used: Set.mem_of_mem_inter_left, FirstOrder.Language.ClosedUnder, Set.mem_inter, Set.mem_of_mem_inter_right
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
s t : Set M
hs : ClosedUnder f s
ht : ClosedUnder f t
⊢ ClosedUnder f (s ⊓ t)

Tactic:
hs.inter ht

Premises used: FirstOrder.Language.ClosedUnder.inter
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
S : Set (Set M)
hS : ∀ s ∈ S, ClosedUnder f s
⊢ ClosedUnder f (InfSet.sInf S)

Tactic:
fun x h s hs =>
  hS s hs x fun i => h i s hs

Premises used: Set.Mem, setOf, FirstOrder.Language.ClosedUnder
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
p q : L.Substructure M
h : (↑p : Set M) = (↑q : Set M)
mk :
  ∀ (carrier : Set M) (fun_mem : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier)
    (h : (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) = (↑q : Set M)),
    { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
q : L.Substructure M
carrier : Set M
fun_mem : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier
h : (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) = (↑q : Set M)
mk :
  ∀ (carrier_1 : Set M) (fun_mem_1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier_1)
    (h :
      (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) =
        (↑{ carrier := carrier_1, fun_mem := @fun_mem_1 : L.Substructure M } : Set M)),
    { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = { carrier := carrier_1, fun_mem := @fun_mem_1 }
⊢ { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = q

Tactic:
cases q
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
carrier : Set M
fun_mem : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier
carrier_1 : Set M
fun_mem_1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier_1
h :
  (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) =
    (↑{ carrier := carrier_1, fun_mem := @fun_mem_1 : L.Substructure M } : Set M)
⊢ { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = { carrier := carrier_1, fun_mem := @fun_mem_1 }

Tactic:
congr
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : L.Substructure M
x : M
⊢ x ∈ (↑s : Set M) ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S T : L.Substructure M
h : ∀ (x : M), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize.{u, v, w, u_3} (L := L) xs (var a) ∈ S

Tactic:
h a

Premises used: Set.Mem, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize.{u, v, w, u_3} (L := L) xs (var a) ∈ S

Tactic:
exact h a
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
l : ℕ
f : L.Functions l
ts : Fin l → L.Term α
ih : ∀ (a : Fin l), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S

Tactic:
Substructure.fun_mem _ _ _ ih

Premises used: Set.Mem, FirstOrder.Language.Substructure.fun_mem, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
l : ℕ
f : L.Functions l
ts : Fin l → L.Term α
ih : ∀ (a : Fin l), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S

Tactic:
exact Substructure.fun_mem _ _ _ ih

Premises used: FirstOrder.Language.Substructure.fun_mem
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
t : L.Term α
xs : α → M
h : ∀ (a : α), xs a ∈ S
var : ∀ (a : α), realize.{u, v, w, u_3} (L := L) xs (Language.var a) ∈ S
func :
  ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term α) (ih : ∀ (a : Fin l), realize xs (ts a) ∈ S),
    realize xs (Language.func f ts) ∈ S
⊢ realize xs t ∈ S

Tactic:
induction t with
  | var a => exact h a
  | func f ts ih => exact Substructure.fun_mem _ _ _ ih

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
s : Set M
hs : s = (↑S : Set M)
⊢ (↑(S.copy s hs) : Set M) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
s : Set M
hs : s = (↑S : Set M)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
c : L.Constants
⊢ (↑c : M) ∈ S

Tactic:
mem_carrier.2 (S.fun_mem c _ finZeroElim)

Premises used: Iff.mpr, finZeroElim, Set.Mem, FirstOrder.Language.Substructure.fun_mem, FirstOrder.Language.Substructure.mem_carrier
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
x : M
⊢ Membership.mem (γ := L.Substructure M) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ (↑⊤ : Set M) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
p p' : L.Substructure M
⊢ (↑(p ⊓ p') : Set M) = (↑p : Set M) ∩ (↑p' : Set M)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
p p' : L.Substructure M
x : M
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
pos :
  ∀ (h : t ∈ s),
    ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
neg :
  ∀ (h : t ∉ s),
    ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
⊢ ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)

Tactic:
by_cases h : t ∈ s
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
h : t ∈ s
⊢ ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)

Tactic:
simpa [h] using t.fun_mem f

Premises used: FirstOrder.Language.Substructure.fun_mem
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
h : t ∉ s
⊢ ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)

Tactic:
simp [h]
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : Set (L.Substructure M)
⊢ (↑(sInf S) : Set M) = ⋂ s ∈ S, (↑s : Set M)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : Set (L.Substructure M)
x : M
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
x : M
⊢ Membership.mem (γ := L.Substructure M) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, FirstOrder.Language.Substructure.mem_sInf
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ (↑(⨅ (i : ι), S i) : Set M) = ⋂ (i : ι), (↑(S i) : Set M)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, FirstOrder.Language.Substructure.coe_sInf, Set.biInter_range
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
x : M
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x ↔
    ∀ (S : L.Substructure M), s ⊆ (↑S : Set M) → x ∈ S

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, FirstOrder.Language.Substructure.mem_sInf
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ s ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M)

Tactic:
(closure L).le_closure s

Premises used: LowerAdjoint.le_closure, FirstOrder.Language.Substructure.closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
P : M
hP : P ∉ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: FirstOrder.Language.Substructure.subset_closure, Not
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ LowerAdjoint.closed (u := SetLike.coe) (closure L) (↑S : Set M)

Tactic:
congr rfl ((closure L).eq_of_le Set.Subset.rfl fun _x xS => mem_closure.2 fun _T hT => hT xS)

Premises used: Iff.mpr, FirstOrder.Language.Substructure.mem_closure, setOf, Set.Subset.rfl, congr, FirstOrder.Language.Substructure.closure, LowerAdjoint.eq_of_le, LowerAdjoint.closed, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
s : Set M
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s ≤ S ↔ s ⊆ (↑S : Set M)

Tactic:
(closure L).closure_le_closed_iff_le s S.closed

Premises used: LowerAdjoint.closure_le_closed_iff_le, Set.Subset, FirstOrder.Language.Substructure.closure, FirstOrder.Language.Substructure.closed
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s t : Set M
h : s ⊆ t
⊢ LE.le (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t)

Tactic:
(closure L).monotone h

Premises used: Set.Mem, Set.Subset, LowerAdjoint.monotone, FirstOrder.Language.Substructure.closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
s : Set M
h₁ : s ⊆ (↑S : Set M)
h₂ : S ≤ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s = S

Tactic:
(closure L).eq_of_le h₁ h₂

Premises used: FirstOrder.Language.Substructure.closure, LowerAdjoint.eq_of_le
-- Module: Mathlib.ModelTheory.Substructures
Goal:
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),
    Membership.mem (γ := Set M)
      (range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) (x i)
⊢ ∀ (i : Fin n),
    ∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x i

Tactic:
simp only [mem_range] at *

Premises used: Set.mem_range
-- Module: Mathlib.ModelTheory.Substructures
Goal:
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.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x i
⊢ ∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = funMap f x

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

Premises used: FirstOrder.Language.Term.func, Exists.intro, Classical.choose
-- Module: Mathlib.ModelTheory.Substructures
Goal:
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.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x i
refine :
  Term.realize (α := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))
      (func f fun (i : Fin n) ↦
        Classical.choose (p := fun (x_1 : Term.{u, v, w} L { x : M // x ∈ s }) ↦
          Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) x_1 = x i) ⋯) =
    funMap f x
⊢ ∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = funMap f x

Tactic:
refine ⟨func f fun i => Classical.choose (hx i), ?_⟩
-- Module: Mathlib.ModelTheory.Substructures
Goal:
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.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x i
⊢ Term.realize (α := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))
      (func f fun (i : Fin n) ↦
        Classical.choose (p := fun (x_1 : Term.{u, v, w} L { x : M // x ∈ s }) ↦
          Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) x_1 = x i) ⋯) =
    funMap f x

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

Premises used: Classical.choose_spec, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
change : (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) = (↑S : Set M)
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) =
    range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))

Tactic:
change _ = (S : Set M)

Premises used: SetLike.coe
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
rw : LowerAdjoint.toFun (u := SetLike.coe) (closure L) s = S
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) = (↑S : Set M)

Tactic:
rw [← SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s = S

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

Premises used: Subtype.mk, FirstOrder.Language.Substructure.closure_eq_of_le, FirstOrder.Language.Term.var, Exists.intro, le_sInf, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
refine :
  ∀ (S' : L.Substructure M)
    (hS' : Membership.mem (γ := Set (L.Substructure M)) {S : L.Substructure M | s ⊆ (↑S : Set M)} S'), S ≤ S'
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s = S

Tactic:
refine closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => ?_)
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
S' : L.Substructure M
hS' : Membership.mem (γ := Set (L.Substructure M)) {S : L.Substructure M | s ⊆ (↑S : Set M)} S'
t : Term.{u, v, w} L { x : M // x ∈ s }
⊢ Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t ∈ S'

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

Premises used: FirstOrder.Language.Term.realize_mem, Subtype.property
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
S' : L.Substructure M
hS' : Membership.mem (γ := Set (L.Substructure M)) {S : L.Substructure M | s ⊆ (↑S : Set M)} S'
t : Term.{u, v, w} L { x : M // x ∈ s }
⊢ Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t ∈ S'

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

Premises used: FirstOrder.Language.Term.realize_mem, Subtype.property
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set M
inst_3 : Small.{u, w} (↑s : Type w)
rw :
  Small.{u, w}
    (↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
      Type w)
⊢ Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
rw [← SetLike.coe_sort_coe, Substructure.coe_closure_eq_range_term_realize]

Premises used: SetLike.coe_sort_coe, FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set M
inst_3 : Small.{u, w} (↑s : Type w)
⊢ Small.{u, w}
    (↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
      Type w)

Tactic:
small_range _

Premises used: small_range
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set M
inst_3 : Small.{u, w} (↑s : Type w)
⊢ Small.{u, w}
    (↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
      Type w)

Tactic:
exact small_range _

Premises used: small_range
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
x : M
rw :
  x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
rw₁ :
  Membership.mem (γ := Set M)
      (range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
rw₂ rw₃ :
  (∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x) ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x

Tactic:
rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]

Premises used: Set.mem_range, SetLike.mem_coe, FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
rw :
  lift.{max u w, w}
      #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
          Type w) ≤
    #(Term.{u, v, w} L (↑s : Type w))
⊢ lift.{max u w, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤ #(Term.{u, v, w} L (↑s : Type w))

Tactic:
rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]

Premises used: SetLike.coe_sort_coe, FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
rw :
  lift.{max u w, w}
      #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
          Type w) ≤
    lift.{w, max u w} #(Term.{u, v, w} L (↑s : Type w))
⊢ lift.{max u w, w}
      #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
          Type w) ≤
    #(Term.{u, v, w} L (↑s : Type w))

Tactic:
rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ lift.{max u w, w}
      #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
          Type w) ≤
    lift.{w, max u w} #(Term.{u, v, w} L (↑s : Type w))

Tactic:
Cardinal.mk_range_le_lift

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ lift.{max u w, w}
      #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
          Type w) ≤
    lift.{w, max u w} #(Term.{u, v, w} L (↑s : Type w))

Tactic:
exact Cardinal.mk_range_le_lift

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
rw :
  lift.{max w u, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
⊢ lift.{u, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤
    max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
rw [← lift_umax]

Premises used: Cardinal.lift_umax