Theorem: LO.FirstOrder.Structure.ofEquiv_val (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
n : ℕ
e : Fin n → N
ε : μ → N
t : Semiterm L μ n
⊢ Semiterm.val (ofEquiv φ) e ε t = φ (Semiterm.val s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε) t)
Tactic:
induction t <;> simp [*, Semiterm.val_func, ofEquiv_func φ, Function.comp]
State after:
no goals