-- The orientation-preserving isometries of ℝ³ as the bundled group of
-- pairs (M, t) acting by x ↦ M x + t, with SO3 embedded compatibly
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Geometry.Euclid.Motions
import Geometry.Vectors3
import Algebra.Group.Homomorphism

-- Vector addition.
defgraph addVector (u v : Set) (i ∈ 3) : ℝ := (u(i):R) + (v(i):R)
requires vectorU : u : 3 → ℝ
requires vectorV : v : 3 → ℝ
proof
  have ui := vector.component_real at u, i with vectorU, member
  have vi := vector.component_real at v, i with vectorV, member
  typecheck

instance addVector.vector (u v : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  shows addVector(u, v) : 3 → ℝ
proof
  exact addVector.function with vectorU, vectorV

theorem addVector.entry (u v i : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  requires index : i ∈ 3
  shows addVector(u, v)(i) = (u(i):R) + (v(i):R)
proof
  exact addVector.value with vectorU, vectorV, index

-- Vector addition is associative, has the zero vector as its unit, and
-- cancels against negation.
theorem addVector.assoc (u v w : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  requires vectorW : w : 3 → ℝ
  shows addVector(addVector(u, v), w) = addVector(u, addVector(v, w))
proof
  have inner := addVector.vector with vectorU, vectorV
  have inner2 := addVector.vector with vectorV, vectorW
  have left := addVector.vector with inner, vectorW
  have right := addVector.vector with vectorU, inner2
  apply FunctionBetween.ext with left, right
  intros i hi
  have ui := vector.component_real at u, i with vectorU, hi
  have vi := vector.component_real at v, i with vectorV, hi
  have wi := vector.component_real at w, i with vectorW, hi
  have e1 := addVector.entry at addVector(u, v), w, i with inner, vectorW, hi
  have e2 := addVector.entry at u, v, i with vectorU, vectorV, hi
  have e3 := addVector.entry at u, addVector(v, w), i with vectorU, inner2, hi
  have e4 := addVector.entry at v, w, i with vectorV, vectorW, hi
  rw [e1, e2, e3, e4]
  ring

theorem addVector.comm (u v : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  shows addVector(u, v) = addVector(v, u)
proof
  have left := addVector.vector with vectorU, vectorV
  have right := addVector.vector with vectorV, vectorU
  apply FunctionBetween.ext with left, right
  intros i hi
  have ui := vector.component_real at u, i with vectorU, hi
  have vi := vector.component_real at v, i with vectorV, hi
  have e1 := addVector.entry at u, v, i with vectorU, vectorV, hi
  have e2 := addVector.entry at v, u, i with vectorV, vectorU, hi
  rw [e1, e2]
  ring

theorem addVector.zero (u : Set)
  requires vectorU : u : 3 → ℝ
  shows addVector(u, zeroVector) = u
proof
  have zero := zeroVector.vector
  have sum := addVector.vector with vectorU, zero
  apply FunctionBetween.ext with sum, vectorU
  intros i hi
  have ui := vector.component_real at u, i with vectorU, hi
  have e1 := addVector.entry at u, zeroVector, i with vectorU, zero, hi
  have e2 := zeroVector.entry at i with hi
  rw [e1, e2]
  ring

theorem addVector.zero_left (u : Set)
  requires vectorU : u : 3 → ℝ
  shows addVector(zeroVector, u) = u
proof
  have zero := zeroVector.vector
  have sum := addVector.vector with zero, vectorU
  apply FunctionBetween.ext with sum, vectorU
  intros i hi
  have ui := vector.component_real at u, i with vectorU, hi
  have e1 := addVector.entry at zeroVector, u, i with zero, vectorU, hi
  have e2 := zeroVector.entry at i with hi
  rw [e1, e2]
  ring

theorem addVector.neg (u : Set)
  requires vectorU : u : 3 → ℝ
  shows addVector(u, vectorNeg(u)) = zeroVector
proof
  have zero := zeroVector.vector
  have negated := vectorNeg.vector with vectorU
  have sum := addVector.vector with vectorU, negated
  apply FunctionBetween.ext with sum, zero
  intros i hi
  have ui := vector.component_real at u, i with vectorU, hi
  have e1 := addVector.entry at u, vectorNeg(u), i with vectorU, negated, hi
  have e2 := vectorNeg.entry at u, i with vectorU, hi
  have e3 := zeroVector.entry at i with hi
  rw [e1, e2, e3]
  ring

theorem addVector.neg_left (u : Set)
  requires vectorU : u : 3 → ℝ
  shows addVector(vectorNeg(u), u) = zeroVector
proof
  have zero := zeroVector.vector
  have negated := vectorNeg.vector with vectorU
  have sum := addVector.vector with negated, vectorU
  apply FunctionBetween.ext with sum, zero
  intros i hi
  have ui := vector.component_real at u, i with vectorU, hi
  have e1 := addVector.entry at vectorNeg(u), u, i with negated, vectorU, hi
  have e2 := vectorNeg.entry at u, i with vectorU, hi
  have e3 := zeroVector.entry at i with hi
  rw [e1, e2, e3]
  ring

-- A matrix acts linearly: it respects sums, the zero vector, and negation.
theorem matrixVector.add_vector (M : realRing ^ 3 × 3) (u v : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  shows M · addVector(u, v) = addVector(M · u, M · v)
proof
  have sum := addVector.vector with vectorU, vectorV
  have left := matrixVector.vector at M, addVector(u, v) with *
  have imageU := matrixVector.vector at M, u with *
  have imageV := matrixVector.vector at M, v with *
  have right := addVector.vector with imageU, imageV
  apply FunctionBetween.ext with left, right
  intros i hi
  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi
  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem
  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem
  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem
  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem
  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem
  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem
  have e1 := matrixVector.entry at M, addVector(u, v), i with *
  have e2 := addVector.entry at M · u, M · v, i with imageU, imageV, hi
  have e3 := matrixVector.entry at M, u, i with *
  have e4 := matrixVector.entry at M, v, i with *
  have s0 := addVector.entry at u, v, 0 with vectorU, vectorV, index.zero_mem
  have s1 := addVector.entry at u, v, 1 with vectorU, vectorV, index.one_mem
  have s2 := addVector.entry at u, v, 2 with vectorU, vectorV, index.two_mem
  rw [e1, e2, e3, e4, s0, s1, s2]
  ring

theorem matrixVector.zero_vector (M : realRing ^ 3 × 3)
  shows M · zeroVector = zeroVector
proof
  have zero := zeroVector.vector
  have left := matrixVector.vector at M, zeroVector with *
  apply FunctionBetween.ext with left, zero
  intros i hi
  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi
  have e1 := matrixVector.entry at M, zeroVector, i with *
  have z0 := zeroVector.entry at 0 with index.zero_mem
  have z1 := zeroVector.entry at 1 with index.one_mem
  have z2 := zeroVector.entry at 2 with index.two_mem
  have zi := zeroVector.entry at i with hi
  rw [e1, z0, z1, z2, zi]
  ring

-- The product in SO3 is the matrix product.
theorem SO3.product_value (M N : realRing ^ 3 × 3)
  requires hM : M ∈ so3Matrices
  requires hN : N ∈ so3Matrices
  shows call2(Group.mul(SO3), M, N) = M * N
proof
  have ring := matrixRing.real_ring
  have magma := IsSemigroup.magma with
    (IsMonoid.semigroup with (IsRing.multiplicative with (Ring.parts
        with ring)))
  have closedMul : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))
    intros A hA B hB
    have matrixA := so3Matrices.matrix with hA
    have matrixB := so3Matrices.matrix with hB
    exact so3Matrices.mul_mem with *
  have operation := restrictBinary.value at Ring.carrier(matrixRing(realRing,
      3)),
    so3Matrices, Ring.mul(matrixRing(realRing, 3)), M, N
    with magma, so3Matrices.subset, closedMul, hM, hN
  rw SO3.mulOf
  exact operation

-- The motions: a rotation paired with a translation vector.
def motions : Set := so3Matrices × ℝ³

theorem motions.pair (M t : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  shows (M, t) ∈ motions
proof
  unfold motions
  exact product.pair with hM, ht

theorem motions.cases (p : Set)
  requires hp : p ∈ motions
  shows ∃ M ∈ so3Matrices, ∃ t ∈ ℝ³, p = (M, t)
proof
  unfold motions at hp
  obtain ⟨bound, M, hM, t, ht, shape⟩ := product.membership.forward with hp
  exact ⟨M, hM, t, ht, shape⟩

-- The product (M, t) · (N, s) = (M N, M s + t), the unit (1, 0), and the
-- inverse (Mᵀ, −Mᵀ t).
defgraph motionMul (q ∈ motions × motions) : motions :=
  (call2(Ring.mul(matrixRing(realRing, 3)), fst(fst(q)), fst(snd(q))),
    addVector(fst(fst(q)) · snd(snd(q)), snd(fst(q))))
proof
  obtain ⟨bound, p, hp, r, hr, shape⟩ :=
    product.membership.forward with member
  obtain ⟨M, hM, t, ht, pShape⟩ := motions.cases with hp
  obtain ⟨N, hN, s, hs, rShape⟩ := motions.cases with hr
  have matrixM := so3Matrices.matrix with hM
  have matrixN := so3Matrices.matrix with hN
  have productIn := so3Matrices.mul_mem with hM, hN
  have vectorT := ℝ³.function with ht
  have vectorS := ℝ³.function with hs
  have image := matrixVector.vector at M, s with *
  have sum := addVector.vector with image, vectorT
  have sumIn := ℝ³.of_function with sum
  have outerFirst := fst.pair at (M, t), (N, s)
  have outerSecond := snd.pair at (M, t), (N, s)
  have firstP := fst.pair at M, t
  have secondP := snd.pair at M, t
  have firstR := fst.pair at N, s
  have secondR := snd.pair at N, s
  rw [shape, pShape, rShape, outerFirst, outerSecond, firstP, secondP, firstR,
      secondR]
  exact motions.pair with productIn, sumIn

def motionOne : Set := (matrixRing(realRing, 3)[1], zeroVector)

theorem motionOne.graph
  shows motionOne = (matrixRing(realRing, 3)[1], zeroVector)
proof
  simp [motionOne]

theorem motionOne.member
  shows motionOne ∈ motions
proof
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector
  rw motionOne.graph
  exact motions.pair with so3Matrices.one_mem, zeroIn

defgraph motionInv (p ∈ motions) : motions :=
  (transpose(fst(p)), vectorNeg(transpose(fst(p)) · snd(p)))
proof
  obtain ⟨M, hM, t, ht, shape⟩ := motions.cases with member
  have matrixM := so3Matrices.matrix with hM
  have transposedIn := so3Matrices.transpose_mem with hM
  have transposed := transpose.matrix at M with *
  have vectorT := ℝ³.function with ht
  have image := matrixVector.vector at transpose(M), t with *
  have negated := vectorNeg.vector with image
  have negIn := ℝ³.of_function with negated
  have firstP := fst.pair at M, t
  have secondP := snd.pair at M, t
  rw [shape, firstP, secondP]
  exact motions.pair with transposedIn, negIn

theorem motionMul.apply (M N : realRing ^ 3 × 3) (t s : Set)
  requires hM : M ∈ so3Matrices
  requires hN : N ∈ so3Matrices
  requires ht : t ∈ ℝ³
  requires hs : s ∈ ℝ³
  shows motionMul((M, t), (N, s)) = (M * N, addVector(M · s, t))
proof
  have first := motions.pair with hM, ht
  have second := motions.pair with hN, hs
  have pair :=
      product.pair at (M, t), (N, s), motions, motions with first, second
  have value := motionMul.value at ((M, t), (N, s)) with pair
  have outerFirst := fst.pair at (M, t), (N, s)
  have outerSecond := snd.pair at (M, t), (N, s)
  have firstP := fst.pair at M, t
  have secondP := snd.pair at M, t
  have firstR := fst.pair at N, s
  have secondR := snd.pair at N, s
  simp [call2]

theorem motionInv.apply (M : realRing ^ 3 × 3) (t : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  shows motionInv((M, t)) = (transpose(M), vectorNeg(transpose(M) · t))
proof
  have pair := motions.pair with hM, ht
  have value := motionInv.value at (M, t) with pair
  have firstP := fst.pair at M, t
  have secondP := snd.pair at M, t
  rw [value, firstP, secondP]
  rfl

-- The group laws of the product on explicit pairs.
theorem motionMul.assoc (M N P : realRing ^ 3 × 3) (t s r : Set)
  requires hM : M ∈ so3Matrices
  requires hN : N ∈ so3Matrices
  requires hP : P ∈ so3Matrices
  requires ht : t ∈ ℝ³
  requires hs : s ∈ ℝ³
  requires hr : r ∈ ℝ³
  shows motionMul(motionMul((M, t), (N, s)), (P, r)) =
    motionMul((M, t), motionMul((N, s), (P, r)))
proof
  have productMN := so3Matrices.mul_mem with hM, hN
  have productNP := so3Matrices.mul_mem with hN, hP
  have vectorT := ℝ³.function with ht
  have vectorS := ℝ³.function with hs
  have vectorR := ℝ³.function with hr
  have imageS := matrixVector.vector at M, s with *
  have imageR := matrixVector.vector at N, r with *
  have sumMS : addVector(M · s, t) ∈ ℝ³ :=
    ℝ³.of_function with (addVector.vector with imageS, vectorT)
  have sumNR : addVector(N · r, s) ∈ ℝ³ :=
    ℝ³.of_function with (addVector.vector with imageR, vectorS)
  have first := motionMul.apply with hM, hN, ht, hs
  have second := motionMul.apply at M * N, P, addVector(M · s, t), r with
    productMN, hP, sumMS, hr
  have third := motionMul.apply with hN, hP, hs, hr
  have fourth := motionMul.apply at M, N * P, t, addVector(N · r, s) with
    hM, productNP, ht, sumNR
  have assocMatrix := matrixRing.mul_assoc at M, N, P with *
  have composed := matrixVector.mul at M, N, r with vectorR
  have linear := matrixVector.add_vector at M, N · r, s with imageR, vectorS
  have imageNR := matrixVector.vector at M, N · r with *
  have assocVector := addVector.assoc at M · (N · r), M · s, t with
    imageNR, imageS, vectorT
  rw [first, second, third, fourth, assocMatrix, composed, linear, assocVector]
  rfl

theorem motionMul.one_left (M : realRing ^ 3 × 3) (t : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  shows motionMul(motionOne, (M, t)) = (M, t)
proof
  have one := Matrix.one_matrix
  have oneIn := so3Matrices.one_mem
  have zero := zeroVector.vector
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zero
  have vectorT := ℝ³.function with ht
  have value := motionMul.apply at matrixRing(realRing, 3)[1], M, zeroVector,
      t with
    oneIn, hM, zeroIn, ht
  have unitMul := matrixRing.one_mul at M with *
  have unitAct := matrixVector.one at t with vectorT
  have unitAdd := addVector.zero at t with vectorT
  rw [motionOne.graph, value, unitMul, unitAct, unitAdd]
  rfl

theorem motionMul.one_right (M : realRing ^ 3 × 3) (t : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  shows motionMul((M, t), motionOne) = (M, t)
proof
  have one := Matrix.one_matrix
  have oneIn := so3Matrices.one_mem
  have zero := zeroVector.vector
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zero
  have vectorT := ℝ³.function with ht
  have value := motionMul.apply at M, matrixRing(realRing, 3)[1], t,
      zeroVector with
    hM, oneIn, ht, zeroIn
  have unitMul := matrixRing.mul_one at M with *
  have killed := matrixVector.zero_vector at M with *
  have unitAdd := addVector.zero_left at t with vectorT
  rw [motionOne.graph, value, unitMul, killed, unitAdd]
  rfl

theorem motionMul.inv_left (M : realRing ^ 3 × 3) (t : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  shows motionMul(motionInv((M, t)), (M, t)) = motionOne
proof
  have transposedIn := so3Matrices.transpose_mem with hM
  have transposed := transpose.matrix at M with *
  have vectorT := ℝ³.function with ht
  have imageT := matrixVector.vector at transpose(M), t with *
  have negated := vectorNeg.vector with imageT
  have negIn : vectorNeg(transpose(M) · t) ∈ ℝ³ :=
    ℝ³.of_function with negated
  have invValue := motionInv.apply with hM, ht
  have value := motionMul.apply at transpose(M), M,
      vectorNeg(transpose(M) · t), t with
    transposedIn, hM, negIn, ht
  have orthogonal := Orthogonal.left with (so3Matrices.orthogonal with hM)
  have cancel := addVector.neg at transpose(M) · t with imageT
  rw [invValue, value, orthogonal, cancel, motionOne.graph]
  rfl

theorem motionMul.inv_right (M : realRing ^ 3 × 3) (t : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  shows motionMul((M, t), motionInv((M, t))) = motionOne
proof
  have transposedIn := so3Matrices.transpose_mem with hM
  have transposed := transpose.matrix at M with *
  have vectorT := ℝ³.function with ht
  have imageT := matrixVector.vector at transpose(M), t with *
  have negated := vectorNeg.vector with imageT
  have negIn : vectorNeg(transpose(M) · t) ∈ ℝ³ :=
    ℝ³.of_function with negated
  have invValue := motionInv.apply with hM, ht
  have value := motionMul.apply at M, transpose(M), t,
      vectorNeg(transpose(M) · t) with
    hM, transposedIn, ht, negIn
  have orthogonal := Orthogonal.right with (so3Matrices.orthogonal with hM)
  have negLaw := matrixVector.neg at M, transpose(M) · t with imageT
  have composed := matrixVector.mul at M, transpose(M), t with vectorT
  have unitAct := matrixVector.one at t with vectorT
  have cancel := addVector.neg_left at t with vectorT
  rw [invValue, value, negLaw, ← composed, orthogonal, unitAct, cancel,
      motionOne.graph]
  rfl

-- The group of motions.
def Motions : Set := Group.mk(motions, motionMul, motionOne, motionInv)

theorem Motions.carrierOf
  shows Group.carrier(Motions) = motions
proof
  simp [Motions, Group.mk.carrier]

theorem Motions.mulOf
  shows Group.mul(Motions) = motionMul
proof
  simp [Motions, Group.mk.mul]

theorem Motions.oneOf
  shows Group.one(Motions) = motionOne
proof
  simp [Motions, Group.mk.one]

theorem Motions.invOf
  shows Group.inv(Motions) = motionInv
proof
  simp [Motions, Group.mk.inv]

theorem Motions.engine
  shows IsGroup(motions, motionMul, motionOne, motionInv)
proof
  have magma : IsMagma(motions, motionMul)
    unfold IsMagma
    exact motionMul.function
  have associative : Associative(motions, motionMul)
    unfold Associative
    intros x hx y hy z hz
    obtain ⟨M, hM, t, ht, xShape⟩ := motions.cases with hx
    obtain ⟨N, hN, s, hs, yShape⟩ := motions.cases with hy
    obtain ⟨P, hP, r, hr, zShape⟩ := motions.cases with hz
    have matrixM := so3Matrices.matrix with hM
    have matrixN := so3Matrices.matrix with hN
    have matrixP := so3Matrices.matrix with hP
    rw [xShape, yShape, zShape]
    exact motionMul.assoc with *
  have identity : Identity(motions, motionMul, motionOne)
    unfold Identity
    constructor
    . exact motionOne.member
    . intros x hx
      obtain ⟨M, hM, t, ht, xShape⟩ := motions.cases with hx
      have matrixM := so3Matrices.matrix with hM
      rw xShape
      constructor
      . exact motionMul.one_left with *
      . exact motionMul.one_right with *
  have inverse : Inverse(motions, motionMul, motionOne, motionInv)
    unfold Inverse
    constructor
    . exact motionInv.function
    . intros x hx
      obtain ⟨M, hM, t, ht, xShape⟩ := motions.cases with hx
      have matrixM := so3Matrices.matrix with hM
      rw xShape
      constructor
      . exact motionMul.inv_left with *
      . exact motionMul.inv_right with *
  unfold IsGroup
  exact ⟨⟨⟨magma, associative⟩, identity⟩, inverse⟩

instance Motions.group
  shows Group(Motions)
proof
  have engine := Motions.engine
  unfold Motions
  exact Group.of_parts with engine

-- The action of the motions on ℝ³: (M, t) sends x to M x + t.
defgraph motionAction (q ∈ motions × ℝ³) : ℝ³ :=
  addVector(fst(fst(q)) · snd(q), snd(fst(q)))
proof
  obtain ⟨bound, p, hp, x, hx, shape⟩ :=
    product.membership.forward with member
  obtain ⟨M, hM, t, ht, pShape⟩ := motions.cases with hp
  have matrixM := so3Matrices.matrix with hM
  have vectorT := ℝ³.function with ht
  have vectorX := ℝ³.function with hx
  have image := matrixVector.vector at M, x with *
  have sum := addVector.vector with image, vectorT
  have outerFirst := fst.pair at (M, t), x
  have outerSecond := snd.pair at (M, t), x
  have firstP := fst.pair at M, t
  have secondP := snd.pair at M, t
  rw [shape, pShape, outerFirst, outerSecond, firstP, secondP]
  exact ℝ³.of_function with sum

theorem motionAction.apply (M : realRing ^ 3 × 3) (t x : Set)
  requires hM : M ∈ so3Matrices
  requires ht : t ∈ ℝ³
  requires hx : x ∈ ℝ³
  shows motionAction((M, t), x) = addVector(M · x, t)
proof
  have first := motions.pair with hM, ht
  have pair := product.pair at (M, t), x, motions, ℝ³ with first, hx
  have value := motionAction.value at ((M, t), x) with pair
  have outerFirst := fst.pair at (M, t), x
  have outerSecond := snd.pair at (M, t), x
  have firstP := fst.pair at M, t
  have secondP := snd.pair at M, t
  simp [call2]

theorem motionAction.action
  shows motionAction : Motions ↷ ℝ³
proof
  have group := Motions.group
  have function := motionAction.function
  rw ← Motions.carrierOf at function
  apply Action.mk with group, function
  . intros x hx
    have vectorX := ℝ³.function with hx
    have one := Matrix.one_matrix
    have oneIn := so3Matrices.one_mem
    have zeroIn : zeroVector ∈ ℝ³ :=
      ℝ³.of_function with zeroVector.vector
    have value := motionAction.apply at matrixRing(realRing, 3)[1],
        zeroVector, x with
      oneIn, zeroIn, hx
    have unitAct := matrixVector.one at x with vectorX
    have unitAdd := addVector.zero at x with vectorX
    rw [Motions.oneOf, motionOne.graph, value, unitAct, unitAdd]
    rfl
  . intros g hg h hh x hx
    rw Motions.carrierOf at hg
    rw Motions.carrierOf at hh
    obtain ⟨M, hM, t, ht, gShape⟩ := motions.cases with hg
    obtain ⟨N, hN, s, hs, hShape⟩ := motions.cases with hh
    have matrixM := so3Matrices.matrix with hM
    have matrixN := so3Matrices.matrix with hN
    have vectorT := ℝ³.function with ht
    have vectorS := ℝ³.function with hs
    have vectorX := ℝ³.function with hx
    have productIn := so3Matrices.mul_mem with hM, hN
    have imageS := matrixVector.vector at M, s with *
    have sumIn : addVector(M · s, t) ∈ ℝ³ :=
      ℝ³.of_function with (addVector.vector with imageS, vectorT)
    have imageX := matrixVector.vector at N, x with *
    have innerIn : addVector(N · x, s) ∈ ℝ³ :=
      ℝ³.of_function with (addVector.vector with imageX, vectorS)
    have product := motionMul.apply with hM, hN, ht, hs
    have outer := motionAction.apply at M * N, addVector(M · s, t), x with
      productIn, sumIn, hx
    have inner := motionAction.apply at N, s, x with hN, hs, hx
    have composed :=
        motionAction.apply at M, t, addVector(N · x, s) with hM, ht, innerIn
    have assocMatrix := matrixVector.mul at M, N, x with vectorX
    have linear := matrixVector.add_vector at M, N · x, s with imageX, vectorS
    have imageNX := matrixVector.vector at M, N · x with *
    have assocVector := addVector.assoc at M · (N · x), M · s, t with
      imageNX, imageS, vectorT
    rw [gShape, hShape, Motions.mulOf, product, outer, inner, composed,
      assocMatrix, linear, assocVector]
    rfl

-- The rotations as the motions fixing the origin.
defgraph rotationMotion (M ∈ so3Matrices) : motions := (M, zeroVector)
proof
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector
  exact motions.pair with member, zeroIn

theorem rotationMotion.apply (M : Set)
  requires hM : M ∈ so3Matrices
  shows rotationMotion(M) = (M, zeroVector)
proof
  exact rotationMotion.value with hM

theorem rotationMotion.hom
  shows rotationMotion : SO3 →* Motions
proof
  have source := SO3.group
  have target := Motions.group
  have function := rotationMotion.function
  rw [← SO3.carrierOf, ← Motions.carrierOf] at function
  apply GroupHom.mk with source, target, function
  intros M hM N hN
  rw SO3.carrierOf at hM
  rw SO3.carrierOf at hN
  have matrixM := so3Matrices.matrix with hM
  have matrixN := so3Matrices.matrix with hN
  have productIn := so3Matrices.mul_mem with hM, hN
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector
  have operation := SO3.product_value with hM, hN
  have imageM := rotationMotion.apply with hM
  have imageN := rotationMotion.apply with hN
  have imageMN := rotationMotion.apply with productIn
  have product := motionMul.apply at M, N, zeroVector, zeroVector with hM, hN,
      zeroIn, zeroIn
  have killed := matrixVector.zero_vector at M with *
  have unitAdd := addVector.zero at zeroVector with zeroVector.vector
  rw [operation, imageMN, imageM, imageN, Motions.mulOf, product, killed,
      unitAdd]
  rfl

-- A rotation acts on ℝ³ as its motion does.
theorem rotationMotion.compatible
  shows ∀ M ∈ Group.carrier(SO3), ∀ x ∈ ℝ³,
    spaceAction(M, x) = motionAction(rotationMotion(M), x)
proof
  intros M hM x hx
  rw SO3.carrierOf at hM
  have matrixM := so3Matrices.matrix with hM
  have vectorX := ℝ³.function with hx
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector
  have image := rotationMotion.apply with hM
  have space := spaceAction.apply with hM, hx
  have motion := motionAction.apply at M, zeroVector, x with hM, zeroIn, hx
  have imageX := matrixVector.vector at M, x with *
  have unitAdd := addVector.zero at M · x with imageX
  rw [image, space, motion, unitAdd]
  rfl