-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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))
refine_1 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (L := L) (M := N) (α := Empty) BoundedFormula.falsum
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (L := L) (α := Empty) BoundedFormula.falsum default xs
refine_2 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (BoundedFormula.equal t₁ t₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (BoundedFormula.equal t₁ t₂).Realize default xs
refine_3 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n))
    (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (BoundedFormula.rel R ts)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (BoundedFormula.rel R ts).Realize default xs
refine_4 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n)
    (f₁_ih :
      ∀ (xs : Fin n → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₁.Realize default xs)
    (f₂_ih :
      ∀ (xs : Fin n → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₂.Realize default xs)
    (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs
⊢ ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → 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
have refine_5 : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (f_1 : L.BoundedFormula Empty (n + 1))
  (f_ih :
    ∀ (xs : Fin (n + 1) → M),
      BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f_1
          (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
        f_1.Realize default xs)
  (xs : Fin n → M),
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∀' f_1)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
    (∀' f_1).Realize default xs
Tactic: refine fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_