awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ 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))

Tactic:
lift_card_closure_le_card_term.trans (Term.card_le.trans ?_)

Premises used: FirstOrder.Language.Substructure.lift_card_closure_le_card_term, FirstOrder.Language.Term.card_le, LE.le.trans
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
refine :
  max ℵ₀ #(Sum.{w, u} (↑s : Type w) ((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
⊢ 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))

Tactic:
refine lift_card_closure_le_card_term.trans (Term.card_le.trans ?_)

Premises used: FirstOrder.Language.Substructure.lift_card_closure_le_card_term, FirstOrder.Language.Term.card_le, LE.le.trans
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
rw :
  max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
rw₁ rw₂ :
  max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
⊢ max ℵ₀ #(Sum.{w, u} (↑s : Type w) ((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
rw [mk_sum, lift_umax.{w, u}]

Premises used: Cardinal.mk_sum
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s ↔
    ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s

Tactic:
⟨fun h n f => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
refine_1 :
  ∀ (h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s) (n : ℕ)
    (f : L.Functions n), ClosedUnder f s
refine_2 :
  ∀ (h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s),
    Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s ↔
    ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s

Tactic:
refine ⟨fun h n f => ?_, fun h => ?_⟩
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
n : ℕ
f : L.Functions n
refine_1 : ClosedUnder f (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M)
⊢ ClosedUnder f s

Tactic:
rw [← h]
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
n : ℕ
f : L.Functions n
⊢ ClosedUnder f (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M)

Tactic:
Substructure.fun_mem _ _

Premises used: FirstOrder.Language.Substructure.fun_mem
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
n : ℕ
f : L.Functions n
⊢ ClosedUnder f (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M)

Tactic:
exact Substructure.fun_mem _ _

Premises used: FirstOrder.Language.Substructure.fun_mem
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) { carrier := s, fun_mem := ⋯ }

Tactic:
have h' : closure L s = ⟨s, h⟩ := closure_eq_of_le (refl _) subset_closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
h' : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) { carrier := s, fun_mem := ⋯ }
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s

Tactic:
congr_arg _ h'

Premises used: Set.Mem, setOf, congr_arg, LowerAdjoint.closed
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
h' : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) { carrier := s, fun_mem := ⋯ }
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s

Tactic:
exact congr_arg _ h'

Premises used: congr_arg
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : L.IsRelational
s : Set M
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s

Tactic:
(mem_closed_iff s).2 isEmptyElim

Premises used: Iff.mpr, isEmptyElim, FirstOrder.Language.Substructure.mem_closed_iff
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : L.IsRelational
s : Set M
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) = s

Tactic:
LowerAdjoint.closure_eq_self_of_mem_closed _ (mem_closed_of_isRelational L s)

Premises used: FirstOrder.Language.Substructure.mem_closed_of_isRelational, LowerAdjoint.closure_eq_self_of_mem_closed
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : L.IsRelational
s : Set M
m : M
rw : m ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔ m ∈ s
rw₁ rw₂ : m ∈ s ↔ m ∈ s
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) m ↔ m ∈ s

Tactic:
rw [← SetLike.mem_coe, closure_eq_of_isRelational]

Premises used: FirstOrder.Language.Substructure.closure_eq_of_isRelational, SetLike.mem_coe
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
inst_1 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
h : s.Countable
⊢ Countable.{w + 1} (↑s : Type w)

Tactic:
haveI : Countable s := h.to_subtype
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
inst_1 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable.{w + 1} (↑s : Type w)
rw : lift.{max u w, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤ ℵ₀
⊢ Countable.{w + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
rw [← mk_le_aleph0_iff, ← lift_le_aleph0]

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

Tactic:
lift_card_closure_le_card_term.trans mk_le_aleph0

Premises used: Cardinal.mk_le_aleph0, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, LE.le.trans
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
inst_1 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable.{w + 1} (↑s : Type w)
⊢ lift.{max u w, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤ ℵ₀

Tactic:
exact lift_card_closure_le_card_term.trans mk_le_aleph0

Premises used: Cardinal.mk_le_aleph0, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, LE.le.trans
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
p : M → Prop
x : M
h : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
⊢ p x

Tactic:
(@closure_le L M _ ⟨setOf p, fun {_} => Hfun⟩ _).2 Hs h

Premises used: Iff.mpr, Set.Mem, setOf, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
p : M → Prop
x : M
s : Set M
hs : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
have :
  ∀
    (this :
      ∀ (x : M), Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x → p x),
    p x
⊢ p x

Tactic:
have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
p : M → Prop
x : M
s : Set M
hs : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
this : ∀ (x : M), Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x → p x
⊢ p x

Tactic:
simpa [hs] using this x
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑S : Set M) = S

Tactic:
(Substructure.gi L M).l_u_eq S

Premises used: FirstOrder.Language.Substructure.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Eq.{w + 1} (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) ⊥

Tactic:
(Substructure.gi L M).gc.l_bot

Premises used: Set.Mem, FirstOrder.Language.Substructure.gi, setOf, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Eq.{w + 1} (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Set.univ) ⊤

Tactic:
@coe_top L M _ ▸ closure_eq ⊤

Premises used: Eq.rec, FirstOrder.Language.Substructure.coe_top, Top.top, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s t : Set M
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (s ∪ t))
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t)

