-- A rotation other than the identity fixes at most two points of the
-- sphere, a point and its antipode
-- 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.Hausdorff.FixedPoints
import Geometry.Vectors3
import Geometry.Absorption.Turn
import Rotation.Freeness

-- Three real squares summing to zero all vanish.
theorem sumSquares.eq_zero (a b c : Real)
  requires zero : a * a + b * b + c * c = 0
  shows a = 0 ∧ b = 0 ∧ c = 0
proof
  have squareA := realMulValue.square_nonnegative at a
  have squareB := realMulValue.square_nonnegative at b
  have squareC := realMulValue.square_nonnegative at c
  have zeroA : a * a = 0 by linarith
  have zeroB : b * b = 0 by linarith
  have zeroC : c * c = 0 by linarith
  have criterionA := realMulValue.square_eq_zero_iff at a
  have criterionB := realMulValue.square_eq_zero_iff at b
  have criterionC := realMulValue.square_eq_zero_iff at c
  exact ⟨criterionA.forward with zeroA, criterionB.forward with zeroB,
    criterionC.forward with zeroC⟩

-- Two unit vectors that are neither equal nor opposite have a nonzero
-- cross product, by Lagrange's identity.
theorem cross.nonzero (u v : Set)
  requires memberU : u ∈ S²
  requires memberV : v ∈ S²
  requires distinct : v ≠ u
  requires opposite : v ≠ vectorNeg(u)
  shows normSq(cross(u, v)) ≠ (0:R)
proof
  obtain ⟨spaceU, unitU⟩ := S².membership.forward with memberU
  obtain ⟨spaceV, unitV⟩ := S².membership.forward with memberV
  have vectorU := ℝ³.function with spaceU
  have vectorV := ℝ³.function with spaceV
  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 dotReal := dot3.real with vectorU, vectorV
  have lagrange := cross.normSq with vectorU, vectorV
  have dotValue := dot3.value at u, v
  rw [unitU, unitV] at lagrange
  rw normSq.value at unitU
  rw normSq.value at unitV
  intro zero
  rw zero at lagrange
  symm at lagrange
  have product : ((1:R) - dot3(u, v)) * ((1:R) + dot3(u, v)) =
      (0:R) * ((1:R) + dot3(u, v))
    linear_combination lagrange
  have split : (1:R) + dot3(u, v) = 0 ∨ (1:R) + dot3(u, v) ≠ 0 by tauto
  cases split with antipodal | generic
  . have sumZero : ((u(0):R) + (v(0):R)) * ((u(0):R) + (v(0):R)) +
        ((u(1):R) + (v(1):R)) * ((u(1):R) + (v(1):R)) +
        ((u(2):R) + (v(2):R)) * ((u(2):R) + (v(2):R)) = 0
      linear_combination unitU + unitV - dotValue - dotValue + antipodal +
        antipodal
    obtain ⟨z0, z1, z2⟩ := sumSquares.eq_zero at (u(0):R) + (v(0):R),
      (u(1):R) + (v(1):R), (u(2):R) + (v(2):R) with sumZero
    apply opposite
    have negated := vectorNeg.vector with vectorU
    apply FunctionBetween.ext with vectorV, negated
    intros i hi
    have entry := vectorNeg.entry at u, i with vectorU, hi
    rw entry
    have alternatives := index.cases with hi
    rcases alternatives with at0 | at1 | at2
    . rw at0
      linarith
    . rw at1
      linarith
    . rw at2
      linarith
  . have cancel := realMulValue.right_cancel_of_nonzero at (1:R) - dot3(u, v),
      (0:R), (1:R) + dot3(u, v) with generic, product
    have sumZero : ((u(0):R) - (v(0):R)) * ((u(0):R) - (v(0):R)) +
        ((u(1):R) - (v(1):R)) * ((u(1):R) - (v(1):R)) +
        ((u(2):R) - (v(2):R)) * ((u(2):R) - (v(2):R)) = 0
      linear_combination unitU + unitV + dotValue + dotValue + cancel + cancel
    obtain ⟨z0, z1, z2⟩ := sumSquares.eq_zero at (u(0):R) - (v(0):R),
      (u(1):R) - (v(1):R), (u(2):R) - (v(2):R) with sumZero
    apply distinct
    apply FunctionBetween.ext with vectorV, vectorU
    intros i hi
    have alternatives := index.cases with hi
    rcases alternatives with at0 | at1 | at2
    . rw at0
      linarith
    . rw at1
      linarith
    . rw at2
      linarith

