-- Module: Mathlib.ModelTheory.ElementaryMaps
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 :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (((↑f : M → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) ((↑f : M → N) ∘ xs) ↔
    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)
rw :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
          (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
          (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
            (⇑(_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 (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
          (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
          (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
            (⇑(_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) ↔
    φ.Realize v xs
rw₁ :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      ((Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs ∘ id) ∘ Sum.inl)
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs ∘ id) Sum.inr) ↔
    φ.Realize v xs
rw₂ :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs ∘ Sum.inl)
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs) Sum.inr) ↔
    φ.Realize v xs
rw₃ :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset))
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs) Sum.inr) ↔
    φ.Realize v xs
rw₄ :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs ↔
    φ.Realize v xs
rw₅ rw₆ : φ.Realize v xs ↔ φ.Realize v xs
⊢ 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) ↔
    φ.Realize v xs

Tactic:
rw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self,
      Function.comp_id, Sum.elim_comp_inl, Sum.elim_comp_inr (v ∘ Subtype.val) xs,
      BoundedFormula.realize_restrictFreeVar v (by simp)]

Premises used: Function.comp_id, Equiv.symm_comp_self, Sum.elim_comp_inr, Sum.elim_comp_inl, Function.comp, Fintype.equivFin, Subtype.val, DFunLike.coe, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar, Function.comp_assoc