-- Explicit 3 × 3 real matrices: triples as functions on 3, the matrix
-- matrix3of(a, b, c, d, e, f, g, h, k) with the given rows as an element of
-- matrixRing(realRing, 3), its entries, and the entries of a product of
-- two 3 × 3 real matrices as sums of three terms
-- 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.Absorption.Triples
import Rotation.Vectors
import Set.Tuple

-- The index set 3 = {0, 1, 2}, as Rotation/Vectors states it.
theorem threeIndex.cases (i : Set)
  requires member : i ∈ 3
  shows i = 0 ∨ i = 1 ∨ i = 2
proof
  exact index.cases with member

theorem threeIndex.zero_ne_one
  shows (0:N) ≠ (1:N)
proof
  exact index.zero_ne_one

theorem threeIndex.zero_ne_two
  shows (0:N) ≠ (2:N)
proof
  exact index.zero_ne_two

theorem threeIndex.one_ne_two
  shows (1:N) ≠ (2:N)
proof
  exact index.one_ne_two

-- The operations of realRing read as the real operations.
theorem realRing.call_add (x y : Set)
  shows call2(Ring.add(realRing), x, y) = call2(realAdd, x, y)
proof
  simp [realRing, Ring.mk.add]

theorem realRing.call_mul (x y : Set)
  shows call2(Ring.mul(realRing), x, y) = call2(realMul, x, y)
proof
  simp [realRing, Ring.mk.mul]

theorem realRing.zero_eq
  shows Ring.zero(realRing) = realZero
proof
  simp [realRing, Ring.mk.zero]

theorem realRing.one_eq
  shows Ring.one(realRing) = realOne
proof
  simp [realRing, Ring.mk.one]

