-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (hypothesis)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  Formula.Realize (α := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
      (Formula.relabel (α := ↥φ.freeVarFinset ⊕ Fin n)
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n)))
        (BoundedFormula.toFormula (φ.restrictFreeVar id)))
      ((↑f : M → N) ∘
        Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
          (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
          (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
            (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n)) ↔
    Formula.Realize (α := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
      (Formula.relabel (α := ↥φ.freeVarFinset ⊕ Fin n)
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n)))
        (BoundedFormula.toFormula (φ.restrictFreeVar id)))
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
        (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
          (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
      (φ.restrictFreeVar id)
      (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
      ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
have h₁ : BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
    (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
      (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
        ((↑f : M → N) ∘
          Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
            (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
            (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
              (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
      Sum.inl)
    (Function.comp.{1, u_5 + 1, u_2 + 1} (β := ↥φ.freeVarFinset ⊕ Fin n)
      (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
        ((↑f : M → N) ∘
          Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
            (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
            (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
              (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
      Sum.inr) ↔
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
    (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
      (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
        (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
          (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
          (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
            (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
      Sum.inl)
    (Function.comp.{1, u_5 + 1, u_1 + 1} (β := ↥φ.freeVarFinset ⊕ Fin n)
      (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
        (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
          (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
          (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
            (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
      Sum.inr)
Tactic: simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula] at h
Cleared hypotheses: h