-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem map_boundedFormula (f : M ↪ₑ[L] N) {α : Type*} {n : ℕ} (φ : L.BoundedFormula α n)
    (v : α → M) (xs : Fin n → M) : φ.Realize (f ∘ v) (f ∘ xs) ↔ φ.Realize v xs

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) = φ.Realize v xs

Tactic:
refine h.trans ?_

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr) =
    φ.Realize v xs

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) = φ.Realize v xs

Tactic:
have h :=
  f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
    (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (Formula.relabel (⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)))
          (φ.restrictFreeVar id).toFormula).Realize
      (↑f ∘ Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ↔
    (Formula.relabel (⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)))
          (φ.restrictFreeVar id).toFormula).Realize
      (Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) = φ.Realize v xs

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id, iff_eq_eq]

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) = φ.Realize v xs

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr) =
    φ.Realize v xs

Tactic:
erw [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,
  ← Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl,
  BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl]

Result:
no goals

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize
      (((↑f ∘ Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((↑f ∘ Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr) =
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) = φ.Realize v xs

Tactic:
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

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin ({ x // x ∈ φ.freeVarFinset } ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) = φ.Realize v xs