-- A finite ring sum over the index set 3 is the sum of its three terms.
theorem finiteRingSum.over_three (A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : 3 → A
  shows finiteRingSum(3, A, add, zero, neg, mul, one, w) =
    call2(add, call2(add, call2(add, zero, w(0)), w(1)), w(2))
proof
  have enumeration := identity.bijective at 3
  have indexed := finiteRingSum.enumeration at 3, A, add, zero, neg, mul, one,
    w, identity(3), 3 with ring, weights, enumeration
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  have at0 := identity.apply at 0, 3 with zeroIn
  have at1 := identity.apply at 1, 3 with oneIn
  have at2 := identity.apply at 2, 3 with twoIn
  rw indexed
  simp [indexedRingSum, at0, at1, at2]

-- A triple (a, b, c) as the function on 3 with those values.
defunique tripleValue (A a b c j : Set) (v ∈ A) :=
  (j = 0 ∧ v = a) ∨ (j = 1 ∧ v = b) ∨ (j = 2 ∧ v = c)
requires aIn : a ∈ A
requires bIn : b ∈ A
requires cIn : c ∈ A
requires index : j ∈ 3
proof
  have alternatives := threeIndex.cases with index
  rcases alternatives with first | second | third
  . refine ⟨a, aIn, ?_⟩
    left
    exact ⟨first, rfl⟩
  . refine ⟨b, bIn, ?_⟩
    right
    left
    exact ⟨second, rfl⟩
  . refine ⟨c, cIn, ?_⟩
    right
    right
    exact ⟨third, rfl⟩
uniqueness
  intros u hu first v hv second
  have d01 := threeIndex.zero_ne_one
  have d02 := threeIndex.zero_ne_two
  have d12 := threeIndex.one_ne_two
  rcases first with firstZero | firstOne | firstTwo
  . obtain ⟨jZero, ua⟩ := firstZero
    rcases second with secondZero | secondOne | secondTwo
    . obtain ⟨kZero, va⟩ := secondZero
      cc
    . obtain ⟨kOne, vb⟩ := secondOne
      exfalso
      apply d01
      cc
    . obtain ⟨kTwo, vc⟩ := secondTwo
      exfalso
      apply d02
      cc
  . obtain ⟨jOne, ub⟩ := firstOne
    rcases second with secondZero | secondOne | secondTwo
    . obtain ⟨kZero, va⟩ := secondZero
      exfalso
      apply d01
      cc
    . obtain ⟨kOne, vb⟩ := secondOne
      cc
    . obtain ⟨kTwo, vc⟩ := secondTwo
      exfalso
      apply d12
      cc
  . obtain ⟨jTwo, uc⟩ := firstTwo
    rcases second with secondZero | secondOne | secondTwo
    . obtain ⟨kZero, va⟩ := secondZero
      exfalso
      apply d02
      cc
    . obtain ⟨kOne, vb⟩ := secondOne
      exfalso
      apply d12
      cc
    . obtain ⟨kTwo, vc⟩ := secondTwo
      cc

defgraph triple (A a b c : Set) (j ∈ 3) : A := tripleValue(A, a, b, c, j)
requires aIn : a ∈ A
requires bIn : b ∈ A
requires cIn : c ∈ A
proof
  have selected := tripleValue.selected at A, a, b, c, j with *
  exact selected.left

section TripleValues
variable (A a b c : Set)
hypothesis aIn : a ∈ A
hypothesis bIn : b ∈ A
hypothesis cIn : c ∈ A

theorem triple.zero
  shows triple(A, a, b, c)(0) = a
proof
  have zeroIn : 0 ∈ 3 by typecheck
  have value := triple.value at A, a, b, c, 0 with *
  have selected := tripleValue.selected at A, a, b, c, 0 with *
  have d01 := threeIndex.zero_ne_one
  have d02 := threeIndex.zero_ne_two
  rw value
  obtain ⟨inA, property⟩ := selected
  rcases property with same | badOne | badTwo
  . exact same.right
  . exfalso
    exact d01 with badOne.left
  . exfalso
    exact d02 with badTwo.left

theorem triple.one
  shows triple(A, a, b, c)(1) = b
proof
  have oneIn : 1 ∈ 3 by typecheck
  have value := triple.value at A, a, b, c, 1 with *
  have selected := tripleValue.selected at A, a, b, c, 1 with *
  have d01 := threeIndex.zero_ne_one
  have d12 := threeIndex.one_ne_two
  rw value
  obtain ⟨inA, property⟩ := selected
  rcases property with badZero | same | badTwo
  . exfalso
    have flipped := badZero.left
    symm at flipped
    exact d01 with flipped
  . exact same.right
  . exfalso
    exact d12 with badTwo.left

theorem triple.two
  shows triple(A, a, b, c)(2) = c
proof
  have twoIn : 2 ∈ 3 by typecheck
  have value := triple.value at A, a, b, c, 2 with *
  have selected := tripleValue.selected at A, a, b, c, 2 with *
  have d02 := threeIndex.zero_ne_two
  have d12 := threeIndex.one_ne_two
  rw value
  obtain ⟨inA, property⟩ := selected
  rcases property with badZero | badOne | same
  . exfalso
    have flipped := badZero.left
    symm at flipped
    exact d02 with flipped
  . exfalso
    have flipped := badOne.left
    symm at flipped
    exact d12 with flipped
  . exact same.right

end TripleValues

-- The 3 × 3 matrix with the three given rows, rows being functions 3 → ℝ.
defgraph matrix3 (r0 r1 r2 : Set) (p ∈ 3 × 3) : ℝ :=
  triple(functionSpace(3, ℝ), r0, r1, r2)(fst(p))(snd(p))
requires row0 : r0 ∈ functionSpace(3, ℝ)
requires row1 : r1 ∈ functionSpace(3, ℝ)
requires row2 : r2 ∈ functionSpace(3, ℝ)
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member
  have rows := triple.function at functionSpace(3, ℝ), r0, r1, r2 with *
  rw [shape, fst.pair, snd.pair]
  have rowIn := FunctionBetween.apply_closed with rows, hi
  have rowFunction := functionSpace.mem_iff.forward with rowIn
  exact FunctionBetween.apply_closed with rowFunction, hj

section MatrixRows
variable (r0 r1 r2 : Set)
hypothesis row0 : r0 ∈ functionSpace(3, ℝ)
hypothesis row1 : r1 ∈ functionSpace(3, ℝ)
hypothesis row2 : r2 ∈ functionSpace(3, ℝ)

theorem matrix3.entry (i j : Set)
  requires hi : i ∈ 3
  requires hj : j ∈ 3
  shows matrix3(r0, r1, r2)[i, j] = triple(functionSpace(3, ℝ), r0, r1, r2)(i)(j)
proof
  have pair := product.pair at i, j, 3, 3 with *
  have value := matrix3.value at r0, r1, r2, (i, j) with *
  rw [value, fst.pair, snd.pair]
  rfl

theorem matrix3.square
  shows matrix3(r0, r1, r2) ∈ squareMatrices(realRing, 3)
proof
  have function := matrix3.function at r0, r1, r2 with *
  rw ← realRing.carrierOf at function
  exact squareMatrices.of_function with function

instance matrix3.matrix
  shows matrix3(r0, r1, r2) : realRing ^ 3 × 3
proof
  have square : matrix3(r0, r1, r2) ∈ squareMatrices(realRing, 3) := matrix3.square with *
  exact Matrix.of_square with square

end MatrixRows

-- A row of three reals, and the matrix with nine given real entries.
def row3 (a b c : Set) : Set := triple(ℝ, a, b, c)
def matrix3of (a b c d e f g h k : Set) : Set :=
  matrix3(row3(a, b, c), row3(d, e, f), row3(g, h, k))

theorem row3.graph (a b c : Set)
  shows row3(a, b, c) = triple(ℝ, a, b, c)
proof
  simp [row3]

theorem matrix3of.graph (a b c d e f g h k : Set)
  shows matrix3of(a, b, c, d, e, f, g, h, k) =
    matrix3(row3(a, b, c), row3(d, e, f), row3(g, h, k))
proof
  simp [matrix3of]

instance row3.member (a b c : Real)
  shows row3(a, b, c) ∈ functionSpace(3, ℝ)
proof
  have function := triple.function at ℝ, a, b, c with *
  rw row3.graph
  exact functionSpace.mem_iff.backward with function

section Entries
variable (a b c d e f g h k : Real)

instance matrix3of.matrix
  shows matrix3of(a, b, c, d, e, f, g, h, k) : realRing ^ 3 × 3
proof
  rw matrix3of.graph
  exact matrix3.matrix with *

theorem matrix3of.entry (i j : Set)
  requires hi : i ∈ 3
  requires hj : j ∈ 3
  shows matrix3of(a, b, c, d, e, f, g, h, k)[i, j] =
    triple(functionSpace(3, ℝ), row3(a, b, c), row3(d, e, f), row3(g, h, k))(i)(j)
proof
  rw matrix3of.graph
  exact matrix3.entry with *

theorem matrix3of.entry00
  shows matrix3of(a, b, c, d, e, f, g, h, k)[0, 0] = a
proof
  have zeroIn : 0 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.zero, row3.graph, triple.zero]
  rfl

