-- 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.{u_2, u_3, u_1, 0} (M := M) φ
      (Function.comp (β := Empty ⊕ Fin (n + 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))
        Sum.inl)
      (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)
⊢ 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

Tactic:
rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula]

Premises used: FirstOrder.Language.LHom.realize_onBoundedFormula, FirstOrder.Language.BoundedFormula.realize_toFormula, FirstOrder.Language.Formula.Realize