Tactic:
(Substructure.gi L M).gc.l_sup

Premises used: Set.Mem, FirstOrder.Language.Substructure.gi, setOf, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
m : M
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (insert m s))
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
closure_union {m} s

Premises used: Set.insert, Set.Mem, setOf, FirstOrder.Language.Substructure.closure_union, Set.singleton, Singleton.singleton
-- 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
rw : Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅)
⊢ Small.{u, w} ↥⊥

Tactic:
rw [← closure_empty]

Premises used: FirstOrder.Language.Substructure.closure_empty
-- 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
⊢ Small.{u, w} (↑∅ : Type w)

Tactic:
haveI : Small.{u} (∅ : Set M) := small_subsingleton _
-- 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
this : Small.{u, w} (↑∅ : Type w)
⊢ Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅)

Tactic:
Substructure.small_closure

Premises used: FirstOrder.Language.Substructure.small_closure
-- 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
this : Small.{u, w} (↑∅ : Type w)
⊢ Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅)

Tactic:
exact Substructure.small_closure

Premises used: FirstOrder.Language.Substructure.small_closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
simp_rw :
  Eq.{w + 1} (α := L.Substructure M) (⨆ (i : ι), S i)
    (⨆ (i : ι), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑(S i) : Set M))
⊢ Eq.{w + 1} (α := L.Substructure M) (⨆ (i : ι), S i)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M)))

Tactic:
simp_rw [closure_iUnion, closure_eq]

