I need show that the following lemma

  0 [`&0 <= theta1`]
  1 [`theta1 < theta 2`]
  2 [`theta2 <= &2 * pi`]
  3 [`theta1 = f_azim_fan x V E v u i`]
  4 [`theta2 = f_azim_fan x V E v u (i + 1)`]
  5 [`x''$1 > &0`]
  6 [`x''$2 > f_azim_fan x V E v u i`]
  7 [`x''$2 < f_azim_fan x V E v u (i + 1)`]
  8 [`x''$3 > &0`]
  9 [`x''$3 < h`]
 10 [`x' =
      x +
      (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
      (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
      (x''$1 * cos (x''$3)) % e3_fan x v u`]
`azim x v u x' = x''$2`
I use REWRITE_TAC[azim_def] we have

  0 [`&0 <= theta1`]
  1 [`theta1 < theta 2`]
  2 [`theta2 <= &2 * pi`]
  3 [`theta1 = f_azim_fan x V E v u i`]
  4 [`theta2 = f_azim_fan x V E v u (i + 1)`]
  5 [`x''$1 > &0`]
  6 [`x''$2 > f_azim_fan x V E v u i`]
  7 [`x''$2 < f_azim_fan x V E v u (i + 1)`]
  8 [`x''$3 > &0`]
  9 [`x''$3 < h`]
 10 [`x' =
      x +
      (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
      (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
      (x''$1 * cos (x''$3)) % e3_fan x v u`]

`(@theta. &0 <= theta /\
          theta < &2 * pi /\
          (?h1 h2.
               !e1 e2 e3.
                   orthonormal e1 e2 e3 /\
                   dist (v,x) % e3 = v - x /\
                   ~(v = x)
                   ==> (?psi r1 r2.
                            u - x =
                            (r1 * cos psi) % e1 +
                            (r1 * sin psi) % e2 +
                            h1 % (v - x) /\
                            x' - x =
                            (r2 * cos (psi + theta)) % e1 +
                            (r2 * sin (psi + theta)) % e2 +
                            h2 % (v - x) /\
                            (~collinear {x, v, u} ==> &0 < r1) /\
                            (~collinear {x, v, x'} ==> &0 < r2)))) =
 x''$2`

I use CONV_TAC SELECT_CONV but this is incorrect

I think that

function @ is function choose but is not uniquely
is this true?
thank you
Hoang Le Truong

| I think that
|
| function @ is function choose but is not uniquely
| is this true?

That's correct: in general the meaning of `@x. P x` is just "some x
such that P x". If there is more than one element with property P,
then it's not predictable which one you get. (And if there is *no*
such element at all, you will get some element but it will not of
course satisfy P and you won't be able to prove much else about it.)
However, in cases where there is a unique element, you can use the
theorem SELECT_UNIQUE to prove that `@x. P x` is equal to something
else:

  |- !P x. (!y. P y <=> y = x) ==> (@) P = x

So in your goal, you might want to start with

  MATCH_MP_TAC SELECT_UNIQUE

I really ought to add this uniqueness property for azim as a lemma to
the existing collection of results in Multivariate/flyspeck.ml, since
it seems generally useful.

John.