theorem X3DH_agree.{u_1, u_2} {FType u_1 : Type u_1A 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_1] {GType u_2 : Type u_2A 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_2] [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_1 GType u_2] {G₀G : GType u_2}
  (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_1 GType u_2 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_1 GType u_2 G₀G)) :
  X3DH_AliceX3DH_Alice.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (ikₐ ekₐ : F) (IKᵦ SPKᵦ : G)
  (OPKᵦ : Option G) : G × G × G × GAlice's DH computations. OPKᵦ is optional; when absent, DH4 = 0.  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_BobX3DH_Bob.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (ikᵦ spkᵦ : F)
  (opkᵦ : Option F) (IKₐ EKₐ : G) : G × G × G × GBob's DH computations (mirror of Alice's).  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