theorem matrix3of.entry01
  shows matrix3of(a, b, c, d, e, f, g, h, k)[0, 1] = b
proof
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.zero, row3.graph, triple.one]
  rfl

theorem matrix3of.entry02
  shows matrix3of(a, b, c, d, e, f, g, h, k)[0, 2] = c
proof
  have zeroIn : 0 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.zero, row3.graph, triple.two]
  rfl

theorem matrix3of.entry10
  shows matrix3of(a, b, c, d, e, f, g, h, k)[1, 0] = d
proof
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.one, row3.graph, triple.zero]
  rfl

theorem matrix3of.entry11
  shows matrix3of(a, b, c, d, e, f, g, h, k)[1, 1] = e
proof
  have oneIn : 1 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.one, row3.graph, triple.one]
  rfl

theorem matrix3of.entry12
  shows matrix3of(a, b, c, d, e, f, g, h, k)[1, 2] = f
proof
  have oneIn : 1 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.one, row3.graph, triple.two]
  rfl

theorem matrix3of.entry20
  shows matrix3of(a, b, c, d, e, f, g, h, k)[2, 0] = g
proof
  have zeroIn : 0 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.two, row3.graph, triple.zero]
  rfl

theorem matrix3of.entry21
  shows matrix3of(a, b, c, d, e, f, g, h, k)[2, 1] = h
