awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
b : M
hb :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
h : BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)
refine_5 :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
refine_5₁ refine_5₂ :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))

Tactic:
rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]

Premises used: Fin.comp_snoc, Inhabited.default, Function.comp, Unique.eq_default, DFunLike.coe
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ f.toElementaryEmbedding.toEmbedding = f.toEmbedding

Tactic:
rfl

Premises used: FirstOrder.Language.StrongHomClass.toEmbedding, FirstOrder.Language.Equiv.toEmbedding, rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Eq (α := (a : M) → N) (⇑f.toElementaryEmbedding : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
inst : L.Structure M
α : Type u_5
S : L.Substructure M
v : α → ↥S
t : L.Term α
⊢ Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v) t = (↑(Term.realize v t) : M)

Tactic:
HomClass.realize_term S.subtype

Premises used: FirstOrder.Language.HomClass.realize_term, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
x x_1 : L.ElementarySubstructure M
s : Set M
hs1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
hs2 : { carrier := s, fun_mem := @hs1 : L.Substructure M }.IsElementary
t : Set M
ht1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f t
isElementary' : { carrier := t, fun_mem := @ht1 : L.Substructure M }.IsElementary
h :
  Eq.{u_1 + 1} (α := Set M)
    ((fun (x : L.ElementarySubstructure M) ↦ (↑(↑x : L.Substructure M) : Set M))
      { toSubstructure := { carrier := s, fun_mem := @hs1 }, isElementary' := hs2 })
    ((fun (x : L.ElementarySubstructure M) ↦ (↑(↑x : L.Substructure M) : Set M))
      { toSubstructure := { carrier := t, fun_mem := @ht1 }, isElementary' := isElementary' })
⊢ { toSubstructure := { carrier := s, fun_mem := @hs1 : L.Substructure M }, isElementary' := hs2 :
      L.ElementarySubstructure M } =
    { toSubstructure := { carrier := t, fun_mem := @ht1 }, isElementary' := isElementary' }

Tactic:
congr
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
⊢ (↑S : L.Substructure M).IsElementary

Tactic:
S.isElementary'

Premises used: FirstOrder.Language.ElementarySubstructure.isElementary'
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
x : ↥S
⊢ (S.subtype : (a : ↥S) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
⊢ Function.Injective (α := ↥S) (β := M) (⇑S.subtype : (a : ↥S) → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
⊢ Eq (α := (a : ↥S) → M) (⇑S.subtype : (a : ↥S) → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
x : M
⊢ Membership.mem (γ := L.ElementarySubstructure M) ⊤ x

Tactic:
Set.mem_univ x

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

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
φ : L.Sentence
⊢ Sentence.Realize.{u_2, u_3, u_1} (↥S) φ ↔ M ⊨ φ

Tactic:
S.subtype.map_sentence φ

Premises used: FirstOrder.Language.ElementarySubstructure.subtype, FirstOrder.Language.ElementaryEmbedding.map_sentence
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
T : L.Theory
⊢ Theory.Model.{u_2, u_3, u_1} (↥S) T ↔ M ⊨ T

Tactic:
simp only [Theory.model_iff, realize_sentence]

Premises used: FirstOrder.Language.Theory.model_iff, FirstOrder.Language.ElementarySubstructure.realize_sentence
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
T : L.Theory
h : M ⊨ T
S : L.ElementarySubstructure M
⊢ Theory.Model.{u_2, u_3, u_1} (↥S) T

Tactic:
(theory_model_iff S T).2 h

Premises used: Iff.mpr, FirstOrder.Language.ElementarySubstructure.theory_model_iff
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Nonempty M
S : L.ElementarySubstructure M
⊢ Nonempty.{u_1 + 1} ↥S

Tactic:
(model_nonemptyTheory_iff L).1 inferInstance

Premises used: inferInstance, Iff.mp, FirstOrder.Language.model_nonemptyTheory_iff
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
⊢ ↥S ≅[L] M

Tactic:
S.subtype.elementarilyEquivalent

Premises used: FirstOrder.Language.ElementarySubstructure.subtype, FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M),
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ x) a) →
      ∃ (b : ↥S),
        BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ x) (↑b : M))
⊢ S.IsElementary

Tactic:
fun _ => S.subtype.isElementary_of_exists htv

Premises used: FirstOrder.Language.Substructure.IsElementary, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.Embedding.isElementary_of_exists
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) = A

Tactic:
Subset.antisymm ?_ subset_closure

Premises used: Set.Subset.antisymm, FirstOrder.Language.Substructure.subset_closure
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
refine : (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) ⊆ A
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) = A

Tactic:
refine Subset.antisymm ?_ subset_closure

Premises used: Set.Subset.antisymm, FirstOrder.Language.Substructure.subset_closure
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
rw : range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A))) ⊆ A
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) ⊆ A

Tactic:
rw [coe_closure_eq_range_term_realize]

Premises used: FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
x : M
hx :
  Membership.mem (γ := Set M)
    (range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)))) x