Premises used: FirstOrder.Language.Substructure.closure_iUnion, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Premises used: _private.0.FirstOrder.Language.Substructure.mem_iSup_of_directed.match_1, iSup, Membership.mem, le_iSup, Iff.intro
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
refine : Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
this :
  Membership.mem (γ := L.Substructure M)
      (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x →
    ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Premises used: FirstOrder.Language.Substructure.closure_iUnion, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
suffices :
  Membership.mem (γ := L.Substructure M)
      (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x →
    ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
suffices x ∈ closure L (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := L.Substructure M)
      (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x →
    ∃ (i : ι), x ∈ S i

Tactic:
fun hx ↦ closure_induction hx (fun _ ↦ mem_iUnion.1) (fun f v hC ↦ ?_)

Premises used: FirstOrder.Language.Substructure.closure_induction
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
refine :
  ∀
    (hx :
      Membership.mem (γ := L.Substructure M)
        (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x)
    {n : ℕ} (f : L.Functions n) (v : Fin n → M)
    (hC : ∀ (i : Fin n), Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (v i)),
    Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (funMap f v)
⊢ Membership.mem (γ := L.Substructure M)
      (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x →
    ∃ (i : ι), x ∈ S i

Tactic:
refine fun hx ↦ closure_induction hx (fun _ ↦ mem_iUnion.1) (fun f v hC ↦ ?_)
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
hx :
  Membership.mem (γ := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x
n : ℕ
f : L.Functions n
v : Fin n → M
hC : ∀ (i : Fin n), Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (v i)
⊢ ∀ (i : Fin n), ∃ (i_1 : ι), v i ∈ S i_1

Tactic:
simp_rw [Set.mem_setOf] at *

Premises used: Set.mem_setOf
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
hx :
  Membership.mem (γ := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x
n : ℕ
f : L.Functions n
v : Fin n → M
hC : ∀ (i : Fin n), ∃ (i_1 : ι), v i ∈ S i_1
have :
  ∀ (i : ι) (hi : ∀ (i_1 : Fin n), S (Classical.choose (p := fun (x : ι) ↦ v i_1 ∈ S x) ⋯) ≤ S i),
    ∃ (i : ι), funMap f v ∈ S i
⊢ ∃ (i : ι), funMap f v ∈ S i

Tactic:
have ⟨i, hi⟩ := hS.finite_le (fun i ↦ Classical.choose (hC i))
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
hx :
  Membership.mem (γ := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x
n : ℕ
f : L.Functions n
v : Fin n → M
hC : ∀ (i : Fin n), ∃ (i_1 : ι), v i ∈ S i_1
i : ι
hi : ∀ (i_1 : Fin n), S (Classical.choose (p := fun (x : ι) ↦ v i_1 ∈ S x) ⋯) ≤ S i
⊢ ∃ (i : ι), funMap f v ∈ S i

Tactic:
⟨i, (S i).fun_mem f v (fun j ↦ hi j (Classical.choose_spec (hC j)))⟩

Premises used: FirstOrder.Language.Substructure.fun_mem, Classical.choose_spec, Exists.intro
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
hx :
  Membership.mem (γ := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x
n : ℕ
f : L.Functions n
v : Fin n → M
hC : ∀ (i : Fin n), ∃ (i_1 : ι), v i ∈ S i_1
i : ι
hi : ∀ (i_1 : Fin n), S (Classical.choose (p := fun (x : ι) ↦ v i_1 ∈ S x) ⋯) ≤ S i
⊢ ∃ (i : ι), funMap f v ∈ S i

Tactic:
refine ⟨i, (S i).fun_mem f v (fun j ↦ hi j (Classical.choose_spec (hC j)))⟩
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ Nonempty.{w + 1} (↑S : Type w)

Tactic:
haveI : Nonempty S := Sne.to_subtype
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
this : Nonempty.{w + 1} (↑S : Type w)
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Premises used: FirstOrder.Language.Substructure.mem_iSup_of_directed, Subtype.exists, exists_prop, DirectedOn.directed_val, sSup_eq_iSup'
-- 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 : IsEmpty.{u + 1} L.Constants
⊢ IsEmpty.{w + 1} ↥⊥

Tactic:
(isEmpty_subtype _).2 (fun x => ?_)

Premises used: Iff.mpr, isEmpty_subtype
-- 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 : IsEmpty.{u + 1} L.Constants
refine : ∀ (x : M), x ∉ ⊥
⊢ IsEmpty.{w + 1} ↥⊥

Tactic:
refine (isEmpty_subtype _).2 (fun x => ?_)

Premises used: Iff.mpr, isEmpty_subtype
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
rw : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder.{u, v, w} (M := M) f ∅
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) ∅

Tactic:
rw [mem_closed_iff]

Premises used: FirstOrder.Language.Substructure.mem_closed_iff
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
n : ℕ
f : L.Functions n
zero : ∀ (f : L.Functions 0), ClosedUnder.{u, v, w} (M := M) f ∅
succ : ∀ (n : ℕ) (f : L.Functions (n + 1)), ClosedUnder.{u, v, w} (M := M) f ∅
⊢ ClosedUnder.{u, v, w} (M := M) f ∅

Tactic:
cases n
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
f : L.Functions 0
⊢ ClosedUnder.{u, v, w} (M := M) f ∅

Tactic:
isEmptyElim f

Premises used: isEmptyElim
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
f : L.Functions 0
⊢ ClosedUnder.{u, v, w} (M := M) f ∅

Tactic:
exact isEmptyElim f
-- 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 : IsEmpty.{u + 1} L.Constants
x_1 : M
n : ℕ
f : L.Functions (n + 1)
x : Fin (n + 1) → M
hx : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set M) ∅ (x i)
⊢ Membership.mem (γ := Set M) ∅ (funMap f x)

Tactic:
simp only [mem_empty_iff_false, forall_const] at hx

Premises used: Set.mem_empty_iff_false, forall_const
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) ∅

Tactic:
have h : (∅ : Set M) ∈ (closure L).closed := by
    rw [mem_closed_iff]
    intro n f
    cases n
    · exact isEmptyElim f
    · intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) ∅
rw : x ∉ ∅
⊢ x ∉ ⊥

Tactic:
rw [← closure_empty, ← SetLike.mem_coe, h]

Premises used: FirstOrder.Language.Substructure.closure_empty, SetLike.mem_coe