-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
rintro :
  ∀ (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)), (D ∩ (↑S : Set M)).Nonempty
rintro₁ rintro₂ :
  ∀ (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]),
    (D ∩ (↑S : Set M)).Nonempty
rintro₃ :
  ∀ (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]),
    let ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ);
    ∀ (hψM : M ⊨ ψ), (D ∩ (↑S : Set M)).Nonempty
rintro₄ :
  ∀ (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]),
    let ψ : (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 ⊨ ψ), (D ∩ (↑S : Set M)).Nonempty
rintro₅ :
  ∀ (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]),
    let ψ : (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), (D ∩ (↑S : Set M)).Nonempty
rintro₆ :
  ∀ (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]),
    let ψ : (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'), (D ∩ (↑S : Set M)).Nonempty
rintro₇ :
  ∀ (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]),
    let ψ : (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) ∈ D
rintro₈ :
  ∀ (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]),
    let ψ : (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')
      (hv'' : φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')), (↑(v' 0) : M) ∈ D
rintro₉ :
  ∀ (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]),
    let ψ : (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')
      (hv'' : φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')),
      Membership.mem (γ := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
⊢ MeetsDefinable.{u_1, u_2, u_3} (L := L) (↑S : Set M)

Tactic:
classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  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)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using hv''

Premises used: FirstOrder.Language.Sentence.Realize, SetLike.coe_sort_coe, Sum.elim_comp_inr, FirstOrder.Language.Formula.realize_relabel, FirstOrder.Language.Formula.realize_iExs