-- The three components of a vector are real.
theorem vector.components (x : Set)
  requires vector : x : 3 → ℝ
  shows x(0) ∈ ℝ ∧ x(1) ∈ ℝ ∧ x(2) ∈ ℝ
proof
  have x0 := vector.component_real at x, 0 with vector, index.zero_mem
  have x1 := vector.component_real at x, 1 with vector, index.one_mem
  have x2 := vector.component_real at x, 2 with vector, index.two_mem
  exact ⟨x0, x1, x2⟩

-- The components of any vector r against the frame u, v, u × v: the
-- squared norm of u × v times r(k) is a combination of the dot products
-- of r with u, v, and u × v.
theorem cross.expand (u v r k : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  requires vectorR : r : 3 → ℝ
  requires index : k ∈ 3
  shows normSq(cross(u, v)) * (r(k):R) =
    dot3(r, u) * (normSq(v) * (u(k):R) - dot3(u, v) * (v(k):R)) +
    dot3(r, v) * (normSq(u) * (v(k):R) - dot3(u, v) * (u(k):R)) +
    dot3(r, cross(u, v)) * (cross(u, v)(k):R)
proof
  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 r0 := vector.component_real at r, 0 with vectorR, index.zero_mem
  have r1 := vector.component_real at r, 1 with vectorR, index.one_mem
  have r2 := vector.component_real at r, 2 with vectorR, index.two_mem
  have c0 := cross.zero with vectorU, vectorV
  have c1 := cross.one with vectorU, vectorV
  have c2 := cross.two with vectorU, vectorV
  have alternatives := index.cases with index
  rcases alternatives with at0 | at1 | at2
  . rw [at0, normSq.value, normSq.value, normSq.value, dot3.value, dot3.value,
      dot3.value, dot3.value, c0, c1, c2]
    ring
  . rw [at1, normSq.value, normSq.value, normSq.value, dot3.value, dot3.value,
      dot3.value, dot3.value, c0, c1, c2]
    ring
  . rw [at2, normSq.value, normSq.value, normSq.value, dot3.value, dot3.value,
      dot3.value, dot3.value, c0, c1, c2]
    ring

-- A vector orthogonal to u, v, and u × v is zero when u × v is not.
theorem cross.orthogonal_zero (u v r : Set)
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  requires vectorR : r : 3 → ℝ
  requires nonzero : normSq(cross(u, v)) ≠ (0:R)
  requires first : dot3(r, u) = (0:R)
  requires second : dot3(r, v) = (0:R)
  requires third : dot3(r, cross(u, v)) = (0:R)
  shows r = zeroVector
proof
  have zero := zeroVector.vector
  have wVector := cross.vector with vectorU, vectorV
  have normReal := normSq.real with wVector
  apply FunctionBetween.ext with vectorR, zero
  intros k hk
  have expand := cross.expand at u, v, r, k with vectorU, vectorV, vectorR, hk
  have component := vector.component_real at r, k with vectorR, hk
  have uk := vector.component_real at u, k with vectorU, hk
  have vk := vector.component_real at v, k with vectorV, hk
  have wk := vector.component_real at cross(u, v), k with wVector, hk
  obtain ⟨u0, u1, u2⟩ := vector.components with vectorU
  obtain ⟨v0, v1, v2⟩ := vector.components with vectorV
  obtain ⟨w0, w1, w2⟩ := vector.components with wVector
  rw [first, second, third] at expand
  have same : (r(k):R) * normSq(cross(u, v)) = (0:R) * normSq(cross(u, v))
    linear_combination expand
  have vanishes := realMulValue.right_cancel_of_nonzero at (r(k):R), (0:R),
    normSq(cross(u, v)) with nonzero, same
  rw zeroVector.entry
  exact vanishes

-- The dot product with a basis vector picks a component.
theorem basis.dot (x i : Set)
  requires vector : x : 3 → ℝ
  requires index : i ∈ 3
  shows (basis(i)(0):R) * (x(0):R) + (basis(i)(1):R) * (x(1):R) +
    (basis(i)(2):R) * (x(2):R) = (x(i):R)
proof
  have x0 := vector.component_real at x, 0 with vector, index.zero_mem
  have x1 := vector.component_real at x, 1 with vector, index.one_mem
  have x2 := vector.component_real at x, 2 with vector, index.two_mem
  have alternatives := index.cases with index
  rcases alternatives with at0 | at1 | at2
  . have same := basis.same at 0 with index.zero_mem
    have other1 := basis.other at 1, 0
      with index.one_mem, index.zero_mem, index.one_ne_zero
    have other2 := basis.other at 2, 0
      with index.two_mem, index.zero_mem, index.two_ne_zero
    rw [at0, same, other1, other2]
    ring
  . have same := basis.same at 1 with index.one_mem
    have other0 := basis.other at 0, 1
      with index.zero_mem, index.one_mem, index.zero_ne_one
    have other2 := basis.other at 2, 1
      with index.two_mem, index.one_mem, index.two_ne_one
    rw [at1, same, other0, other2]
    ring
  . have same := basis.same at 2 with index.two_mem
    have other0 := basis.other at 0, 2
      with index.zero_mem, index.two_mem, index.zero_ne_two
    have other1 := basis.other at 1, 2
      with index.one_mem, index.two_mem, index.one_ne_two
    rw [at2, same, other0, other1]
    ring

-- Row i of M − 1, as a vector.
defgraph rowShift (M i : Set) (k ∈ 3) : ℝ := (M[i, k]:R) - (basis(i)(k):R)
requires matrix : M : realRing ^ 3 × 3
requires row : i ∈ 3
proof
  have entry := Matrix.real_entry at M, i, k with matrix, row, member
  have basisVector := basis.vector with row
  have component := vector.component_real at basis(i), k
    with basisVector, member
  typecheck

instance rowShift.vector (M i : Set)
  requires matrix : M : realRing ^ 3 × 3
  requires row : i ∈ 3
  shows rowShift(M, i) : 3 → ℝ
proof
  exact rowShift.function with matrix, row

theorem rowShift.entry (M i k : Set)
  requires matrix : M : realRing ^ 3 × 3
  requires row : i ∈ 3
  requires column : k ∈ 3
  shows rowShift(M, i)(k) = (M[i, k]:R) - (basis(i)(k):R)
proof
  exact rowShift.value with matrix, row, column

-- A row of M − 1 is orthogonal to every vector fixed by M.
theorem rowShift.dot (M i x : Set)
  requires matrix : M : realRing ^ 3 × 3
  requires row : i ∈ 3
  requires vector : x : 3 → ℝ
  requires fixed : M · x = x
  shows dot3(rowShift(M, i), x) = (0:R)
proof
  have entry := matrixVector.entry at M, x, i with matrix, vector, row
  rw fixed at entry
  have basisDot := basis.dot with vector, row
  have basisVector := basis.vector with row
  have b0 := vector.component_real at basis(i), 0
    with basisVector, index.zero_mem
  have b1 := vector.component_real at basis(i), 1
    with basisVector, index.one_mem
  have b2 := vector.component_real at basis(i), 2
    with basisVector, index.two_mem
  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with row
  have x0 := vector.component_real at x, 0 with vector, index.zero_mem
  have x1 := vector.component_real at x, 1 with vector, index.one_mem
  have x2 := vector.component_real at x, 2 with vector, index.two_mem
  have xi := vector.component_real at x, i with vector, row
  have r0 := rowShift.entry at M, i, 0 with matrix, row, index.zero_mem
  have r1 := rowShift.entry at M, i, 1 with matrix, row, index.one_mem
  have r2 := rowShift.entry at M, i, 2 with matrix, row, index.two_mem
  rw [dot3.value, r0, r1, r2]
  symm at entry
  linear_combination entry - basisDot

-- The drift of row i: the component of row i of M − 1 along u × v.
def drift (M u v i : Set) : Set := dot3(rowShift(M, i), cross(u, v))

theorem drift.value (M u v i : Set)
  shows drift(M, u, v, i) = dot3(rowShift(M, i), cross(u, v))
proof
  simp [drift]

instance drift.real (M u v i : Set)
  requires matrix : M : realRing ^ 3 × 3
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  requires row : i ∈ 3
  shows drift(M, u, v, i) ∈ ℝ
proof
  have shift := rowShift.vector with matrix, row
  have wVector := cross.vector with vectorU, vectorV
  rw drift.value
  exact dot3.real with shift, wVector

-- When M fixes u and v, the entries of M are those of the identity plus
-- the drift of the row times u × v, up to the factor |u × v|².
theorem fixed.entry (M u v i k : Set)
  requires matrix : M : realRing ^ 3 × 3
  requires vectorU : u : 3 → ℝ
  requires vectorV : v : 3 → ℝ
  requires fixedU : M · u = u
  requires fixedV : M · v = v
  requires row : i ∈ 3
  requires column : k ∈ 3
  shows normSq(cross(u, v)) * (M[i, k]:R) =
    normSq(cross(u, v)) * (basis(i)(k):R) +
    drift(M, u, v, i) * (cross(u, v)(k):R)
proof
  have shift := rowShift.vector with matrix, row
  have expand := cross.expand at u, v, rowShift(M, i), k
    with vectorU, vectorV, shift, column
  have first := rowShift.dot with matrix, row, vectorU, fixedU
  have second := rowShift.dot with matrix, row, vectorV, fixedV
  have entry := rowShift.entry at M, i, k with matrix, row, column
  have wVector := cross.vector with vectorU, vectorV
  have uk := vector.component_real at u, k with vectorU, column
  have vk := vector.component_real at v, k with vectorV, column
  have wk := vector.component_real at cross(u, v), k with wVector, column
  obtain ⟨u0, u1, u2⟩ := vector.components with vectorU
  obtain ⟨v0, v1, v2⟩ := vector.components with vectorV
  obtain ⟨w0, w1, w2⟩ := vector.components with wVector
  obtain ⟨s0, s1, s2⟩ := vector.components with shift
  have mik := Matrix.real_entry at M, i, k with matrix, row, column
  have basisVector := basis.vector with row
  have bik := vector.component_real at basis(i), k
    with basisVector, column
  rw [first, second, entry] at expand
  rw drift.value
  linear_combination expand

-- A rotation fixing two unit vectors that are neither equal nor opposite
-- is the identity.
theorem so3.fixed_pair (M u v : Set)
  requires member : M ∈ so3Matrices
  requires memberU : u ∈ S²
  requires memberV : v ∈ S²
  requires fixedU : M · u = u
  requires fixedV : M · v = v
  requires distinct : v ≠ u
  requires opposite : v ≠ vectorNeg(u)
  shows M = Ring.one(matrixRing(realRing, 3))
proof
  have comm := realRing.comm_ring
  have matrix := so3Matrices.matrix with member
  have orthogonal := so3Matrices.orthogonal with member
  have unit := so3Matrices.determinant with member
  have one := Matrix.one_matrix
  have nonzero := cross.nonzero with memberU, memberV, distinct, opposite
  have vectorU := S².function with memberU
  have vectorV := S².function with memberV
  have wVector := cross.vector with vectorU, vectorV
  have normReal := normSq.real with wVector
  have normValue := normSq.value at cross(u, v)
  obtain ⟨w0, w1, w2⟩ := vector.components with wVector
  obtain ⟨u0, u1, u2⟩ := vector.components with vectorU
  obtain ⟨v0, v1, v2⟩ := vector.components with vectorV
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ :=
    Matrix.entries_real with matrix
  have shift0 := rowShift.vector at M, 0 with matrix, index.zero_mem
  have shift1 := rowShift.vector at M, 1 with matrix, index.one_mem
  have shift2 := rowShift.vector at M, 2 with matrix, index.two_mem
  obtain ⟨s00, s01, s02⟩ := vector.components with shift0
  obtain ⟨s10, s11, s12⟩ := vector.components with shift1
  obtain ⟨s20, s21, s22⟩ := vector.components with shift2
  have d0 := drift.real at M, u, v, 0
    with matrix, vectorU, vectorV, index.zero_mem
  have d1 := drift.real at M, u, v, 1
    with matrix, vectorU, vectorV, index.one_mem
  have d2 := drift.real at M, u, v, 2
    with matrix, vectorU, vectorV, index.two_mem
  have b00 := basis.same at 0 with index.zero_mem
  have b11 := basis.same at 1 with index.one_mem
  have b22 := basis.same at 2 with index.two_mem
  have b01 := basis.other at 1, 0
    with index.one_mem, index.zero_mem, index.one_ne_zero
  have b02 := basis.other at 2, 0
    with index.two_mem, index.zero_mem, index.two_ne_zero
  have b10 := basis.other at 0, 1
    with index.zero_mem, index.one_mem, index.zero_ne_one
  have b12 := basis.other at 2, 1
    with index.two_mem, index.one_mem, index.two_ne_one
  have b20 := basis.other at 0, 2
    with index.zero_mem, index.two_mem, index.zero_ne_two
  have b21 := basis.other at 1, 2
    with index.one_mem, index.two_mem, index.one_ne_two
  have entries : ∀ i ∈ 3, ∀ k ∈ 3, normSq(cross(u, v)) * (M[i, k]:R) =
      normSq(cross(u, v)) * (basis(i)(k):R) +
      drift(M, u, v, i) * (cross(u, v)(k):R)
    intros i hi k hk
    exact fixed.entry with matrix, vectorU, vectorV, fixedU, fixedV, hi, hk
  have e00 := entries with 0, index.zero_mem, 0, index.zero_mem
  have e01 := entries with 0, index.zero_mem, 1, index.one_mem
  have e02 := entries with 0, index.zero_mem, 2, index.two_mem
  have e10 := entries with 1, index.one_mem, 0, index.zero_mem
  have e11 := entries with 1, index.one_mem, 1, index.one_mem
  have e12 := entries with 1, index.one_mem, 2, index.two_mem
  have e20 := entries with 2, index.two_mem, 0, index.zero_mem
  have e21 := entries with 2, index.two_mem, 1, index.one_mem
  have e22 := entries with 2, index.two_mem, 2, index.two_mem
  rw b00 at e00
  rw b01 at e01
  rw b02 at e02
  rw b10 at e10
  rw b11 at e11
  rw b12 at e12
  rw b20 at e20
  rw b21 at e21
  rw b22 at e22
  -- The determinant: 1 = det M, and |w|⁶ det M expands through the entries.
  have detValue := determinant3.value at M
  rw unit at detValue
  have cubic : normSq(cross(u, v)) * normSq(cross(u, v)) *
      normSq(cross(u, v)) * (1:R) =
      (normSq(cross(u, v)) * (M[0, 0]:R)) *
        ((normSq(cross(u, v)) * (M[1, 1]:R)) *
          (normSq(cross(u, v)) * (M[2, 2]:R)) -
         (normSq(cross(u, v)) * (M[1, 2]:R)) *
          (normSq(cross(u, v)) * (M[2, 1]:R))) -
      (normSq(cross(u, v)) * (M[0, 1]:R)) *
        ((normSq(cross(u, v)) * (M[1, 0]:R)) *
          (normSq(cross(u, v)) * (M[2, 2]:R)) -
         (normSq(cross(u, v)) * (M[1, 2]:R)) *
          (normSq(cross(u, v)) * (M[2, 0]:R))) +
      (normSq(cross(u, v)) * (M[0, 2]:R)) *
        ((normSq(cross(u, v)) * (M[1, 0]:R)) *
          (normSq(cross(u, v)) * (M[2, 1]:R)) -
         (normSq(cross(u, v)) * (M[1, 1]:R)) *
          (normSq(cross(u, v)) * (M[2, 0]:R)))
    rw detValue
    ring
  rw [e00, e01, e02, e10, e11, e12, e20, e21, e22] at cubic
  have driftScaled : (normSq(cross(u, v)) *
      (drift(M, u, v, 0) * (cross(u, v)(0):R) +
        drift(M, u, v, 1) * (cross(u, v)(1):R) +
        drift(M, u, v, 2) * (cross(u, v)(2):R))) *
      normSq(cross(u, v)) = (0:R) * normSq(cross(u, v))
    symm at cubic
    linear_combination cubic
  have driftOnce := realMulValue.right_cancel_of_nonzero at
    normSq(cross(u, v)) * (drift(M, u, v, 0) * (cross(u, v)(0):R) +
      drift(M, u, v, 1) * (cross(u, v)(1):R) +
      drift(M, u, v, 2) * (cross(u, v)(2):R)),
    (0:R), normSq(cross(u, v)) with nonzero, driftScaled
  have driftTwice : (drift(M, u, v, 0) * (cross(u, v)(0):R) +
      drift(M, u, v, 1) * (cross(u, v)(1):R) +
      drift(M, u, v, 2) * (cross(u, v)(2):R)) *
      normSq(cross(u, v)) = (0:R) * normSq(cross(u, v))
    linear_combination driftOnce
  have driftDot := realMulValue.right_cancel_of_nonzero at
    drift(M, u, v, 0) * (cross(u, v)(0):R) +
      drift(M, u, v, 1) * (cross(u, v)(1):R) +
      drift(M, u, v, 2) * (cross(u, v)(2):R), (0:R), normSq(cross(u, v))
    with nonzero, driftTwice
  -- The image of w: M · w = w + drift, and it has the length of w.
  have image := matrixVector.vector with matrix, wVector
  have moved : ∀ i ∈ 3,
      ((M · cross(u, v))(i):R) = (cross(u, v)(i):R) + drift(M, u, v, i)
    intros i hi
    have entry := matrixVector.entry at M, cross(u, v), i
      with matrix, wVector, hi
    have component := vector.component_real at M · cross(u, v), i
      with image, hi
    have wi := vector.component_real at cross(u, v), i with wVector, hi
    have driftI := drift.real at M, u, v, i with matrix, vectorU, vectorV, hi
    have shiftI := rowShift.vector at M, i with matrix, hi
    obtain ⟨si0, si1, si2⟩ := vector.components with shiftI
    have basisDot := basis.dot with wVector, hi
    have basisVector := basis.vector with hi
    have b0 := vector.component_real at basis(i), 0
      with basisVector, index.zero_mem
    have b1 := vector.component_real at basis(i), 1
      with basisVector, index.one_mem
    have b2 := vector.component_real at basis(i), 2
      with basisVector, index.two_mem
    obtain ⟨mi0, mi1, mi2⟩ := Matrix.row_real at M, i with hi
    have f0 := entries with i, hi, 0, index.zero_mem
    have f1 := entries with i, hi, 1, index.one_mem
    have f2 := entries with i, hi, 2, index.two_mem
    have same : ((M · cross(u, v))(i):R) * normSq(cross(u, v)) =
        ((cross(u, v)(i):R) + drift(M, u, v, i)) * normSq(cross(u, v))
      linear_combination normSq(cross(u, v)) * entry + (cross(u, v)(0):R) * f0 +
        (cross(u, v)(1):R) * f1 + (cross(u, v)(2):R) * f2 +
        normSq(cross(u, v)) * basisDot - drift(M, u, v, i) * normValue
    exact realMulValue.right_cancel_of_nonzero at ((M · cross(u, v))(i):R),
      (cross(u, v)(i):R) + drift(M, u, v, i), normSq(cross(u, v))
      with nonzero, same
  have moved0 := moved with 0, index.zero_mem
  have moved1 := moved with 1, index.one_mem
  have moved2 := moved with 2, index.two_mem
  have norm := Orthogonal.normSq with orthogonal, wVector
  rw [normSq.value, normSq.value, moved0, moved1, moved2] at norm
  have squares : drift(M, u, v, 0) * drift(M, u, v, 0) +
      drift(M, u, v, 1) * drift(M, u, v, 1) +
      drift(M, u, v, 2) * drift(M, u, v, 2) = 0
    linear_combination norm - driftDot - driftDot
  obtain ⟨z0, z1, z2⟩ := sumSquares.eq_zero at drift(M, u, v, 0),
    drift(M, u, v, 1), drift(M, u, v, 2) with squares
  have driftZero : ∀ i ∈ 3, drift(M, u, v, i) = 0
    intros i hi
    have alternatives := index.cases with hi
    rcases alternatives with at0 | at1 | at2
    . rw at0
      exact z0
    . rw at1
      exact z1
    . rw at2
      exact z2
  -- Every entry of M is the matching entry of the identity.
  apply Matrix.ext with matrix, one
  intros i hi j hj
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) :=
    Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) :=
    Ring.one_mem with *
  have shape := entries with i, hi, j, hj
  have vanish := driftZero with i, hi
  rw vanish at shape
  have shiftI := rowShift.vector at M, i with matrix, hi
  obtain ⟨si0, si1, si2⟩ := vector.components with shiftI
  have basisVector := basis.vector with hi
  have bij := vector.component_real at basis(i), j
    with basisVector, hj
  have mij := Matrix.real_entry at M, i, j with matrix, hi, hj
  have wj := vector.component_real at cross(u, v), j with wVector, hj
  have same : (M[i, j]:R) * normSq(cross(u, v)) =
      (basis(i)(j):R) * normSq(cross(u, v))
    linear_combination shape
  have entry := realMulValue.right_cancel_of_nonzero at (M[i, j]:R),
    (basis(i)(j):R), normSq(cross(u, v)) with nonzero, same
  have basisValue := basis.value at i, j with hi, hj
  have symmetric := singleValue.symmetric at i, j
  have oneEntry := matrixRing.one_entry at realRing, 3, i, j with comm, hi, hj
  rw [entry, basisValue, oneEntry, symmetric]
  rfl

