theorem X3DH_session_key_agree.{u_1, u_2, u_3}
  {FType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  FType u_3] {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  FType u_3 GType u_1]
  {SKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (kdfKDF (G × G × G × G) SK : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SKType u_2) {G₀G : GType u_1}
  (ikₐKeyPair F G G₀ ekₐKeyPair F G G₀ ikᵦKeyPair F G G₀ spkᵦKeyPair F G G₀ : KeyPairKeyPair.{u_1, u_2} (F : Type u_1) (G : Type u_2) [Field F] [AddCommGroup G] [Module F G] (G₀ : G) : Type (max u_1 u_2)A key pair: private scalar and public group element satisfying
pub = DH(priv, G₀). The paper defines four key types: identity (IK),
signed prekey (SPK), one-time prekey (OPK), and ephemeral (EK).  FType u_3 GType u_1 G₀G)
  (opkᵦOption (KeyPair F G G₀) : OptionOption.{u} (α : Type u) : Type uOptional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
 (KeyPairKeyPair.{u_1, u_2} (F : Type u_1) (G : Type u_2) [Field F] [AddCommGroup G] [Module F G] (G₀ : G) : Type (max u_1 u_2)A key pair: private scalar and public group element satisfying
pub = DH(priv, G₀). The paper defines four key types: identity (IK),
signed prekey (SPK), one-time prekey (OPK), and ephemeral (EK).  FType u_3 GType u_1 G₀G)) :
  X3DH_SK_AliceX3DH_SK_Alice.{u_1, u_2, u_3} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] {SK : Type u_3}
  (kdf : KDF (G × G × G × G) SK) (ikₐ ekₐ : F) (IKᵦ SPKᵦ : G) (OPKᵦ : Option G) : SKAlice derives the session key SKₐ = KDF(DH1 ‖ DH2 ‖ DH3 ‖ DH4).  kdfKDF (G × G × G × G) SK ikₐKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F ekₐKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F
      ikᵦKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G spkᵦKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G
      (Option.mapOption.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : Option α → Option βApply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.

Examples:
 * `(none : Option Nat).map (· + 1) = none`
 * `(some 3).map (· + 1) = some 4`
 KeyPair.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G opkᵦOption (KeyPair F G G₀)) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    X3DH_SK_BobX3DH_SK_Bob.{u_1, u_2, u_3} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] {SK : Type u_3}
  (kdf : KDF (G × G × G × G) SK) (ikᵦ spkᵦ : F) (opkᵦ : Option F) (IKₐ EKₐ : G) : SKBob derives the session key SKᵦ = KDF(DH1 ‖ DH2 ‖ DH3 ‖ DH4).  kdfKDF (G × G × G × G) SK ikᵦKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F spkᵦKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F
      (Option.mapOption.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : Option α → Option βApply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.

Examples:
 * `(none : Option Nat).map (· + 1) = none`
 * `(some 3).map (· + 1) = some 4`
 KeyPair.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F opkᵦOption (KeyPair F G G₀))
      ikₐKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G ekₐKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G