awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
v : Fin 1 → 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)
        (v 0)) ↔
    BoundedFormula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) (M := M)
      (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ))
      (Function.comp (β := Fin (n + 1) ⊕ Fin 0)
        (Sum.elim
          (fun (a : Fin (n + 1)) ↦
            Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
              (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) ⋯))) a))
          default)
        (Sum.inl ∘ Sum.elim Empty.elim id))
      default
⊢ 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

Tactic:
simp only [Fin.isValue, mem_setOf_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]

Premises used: Function.comp_id, Fin.castAdd_zero, Set.mem_setOf_eq, FirstOrder.Language.BoundedFormula.realize_relabel, FirstOrder.Language.BoundedFormula.realize_subst, FirstOrder.Language.Formula.relabel, Fin.isValue, Nat.add_zero, Fin.natAdd_zero, Fin.cast_refl, FirstOrder.Language.Formula.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
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
v : Fin 1 → M
h :
  ∀ (i : Fin (n + 1)),
    Eq.{u_1 + 1} (α := M)
      (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)
          (v 0) i :
        M)
      ((Function.comp (β := Fin (n + 1) ⊕ Fin 0)
              (Sum.elim
                (fun (a : Fin (n + 1)) ↦
                  Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
                    (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) ⋯)))
                      a))
                default)
              (Sum.inl ∘ Sum.elim Empty.elim id) ∘
            Sum.inr)
          i :
        M)
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → M)
    (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)
      (v 0))
    (Function.comp (β := Fin (n + 1) ⊕ Fin 0)
        (Sum.elim
          (fun (a : Fin (n + 1)) ↦
            Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
              (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) ⋯))) a))
          default)
        (Sum.inl ∘ Sum.elim Empty.elim id) ∘
      Sum.inr)

Tactic:
ext 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
v : Fin 1 → M
⊢ Eq.{u_1 + 1} (α := M)
    (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)
        (v 0) (Fin.last n) :
      M)
    ((Function.comp (β := Fin (n + 1) ⊕ Fin 0)
            (Sum.elim
              (fun (a : Fin (n + 1)) ↦
                Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
                  (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) ⋯)))
                    a))
              default)
            (Sum.inl ∘ Sum.elim Empty.elim id) ∘
          Sum.inr)
        (Fin.last n) :
      M)

Tactic:
simp
-- 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
v : Fin 1 → M
i : Fin n
⊢ Eq.{u_1 + 1} (α := M)
    (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)
        (v 0) i.castSucc :
      M)
    ((Function.comp (β := Fin (n + 1) ⊕ Fin 0)
            (Sum.elim
              (fun (a : Fin (n + 1)) ↦
                Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
                  (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) ⋯)))
                    a))
              default)
            (Sum.inl ∘ Sum.elim Empty.elim id) ∘
          Sum.inr)
        i.castSucc :
      M)

Tactic:
simp
-- 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
⊢ A.Definable₁ L D

Tactic:
have hD : A.Definable₁ L D := by
    simp only [Definable₁, Definable, Fin.isValue]
    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, ?_⟩
    ext v
    simp only [Fin.isValue, mem_setOf_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]
    rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula]
    congr! 1
    ext i; cases i using Fin.lastCases <;> simp
-- 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
hD : A.Definable₁ L D
obtain :
  ∀ (b : M) (hbD : b ∈ D) (hbA : b ∈ 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))
⊢ ∃ (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))

Tactic:
obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD
-- 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
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ A
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hbA : b ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M)),
    Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) b
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) b

Tactic:
rwa [← hA.closure_eq_self] at hbA

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
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ 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))

Tactic:
exact ⟨⟨b, by rwa [← hA.closure_eq_self] at hbA⟩, hbD⟩
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
⊢ ∀ (x : Fin 1 → M), x 0 ∈ D ↔ φ.Realize x

Tactic:
simp [Set.ext_iff] at hφ

Premises used: Set.ext_iff
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : ∀ (x : Fin 1 → M), x 0 ∈ D ↔ φ.Realize x
⊢ φ.Realize ![x]

Tactic:
simp [← hφ, hx]
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
⊢ φ.Realize ![x]

Tactic:
have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
⊢ M ⊨ ψ

Tactic:
simpa only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
      Formula.realize_relabel, Sum.elim_comp_inr, ψ] using
        (⟨![x], hφx⟩ : ∃ w : Fin 1 → M, φ.Realize w)

Premises used: FirstOrder.Language.Sentence.Realize, SetLike.coe_sort_coe, Sum.elim_comp_inr, FirstOrder.Language.Formula.realize_relabel, Exists.intro, Matrix.vecEmpty, Matrix.vecCons, FirstOrder.Language.Formula.realize_iExs
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
⊢ M ⊨ ψ

Tactic:
have hψM : ψ.Realize M := by
    simpa only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
      Formula.realize_relabel, Sum.elim_comp_inr, ψ] using
        (⟨![x], hφx⟩ : ∃ w : Fin 1 → M, φ.Realize w)
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
rwa :
  Realize.{u_2, u_3, u_1, u_1} (L := L) (M := ↥S)
    ((_root_.Equiv.symm equivSentence :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
      ψ)
    fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)
rwa₁ :
  Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1))
    ((_root_.Equiv.symm equivSentence :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
      ψ)
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S))
rwa₂ rwa₃ rwa₄ rwa₅ : M ⊨ ψ
⊢ ↥S ⊨ ψ

Tactic:
rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]

Premises used: FirstOrder.Language.ElementarySubstructure.subtype, FirstOrder.Language.Formula.realize_equivSentence_symm_con, FirstOrder.Language.ElementaryEmbedding.map_formula, FirstOrder.Language.Formula.realize_equivSentence_symm
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
⊢ ↥S ⊨ ψ

Tactic:
have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
hψS : ↥S ⊨ ψ
⊢ ∃ (i : Fin 1 → ↥S), φ.Realize i

Tactic:
simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS

Premises used: FirstOrder.Language.Sentence.Realize, SetLike.coe_sort_coe, Sum.elim_comp_inr, FirstOrder.Language.Formula.realize_relabel, FirstOrder.Language.Formula.realize_iExs
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
hψS : ∃ (i : Fin 1 → ↥S), φ.Realize i
obtain : ∀ (v' : Fin 1 → ↥S) (hv' : φ.Realize v'), (D ∩ (↑S : Set M)).Nonempty
⊢ (D ∩ (↑S : Set M)).Nonempty

Tactic:
obtain ⟨v', hv'⟩ := hψS
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ (↑(v' 0) : M) ∈ (↑S : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
refine : (↑(v' 0) : M) ∈ D
⊢ (D ∩ (↑S : Set M)).Nonempty

Tactic:
refine ⟨v' 0, ?_, by simp⟩