-- 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
rw :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
      (φ.restrictFreeVar (Set.inclusion (s := (↑φ.freeVarFinset : Set α)) (t := (↑φ.freeVarFinset : Set α)) ⋯))
      (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
      ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
rw₁ rw₂ rw₃ :
  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
rw₄ :
  ∀
    (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
rw₅ :
  ∀
    (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)),
    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
rw₆ :
  ∀
    (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)),
    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
rw₇ :
  ∀
    (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)),
    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
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs

Tactic:
classical
    rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]
    have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
    simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula] at h
    rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
      Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _),
      _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl,
      Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h
    refine h.trans ?_
    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, Set.inclusion_eq_id, FirstOrder.Language.Formula.realize_relabel, Fintype.equivFin, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar', Set.Subset.rfl, Sum.inr, Equiv.symm, Subtype.val, DFunLike.coe, FirstOrder.Language.BoundedFormula.realize_toFormula, Function.comp_assoc