proof
  have oneIn : 1 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.two, row3.graph, triple.one]
  rfl

theorem matrix3of.entry22
  shows matrix3of(a, b, c, d, e, f, g, h, k)[2, 2] = k
proof
  have twoIn : 2 ∈ 3 by typecheck
  rw [matrix3of.entry, triple.two, row3.graph, triple.two]
  rfl

end Entries

-- Entries of 3 × 3 real matrices are real, and a product entry is the
-- sum of three products.
section Products
variable (M N : realRing ^ 3 × 3)

instance matrix3.entry_real (i j : Set)
  requires hi : i ∈ 3
  requires hj : j ∈ 3
  shows M[i, j] ∈ ℝ
proof
  have entry := Matrix.entry at M, realRing, 3, i, j with *
  rw realRing.carrierOf at entry
  exact entry

theorem matrix3.mul_entry (i j : Set)
  requires hi : i ∈ 3
  requires hj : j ∈ 3
  shows call2(Ring.mul(matrixRing(realRing, 3)), M, N)[i, j] =
    (M[i, 0]:R) * (N[0, j]:R) + (M[i, 1]:R) * (N[1, j]:R) + (M[i, 2]:R) * (N[2, j]:R)
proof
  have comm := realRing.comm_ring
  have parts := CommRing.parts with comm
  have squareM := Matrix.square at M, realRing, 3 with assumption
  have squareN := Matrix.square at N, realRing, 3 with assumption
  have shapeM := squareMatrices.membership.forward with squareM
  have shapeN := squareMatrices.membership.forward with squareN
  have entry := matrixRing.mul_entry at realRing, 3, M, N, i, j with *
  have weights := matrixProductWeights.function at 3, Ring.carrier(realRing),
    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),
    Ring.mul(realRing), Ring.one(realRing), M, N, i, j with *
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  have w0 := matrixProductWeights.value at 3, Ring.carrier(realRing),
    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),
    Ring.mul(realRing), Ring.one(realRing), M, N, i, j, 0 with *
  have w1 := matrixProductWeights.value at 3, Ring.carrier(realRing),
    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),
    Ring.mul(realRing), Ring.one(realRing), M, N, i, j, 1 with *
  have w2 := matrixProductWeights.value at 3, Ring.carrier(realRing),
    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),
    Ring.mul(realRing), Ring.one(realRing), M, N, i, j, 2 with *
  have sum := finiteRingSum.over_three with parts, weights
  rw entry
  simp [matrixProductEntry]
  rw [realRing.call_add, realRing.call_add, realRing.call_add,
    realRing.call_mul, realRing.call_mul, realRing.call_mul, realRing.zero_eq]
  have m0 : M[i, 0] ∈ ℝ := matrix3.entry_real with *
  have m1 : M[i, 1] ∈ ℝ := matrix3.entry_real with *
  have m2 : M[i, 2] ∈ ℝ := matrix3.entry_real with *
  have n0 : N[0, j] ∈ ℝ := matrix3.entry_real with *
  have n1 : N[1, j] ∈ ℝ := matrix3.entry_real with *
  have n2 : N[2, j] ∈ ℝ := matrix3.entry_real with *
  ring

