Theorem: LO.FirstOrder.Semiterm.val_Uprod (Logic/FirstOrder/Ultraproduct.lean)

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
e : Fin n → Uprod A 𝓤
ε : μ → Uprod A 𝓤
t : Semiterm L μ n
⊢ valm (Uprod A 𝓤) e ε t = { val := fun i => val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) t }
Tactic:
induction t <;> simp[*, val_func]
State after:
no goals