-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
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
⊢ 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)
have h : 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) sorry))) a))
        default)
      (Sum.inl ∘ Sum.elim Empty.elim id) ∘
    Sum.inr)
Tactic: congr! 1