instance matrix3.mul_matrix
  shows call2(Ring.mul(matrixRing(realRing, 3)), M, N) : realRing ^ 3 × 3
proof
  have comm := realRing.comm_ring
  have ring := matrixRing.ring at realRing, 3 with comm
  have mIn : M ∈ Ring.carrier(matrixRing(realRing, 3)) := Matrix.mem_ring with assumption
  have nIn : N ∈ Ring.carrier(matrixRing(realRing, 3)) := Matrix.mem_ring with assumption
  have productIn : call2(Ring.mul(matrixRing(realRing, 3)), M, N) ∈ Ring.carrier(matrixRing(realRing, 3)) :=
    Ring.mul_mem with *
  exact Matrix.of_mem with productIn

end Products

-- The 3 × 3 real matrices as a type: Matrix3(M) is the guard
-- M : realRing ^ 3 × 3, and M * N on such matrices is matrixMul3(M, N),
-- the product of the matrix ring.
class Matrix3 (M : Set) := Matrix(M, realRing, 3, 3)
def matrixMul3 (M N : Set) : Set := call2(Ring.mul(matrixRing(realRing, 3)), M, N)
notation infixl 70 "*" => matrixMul3 for Matrix3

theorem matrixMul3.graph (M N : Set)
  shows matrixMul3(M, N) = call2(Ring.mul(matrixRing(realRing, 3)), M, N)
proof
  simp [matrixMul3]

instance Matrix3.of_matrix (M : Set)
  requires matrix : M : realRing ^ 3 × 3
  shows Matrix3(M)
proof
  exact matrix

theorem Matrix3.matrix (M : Matrix3)
  shows M : realRing ^ 3 × 3
proof
  have typed : Matrix3(M) by assumption
  unfold Matrix3 at typed
  exact typed

instance Matrix3.mul (M N : Matrix3)
  shows Matrix3(matrixMul3(M, N))
proof
  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *
  have matrixN : N : realRing ^ 3 × 3 := Matrix3.matrix with *
  have product : call2(Ring.mul(matrixRing(realRing, 3)), M, N) : realRing ^ 3 × 3 :=
    matrix3.mul_matrix with *
  unfold Matrix3
  rw matrixMul3.graph
  exact product

instance Matrix3.entry_real (M : Matrix3) (i j : Set)
  requires hi : i ∈ 3
  requires hj : j ∈ 3
  shows M[i, j] ∈ ℝ
proof
  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *
  exact matrix3.entry_real with *

theorem Matrix3.mul_entry (M N : Matrix3) (i j : Set)
  requires hi : i ∈ 3
  requires hj : j ∈ 3
  shows matrixMul3(M, N)[i, j] =
    (M[i, 0]:R) * (N[0, j]:R) + (M[i, 1]:R) * (N[1, j]:R) + (M[i, 2]:R) * (N[2, j]:R)
proof
  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *
  have matrixN : N : realRing ^ 3 × 3 := Matrix3.matrix with *
  rw matrixMul3.graph
  exact matrix3.mul_entry with *

instance Matrix3.one
  shows Matrix3(Ring.one(matrixRing(realRing, 3)))
proof
  have comm := realRing.comm_ring
  have ring := matrixRing.ring at realRing, 3 with comm
  have oneIn : Ring.one(matrixRing(realRing, 3)) ∈ Ring.carrier(matrixRing(realRing, 3)) :=
    Ring.one_mem with *
  unfold Matrix3
  exact Matrix.of_mem with oneIn

theorem Matrix3.ext (M N : Matrix3)
  requires entries : ∀ i ∈ 3, ∀ j ∈ 3, M[i, j] = N[i, j]
  shows M = N
proof
  have comm := realRing.comm_ring
  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *
  have matrixN : N : realRing ^ 3 × 3 := Matrix3.matrix with *
  exact matrixRing.ext with entries

