what is Case.Aux in shapeless

I am confused about the example shown in the shapeless feature overview.

object size extends Poly1 {
  implicit def caseInt = at[Int](x => 1)
  implicit def caseString = at[String](_.length)
  implicit def caseTuple[T, U]
    (implicit st : Case.Aux[T, Int], su : Case.Aux[U, Int]) =
      at[(T, U)](t => size(t._1)+size(t._2))
}

scala> size(((23, "foo"), 13))
res7: Int = 5

what is the Case.Aux ?
why is parameterised type is Int not String
if size(((23, "foo", 123), 13)), how to define CaseTuple ?

Many thanks in advance

More explanations about PolyN function you can find here: What is "at" in shapeless (scala)?

1 & 2. So let's rewrite this code to make it more clear:

object size extends Poly1 {
  implicit def caseInt = at[Int](x => 1)
  implicit def caseString = at[String](_.length)
  implicit def caseTuple[T, U]
    (implicit st : Case.Aux[T, Int], su : Case.Aux[U, Int]) =
      at[(T, U)](t => st(t._1) + su(t._2))
}

Case type class provides us applying some poly function to some object with it's type. http://xuwei-k.github.io/shapeless-sxr/shapeless-2.10-2.0.0-M1/shapeless/poly.scala.html#shapeless.PolyDefns;Case

Let's try to make some function:

def sizeF[F, S](t: (F, S)) = size(t)

It is impossible, without type class wich defines how to apply function:

def sizeF[F, S](t: (F, S))
(implicit cse: Case[size.type, (F, S) :: HNil]) = size(t)

Case.Aux[T, U] it is a shortcut for: poly.Case[this.type, T :: HNil]{ type Result = U } T - it is an argument, U - the result type after application.

3. Let's modify function and make avalible application to ((23, "foo", 123), 13), we need to add function to work with triples:

object size extends Poly1 {
  implicit def caseInt = at[Int](x => 1)
  implicit def caseString = at[String](_.length)
  implicit def caseTuple[T, U]
  (implicit st : Case.Aux[T, Int], su : Case.Aux[U, Int]) =
    at[(T, U)](t => size(t._1) + size(t._2))
  implicit def caseTriple[T, U, F]
  (implicit st : Case.Aux[T, Int], su : Case.Aux[U, Int], sf: Case.Aux[F, Int]) =
    at[(T, U, F)](t => size(t._1) + size(t._2) + size(t._3))
}

size(((23, "foo", 123), 13)) //> res0: Int = 6

As expected.