-- A rotation that is not the identity fixes at most two points of the
-- sphere, a point and its opposite.
theorem so3.fixed_points (M : Set)
  requires member : M ∈ so3Matrices
  requires nontrivial : M ≠ Ring.one(matrixRing(realRing, 3))
  shows ∃ p ∈ S², ∀ v ∈ S², M · v = v → v = p ∨ v = vectorNeg(p)
proof
  have split : (∃ u ∈ S², M · u = u) ∨ ¬(∃ u ∈ S², M · u = u)
    tauto
  cases split with some | none
  . obtain ⟨u, hu, fixedU⟩ := some
    refine ⟨u, hu, ?_⟩
    intros v hv fixedV
    by_contra
    have distinct : v ≠ u
      intro equal
      apply this
      left
      exact equal
    have opposite : v ≠ vectorNeg(u)
      intro equal
      apply this
      right
      exact equal
    have identity := so3.fixed_pair with member, hu, hv, fixedU, fixedV,
      distinct, opposite
    exact nontrivial with identity
  . have poleVector := basis.vector at 2 with index.two_mem
    have poleSpace := ℝ³.of_function with poleVector
    have same := basis.same at 2 with index.two_mem
    have other0 := basis.other at 0, 2
      with index.zero_mem, index.two_mem, index.zero_ne_two
    have other1 := basis.other at 1, 2
      with index.one_mem, index.two_mem, index.one_ne_two
    have poleUnit : normSq(basis(2)) = (1:R)
      rw [normSq.value, same, other0, other1]
      ring
    have poleIn := S².membership.backward at basis(2)
      with ⟨poleSpace, poleUnit⟩
    refine ⟨basis(2), poleIn, ?_⟩
    intros v hv fixedV
    exfalso
    apply none
    exact ⟨v, hv, fixedV⟩