-- Two explicit matrices with the same entries are equal, the product of
-- two explicit matrices, and the identity matrix as an explicit matrix.
theorem matrix3of.congr (a b c d e f g h k l m n o p q r s u : Real)
  requires e00 : a = l
  requires e01 : b = m
  requires e02 : c = n
  requires e10 : d = o
  requires e11 : e = p
  requires e12 : f = q
  requires e20 : g = r
  requires e21 : h = s
  requires e22 : k = u
  shows matrix3of(a, b, c, d, e, f, g, h, k) = matrix3of(l, m, n, o, p, q, r, s, u)
proof
  rw [e00, e01, e02, e10, e11, e12, e20, e21, e22]
  rfl

tactic matrix3of_entries := simp [matrix3of.entry00, matrix3of.entry01, matrix3of.entry02, matrix3of.entry10, matrix3of.entry11, matrix3of.entry12, matrix3of.entry20, matrix3of.entry21, matrix3of.entry22]

theorem matrix3of.mul (a b c d e f g h k l m n o p q r s u : Real)
  shows matrixMul3(matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u)) =
    matrix3of(a * l + b * o + c * r, a * m + b * p + c * s, a * n + b * q + c * u,
      d * l + e * o + f * r, d * m + e * p + f * s, d * n + e * q + f * u,
      g * l + h * o + k * r, g * m + h * p + k * s, g * n + h * q + k * u)
proof
  have leftMatrix : matrix3of(a, b, c, d, e, f, g, h, k) : realRing ^ 3 × 3 :=
    matrix3of.matrix with *
  have rightMatrix : matrix3of(l, m, n, o, p, q, r, s, u) : realRing ^ 3 × 3 :=
    matrix3of.matrix with *
  have leftTyped : Matrix3(matrix3of(a, b, c, d, e, f, g, h, k)) :=
    Matrix3.of_matrix with leftMatrix
  have rightTyped : Matrix3(matrix3of(l, m, n, o, p, q, r, s, u)) :=
    Matrix3.of_matrix with rightMatrix
  have entries : ∀ i ∈ 3, ∀ j ∈ 3,
      matrixMul3(matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u))[i, j] =
      matrix3of(a * l + b * o + c * r, a * m + b * p + c * s, a * n + b * q + c * u,
        d * l + e * o + f * r, d * m + e * p + f * s, d * n + e * q + f * u,
        g * l + h * o + k * r, g * m + h * p + k * s, g * n + h * q + k * u)[i, j]
    intros i hi j hj
    have entry := Matrix3.mul_entry at matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u), i, j with leftTyped, rightTyped, hi, hj
    rw entry
    have rows := threeIndex.cases with hi
    have columns := threeIndex.cases with hj
    rcases rows with rowZero | rowOne | rowTwo
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowZero, columnZero]
        matrix3of_entries
      . rw [rowZero, columnOne]
        matrix3of_entries
      . rw [rowZero, columnTwo]
        matrix3of_entries
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowOne, columnZero]
        matrix3of_entries
      . rw [rowOne, columnOne]
        matrix3of_entries
      . rw [rowOne, columnTwo]
        matrix3of_entries
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowTwo, columnZero]
        matrix3of_entries
      . rw [rowTwo, columnOne]
        matrix3of_entries
      . rw [rowTwo, columnTwo]
        matrix3of_entries
  have e00 : a * l + b * o + c * r ∈ ℝ by typecheck
  have e01 : a * m + b * p + c * s ∈ ℝ by typecheck
  have e02 : a * n + b * q + c * u ∈ ℝ by typecheck
  have e10 : d * l + e * o + f * r ∈ ℝ by typecheck
  have e11 : d * m + e * p + f * s ∈ ℝ by typecheck
  have e12 : d * n + e * q + f * u ∈ ℝ by typecheck
  have e20 : g * l + h * o + k * r ∈ ℝ by typecheck
  have e21 : g * m + h * p + k * s ∈ ℝ by typecheck
  have e22 : g * n + h * q + k * u ∈ ℝ by typecheck
  have resultMatrix : matrix3of(a * l + b * o + c * r, a * m + b * p + c * s,
      a * n + b * q + c * u, d * l + e * o + f * r, d * m + e * p + f * s,
      d * n + e * q + f * u, g * l + h * o + k * r, g * m + h * p + k * s,
      g * n + h * q + k * u) : realRing ^ 3 × 3 :=
    matrix3of.matrix with *
  have productTyped : Matrix3(matrixMul3(matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u))) :=
    Matrix3.mul with leftTyped, rightTyped
  have resultTyped : Matrix3(matrix3of(a * l + b * o + c * r, a * m + b * p + c * s,
      a * n + b * q + c * u, d * l + e * o + f * r, d * m + e * p + f * s,
      d * n + e * q + f * u, g * l + h * o + k * r, g * m + h * p + k * s,
      g * n + h * q + k * u)) :=
    Matrix3.of_matrix with resultMatrix
  exact Matrix3.ext with productTyped, resultTyped, entries