obtain :
  ∀ (t : Term.{u_2, u_3, u_1} L { x : M // x ∈ A }),
    A.Definable₁ L {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t}
⊢ A.Definable₁ L {x}

Tactic:
obtain ⟨t, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
t : Term.{u_2, u_3, u_1} L { x : M // x ∈ A }
h :
  Eq.{u_1 + 1} (α := Set (Fin 1 → M))
    {x : Fin 1 → M | Membership.mem (γ := Set M) {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t} (x 0)}
    (setOf (Formula.Realize (Term.equal (var 0) (Term.varsToConstants (Term.relabel Sum.inl t)))))
⊢ A.Definable₁ L {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t}

Tactic:
use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants

Premises used: FirstOrder.Language.Term.relabel, FirstOrder.Language.Term.equal, Sum.inl, FirstOrder.Language.Term.var, FirstOrder.Language.Term.varsToConstants, OfNat.ofNat
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
t : Term.{u_2, u_3, u_1} L { x : M // x ∈ A }
⊢ Eq.{u_1 + 1} (α := Set (Fin 1 → M))
    {x : Fin 1 → M | Membership.mem (γ := Set M) {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t} (x 0)}
    (setOf (Formula.Realize (Term.equal (var 0) (Term.varsToConstants (Term.relabel Sum.inl t)))))

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
x : M
hx :
  Membership.mem (γ := Set M)
    (range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)))) x
⊢ A.Definable₁ L {x}

Tactic:
have : A.Definable₁ L {x} := by
    obtain ⟨t, rfl⟩ := hx
    use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants
    simp [Set.ext_iff]
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
x : M
hx :
  Membership.mem (γ := Set M)
    (range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)))) x
this : A.Definable₁ L {x}
⊢ x ∈ A

Tactic:
singleton_inter_nonempty.mp <| hA _ (singleton_nonempty x) this

Premises used: Set.singleton_nonempty, Iff.mp, Set.singleton_inter_nonempty
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
x : M
hx :
  Membership.mem (γ := Set M)
    (range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)))) x
this : A.Definable₁ L {x}
⊢ x ∈ A

Tactic:
exact singleton_inter_nonempty.mp <| hA _ (singleton_nonempty x) this

Premises used: Set.singleton_nonempty, Iff.mp, Set.singleton_inter_nonempty
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
⊢ IsElementary (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)

Tactic:
isElementary_of_exists ((closure L).toFun A) ?_

Premises used: LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure, FirstOrder.Language.Substructure.isElementary_of_exists
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
refine :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A))
    (a : M),
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
          (Subtype.val (p := fun (x : M) ↦
              Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
            x)
          a) →
      ∃ (b : ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)),
        BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
            (Subtype.val (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
              x)
            (↑b : M))
⊢ IsElementary (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)

Tactic:
refine isElementary_of_exists ((closure L).toFun A) ?_

Premises used: LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure, FirstOrder.Language.Substructure.isElementary_of_exists
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
⊢ D.Nonempty

Tactic:
have hD_ne : D.Nonempty := ⟨a,hφ⟩
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
nth_rw : (↑(x j) : M) ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M)
⊢ (↑(x j) : M) ∈ A

Tactic:
nth_rw 1 [← hA.closure_eq_self]

Premises used: FirstOrder.Language.MeetsDefinable.closure_eq_self
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
⊢ (↑(x j) : M) ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M)

Tactic:
simp only [Subtype.coe_prop]

Premises used: Subtype.coe_prop
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
refine :
  Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D}
    (setOf
      (Formula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1))
        (BoundedFormula.subst
          (Formula.relabel (Sum.elim Empty.elim id)
            (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ)))
          fun (i : Fin (n + 1)) ↦
          Fin.lastCases (motive := fun (x : Fin (n + 1)) ↦
            (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Term (Fin 1)) (var 0)
            (fun (j : Fin n) ↦ Constants.term (L.con (Subtype.mk (p := fun (x : M) ↦ x ∈ A) (↑(x j) : M) ⋯))) i)))
⊢ ∃ (φ : (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Formula (Fin 1)),
    Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)

Tactic:
refine ⟨((L.lhomWithConstants A).onBoundedFormula φ).toFormula.relabel
      (Sum.elim Empty.elim id) |>.subst fun i => Fin.lastCases (Term.var 0)
        (fun j => (L.con ⟨x j, by
        nth_rw 1 [← hA.closure_eq_self]
        simp only [Subtype.coe_prop]
        ⟩).term) i, ?_⟩
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
h :
  ∀ (v : Fin 1 → M),
    Membership.mem (γ := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} v ↔
      Membership.mem (γ := Set (Fin 1 → M))
        (setOf
          (Formula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1))
            (BoundedFormula.subst
              (Formula.relabel (Sum.elim Empty.elim id)
                (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ)))
              fun (i : Fin (n + 1)) ↦
              Fin.lastCases (motive := fun (x : Fin (n + 1)) ↦
                (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Term (Fin 1)) (var 0)
                (fun (j : Fin n) ↦ Constants.term (L.con (Subtype.mk (p := fun (x : M) ↦ x ∈ A) (↑(x j) : M) ⋯))) i)))
        v
⊢ Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D}
    (setOf
      (Formula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1))
        (BoundedFormula.subst
          (Formula.relabel (Sum.elim Empty.elim id)
            (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ)))
          fun (i : Fin (n + 1)) ↦
          Fin.lastCases (motive := fun (x : Fin (n + 1)) ↦
            (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Term (Fin 1)) (var 0)
            (fun (j : Fin n) ↦ Constants.term (L.con (Subtype.mk (p := fun (x : M) ↦ x ∈ A) (↑(x j) : M) ⋯))) i)))

Tactic:
ext v