theorem matrix3of.one
  shows matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R)) =
    Ring.one(matrixRing(realRing, 3))
proof
  have zeroReal : (0:R) ∈ ℝ by typecheck
  have oneReal : (1:R) ∈ ℝ by typecheck
  have d01 := threeIndex.zero_ne_one
  have d02 := threeIndex.zero_ne_two
  have d12 := threeIndex.one_ne_two
  have entries : ∀ i ∈ 3, ∀ j ∈ 3,
      matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R))[i, j] =
      Ring.one(matrixRing(realRing, 3))[i, j]
    intros i hi j hj
    have comm := realRing.comm_ring
    have entry := matrixRing.one_entry at realRing, 3, i, j with *
    rw [entry, realRing.carrierOf, realRing.zero_eq, realRing.one_eq]
    have rows := threeIndex.cases with hi
    have columns := threeIndex.cases with hj
    rcases rows with rowZero | rowOne | rowTwo
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowZero, columnZero, matrix3of.entry00, singleValue.same]
        rfl
      . have different : (0:N) ≠ (1:N) := d01
        rw [rowZero, columnOne, matrix3of.entry01, singleValue.other]
        rfl
      . have different : (0:N) ≠ (2:N) := d02
        rw [rowZero, columnTwo, matrix3of.entry02, singleValue.other]
        rfl
    . rcases columns with columnZero | columnOne | columnTwo
      . have different : (1:N) ≠ (0:N)
          intro same
          symm at same
          exact d01 with same
        rw [rowOne, columnZero, matrix3of.entry10, singleValue.other]
        rfl
      . rw [rowOne, columnOne, matrix3of.entry11, singleValue.same]
        rfl
      . have different : (1:N) ≠ (2:N) := d12
        rw [rowOne, columnTwo, matrix3of.entry12, singleValue.other]
        rfl
    . rcases columns with columnZero | columnOne | columnTwo
      . have different : (2:N) ≠ (0:N)
          intro same
          symm at same
          exact d02 with same
        rw [rowTwo, columnZero, matrix3of.entry20, singleValue.other]
        rfl
      . have different : (2:N) ≠ (1:N)
          intro same
          symm at same
          exact d12 with same
        rw [rowTwo, columnOne, matrix3of.entry21, singleValue.other]
        rfl
      . rw [rowTwo, columnTwo, matrix3of.entry22, singleValue.same]
        rfl
  have leftMatrix : matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R)) : realRing ^ 3 × 3 :=
    matrix3of.matrix with *
  have leftTyped : Matrix3(matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R))) :=
    Matrix3.of_matrix with leftMatrix
  have oneTyped : Matrix3(Ring.one(matrixRing(realRing, 3))) := Matrix3.one
  exact Matrix3.ext with leftTyped, oneTyped, entries