-- Bundled matrix rings: the ring value matrixRing(R, n) of the n × n
-- matrices over a bundled commutative ring R, its ring instance, the
-- entries of sums and products, and the determinant and adjugate of a
-- square matrix read off the ring; everything here is ZF
-- 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.Algebra.Ring.MatrixRing
import DeterminantIdentity
import Basic

-- The n × n matrices over R are the functions on the square of indices.
def squareMatrices (R n : Set) : Set := functionSpace(n × n, Ring.carrier(R))

theorem squareMatrices.membership (R n M : Set)
  shows M ∈ squareMatrices(R, n) ↔ RingMatrix(n, Ring.carrier(R), M)
proof
  simp [squareMatrices, RingMatrix, functionSpace.mem_iff]

theorem squareMatrices.function (R n M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows M : n × n → Ring.carrier(R)
proof
  have shape := squareMatrices.membership.forward with matrix
  unfold RingMatrix at shape
  exact shape

theorem squareMatrices.of_function (R n M : Set)
  requires function : M : n × n → Ring.carrier(R)
  shows M ∈ squareMatrices(R, n)
proof
  have shape : RingMatrix(n, Ring.carrier(R), M) by exact function
  exact squareMatrices.membership.backward with shape

-- The entrywise sum of two matrices.
defgraph matrixSum (R n M N : Set) (p ∈ n × n) : Ring.carrier(R) := M(p) + N(p)
requires ring : Ring(R)
requires matrixM : M ∈ squareMatrices(R, n)
requires matrixN : N ∈ squareMatrices(R, n)
proof
  have functionM := squareMatrices.function with matrixM
  have functionN := squareMatrices.function with matrixN
  have left := FunctionBetween.apply_closed with functionM, member
  have right := FunctionBetween.apply_closed with functionN, member
  exact Ring.add_mem with *

theorem matrixSum.entry (R n M N i j : Set)
  requires ring : Ring(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixSum(R, n, M, N)[i, j] = M[i, j] + N[i, j]
proof
  have pair := product.pair at i, j, n, n with *
  exact matrixSum.value at R, n, M, N, (i, j) with *

theorem matrixSum.matrix (R n M N : Set)
  requires ring : Ring(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  shows matrixSum(R, n, M, N) ∈ squareMatrices(R, n)
proof
  have function := matrixSum.function at R, n, M, N with *
  exact squareMatrices.of_function with function

-- The entrywise negation of a matrix.
defgraph matrixNegative (R n M : Set) (p ∈ n × n) : Ring.carrier(R) := -M(p)
requires ring : Ring(R)
requires matrix : M ∈ squareMatrices(R, n)
proof
  have function := squareMatrices.function with matrix
  have entry := FunctionBetween.apply_closed with function, member
  exact Ring.neg_mem with *

theorem matrixNegative.entry (R n M i j : Set)
  requires ring : Ring(R)
  requires matrix : M ∈ squareMatrices(R, n)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixNegative(R, n, M)[i, j] = -M[i, j]
proof
  have pair := product.pair at i, j, n, n with *
  exact matrixNegative.value at R, n, M, (i, j) with *

theorem matrixNegative.matrix (R n M : Set)
  requires ring : Ring(R)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixNegative(R, n, M) ∈ squareMatrices(R, n)
proof
  have function := matrixNegative.function at R, n, M with *
  exact squareMatrices.of_function with function

-- The product, entry by entry the finite sum of the engine.
defunique matrixProductValue (R : Set, n : Nat, M N p : Set) (a ∈ Ring.carrier(R)) :=
  ∃ i ∈ n, ∃ j ∈ n, p = (i, j) ∧
    a = matrixProductEntry(n, Ring.carrier(R), Ring.add(R), Ring.zero(R),
      Ring.neg(R), Ring.mul(R), Ring.one(R), M, N, i, j)
requires comm : CommRing(R)
requires matrixM : M ∈ squareMatrices(R, n)
requires matrixN : N ∈ squareMatrices(R, n)
requires pair : p ∈ n × n
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at
    n, n, p with *
  have parts := CommRing.parts with comm
  have shapeM := squareMatrices.membership.forward with matrixM
  have shapeN := squareMatrices.membership.forward with matrixN
  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, N, i, j with *
  have finiteN := Finite.natural at n
  have finite := Finite.product with finiteN, finiteN
  have value : matrixProductEntry(n, R.carrier, R.add, R.zero, R.neg, R.mul,
      R.one, M, N, i, j) ∈ R.carrier
    unfold matrixProductEntry
    exact finiteRingSum.closed with *
  refine ⟨matrixProductEntry(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
    M, N, i, j), value, i, hi, j, hj, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first
  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second
  have equal : (i, j) = (k, l)
    cc
  have coordinates := orderedPair.injective at i, j, k, l with equal
  cc

defgraph matrixProduct (R : Set, n : Nat, M N : Set) (p ∈ n × n) : Ring.carrier(R) :=
  matrixProductValue(R, n, M, N, p)
requires comm : CommRing(R)
requires matrixM : M ∈ squareMatrices(R, n)
requires matrixN : N ∈ squareMatrices(R, n)
proof
  have selected := matrixProductValue.selected at R, n, M, N, p with *
  exact selected.left

theorem matrixProduct.entry (R : Set, n : Nat, M N i j : Set)
  requires comm : CommRing(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixProduct(R, n, M, N)[i, j] =
    matrixProductEntry(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
      M, N, i, j)
proof
  have pair := product.pair at i, j, n, n with *
  have selected := matrixProductValue.selected at R, n, M, N, (i, j) with *
  obtain ⟨k, hk, l, hl, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := matrixProduct.value at R, n, M, N, (i, j) with *
  cc

theorem matrixProduct.matrix (R : Set, n : Nat, M N : Set)
  requires comm : CommRing(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  shows matrixProduct(R, n, M, N) ∈ squareMatrices(R, n)
proof
  have function := matrixProduct.function at R, n, M, N with *
  exact squareMatrices.of_function with function

-- The operations as graphs on the matrices, the data of the ring value.
defunique matrixAdditionValue (R n q : Set) (S ∈ squareMatrices(R, n)) :=
  ∃ M ∈ squareMatrices(R, n), ∃ N ∈ squareMatrices(R, n),
    q = (M, N) ∧ S = matrixSum(R, n, M, N)
requires ring : Ring(R)
requires pair : q ∈ squareMatrices(R, n) × squareMatrices(R, n)
proof
  obtain ⟨bound, M, hM, N, hN, shape⟩ := product.membership.forward at
    squareMatrices(R, n), squareMatrices(R, n), q with *
  have value := matrixSum.matrix at R, n, M, N with *
  refine ⟨matrixSum(R, n, M, N), value, M, hM, N, hN, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨M, hM, N, hN, shapeU, valueU⟩ := first
  obtain ⟨K, hK, L, hL, shapeV, valueV⟩ := second
  have equal : (M, N) = (K, L)
    cc
  have coordinates := orderedPair.injective at M, N, K, L with equal
  cc

defgraph matrixAddition (R n : Set) (q ∈ squareMatrices(R, n) × squareMatrices(R, n)) :
    squareMatrices(R, n) :=
  matrixAdditionValue(R, n, q)
requires ring : Ring(R)
proof
  have selected := matrixAdditionValue.selected at R, n, q with *
  exact selected.left

theorem matrixAddition.apply (R n M N : Set)
  requires ring : Ring(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  shows matrixAddition(R, n)(M, N) = matrixSum(R, n, M, N)
proof
  have pair := product.pair at M, N, squareMatrices(R, n), squareMatrices(R, n) with *
  have selected := matrixAdditionValue.selected at R, n, (M, N) with *
  obtain ⟨K, hK, L, hL, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := matrixAddition.value at R, n, (M, N) with *
  unfold call2
  cc

defunique matrixMultiplicationValue (R : Set, n : Nat, q : Set) (S ∈ squareMatrices(R, n)) :=
  ∃ M ∈ squareMatrices(R, n), ∃ N ∈ squareMatrices(R, n),
    q = (M, N) ∧ S = matrixProduct(R, n, M, N)
requires comm : CommRing(R)
requires pair : q ∈ squareMatrices(R, n) × squareMatrices(R, n)
proof
  obtain ⟨bound, M, hM, N, hN, shape⟩ := product.membership.forward at
    squareMatrices(R, n), squareMatrices(R, n), q with *
  have value := matrixProduct.matrix at R, n, M, N with *
  refine ⟨matrixProduct(R, n, M, N), value, M, hM, N, hN, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨M, hM, N, hN, shapeU, valueU⟩ := first
  obtain ⟨K, hK, L, hL, shapeV, valueV⟩ := second
  have equal : (M, N) = (K, L)
    cc
  have coordinates := orderedPair.injective at M, N, K, L with equal
  cc

defgraph matrixMultiplication (R : Set, n : Nat) (q ∈ squareMatrices(R, n) × squareMatrices(R, n)) :
    squareMatrices(R, n) :=
  matrixMultiplicationValue(R, n, q)
requires comm : CommRing(R)
proof
  have selected := matrixMultiplicationValue.selected at R, n, q with *
  exact selected.left

theorem matrixMultiplication.apply (R : Set, n : Nat, M N : Set)
  requires comm : CommRing(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  shows matrixMultiplication(R, n)(M, N) = matrixProduct(R, n, M, N)
proof
  have pair := product.pair at M, N, squareMatrices(R, n), squareMatrices(R, n) with *
  have selected := matrixMultiplicationValue.selected at R, n, (M, N) with *
  obtain ⟨K, hK, L, hL, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := matrixMultiplication.value at R, n, (M, N) with *
  unfold call2
  cc

defgraph matrixNegation (R n : Set) (M ∈ squareMatrices(R, n)) : squareMatrices(R, n) :=
  matrixNegative(R, n, M)
requires ring : Ring(R)
proof
  exact matrixNegative.matrix at R, n, M with *

-- The zero matrix and the identity matrix of the engine.
def zeroMatrix (R n : Set) : Set :=
  constantFunction(n × n, Ring.carrier(R), Ring.zero(R))
def oneMatrix (R n : Set) : Set :=
  identityMatrix(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R),
    Ring.mul(R), Ring.one(R))

-- The matrix ring itself.
def matrixRing (R n : Set) : Set :=
  Ring.mk(squareMatrices(R, n), matrixAddition(R, n), zeroMatrix(R, n),
    matrixNegation(R, n), matrixMultiplication(R, n), oneMatrix(R, n))

theorem matrixRing.carrierOf (R n : Set)
  shows Ring.carrier(matrixRing(R, n)) = squareMatrices(R, n)
proof
  simp [matrixRing, Ring.mk.carrier]

theorem matrixRing.addOf (R n : Set)
  shows Ring.add(matrixRing(R, n)) = matrixAddition(R, n)
proof
  simp [matrixRing, Ring.mk.add]

theorem matrixRing.zeroOf (R n : Set)
  shows Ring.zero(matrixRing(R, n)) = zeroMatrix(R, n)
proof
  simp [matrixRing, Ring.mk.zero]

theorem matrixRing.negOf (R n : Set)
  shows Ring.neg(matrixRing(R, n)) = matrixNegation(R, n)
proof
  simp [matrixRing, Ring.mk.neg]

theorem matrixRing.mulOf (R n : Set)
  shows Ring.mul(matrixRing(R, n)) = matrixMultiplication(R, n)
proof
  simp [matrixRing, Ring.mk.mul]

theorem matrixRing.oneOf (R n : Set)
  shows Ring.one(matrixRing(R, n)) = oneMatrix(R, n)
proof
  simp [matrixRing, Ring.mk.one]

section Constants
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)
notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem zeroMatrix.matrix
  shows zeroMatrix(R, n) ∈ squareMatrices(R, n)
proof
  have zeroIn : R[0] ∈ R := Ring.zero_mem with *
  have function := constantFunction.function at n × n, R.carrier, R.zero with *
  unfold zeroMatrix
  exact squareMatrices.of_function with function

theorem zeroMatrix.entry (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows zeroMatrix(R, n)[i, j] = R[0]
proof
  have zeroIn : R[0] ∈ R := Ring.zero_mem with *
  have pair := product.pair at i, j, n, n with *
  unfold zeroMatrix
  exact constantFunction.apply with *

theorem oneMatrix.matrix
  shows oneMatrix(R, n) ∈ squareMatrices(R, n)
proof
  have parts := CommRing.parts with comm
  have shape := identityMatrix.matrix at R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, n with *
  unfold oneMatrix
  exact squareMatrices.membership.backward with shape

theorem oneMatrix.entry (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows oneMatrix(R, n)[i, j] = singleValue(R.carrier, R.zero, R.one, j, i)
proof
  have parts := CommRing.parts with comm
  unfold oneMatrix
  exact identityMatrix.entry with *

theorem squareMatrices.entry (M i j : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  requires row : i ∈ n
  requires column : j ∈ n
  shows M[i, j] ∈ R
proof
  have function := squareMatrices.function with matrix
  have pair := product.pair at i, j, n, n with *
  exact FunctionBetween.apply_closed with function, pair

theorem squareMatrices.ext (M N : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]
  shows M = N
proof
  have shapeM := squareMatrices.membership.forward with matrixM
  have shapeN := squareMatrices.membership.forward with matrixN
  exact RingMatrix.ext with shapeM, shapeN, entries

end Constants

section AdditiveLaws
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)

theorem matrixSum.comm (M N : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  shows matrixSum(R, n, M, N) = matrixSum(R, n, N, M)
proof
  have left := matrixSum.matrix at R, n, M, N with *
  have right := matrixSum.matrix at R, n, N, M with *
  apply squareMatrices.ext with left, right
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have entryN := squareMatrices.entry at R, n, N, i, j with *
  have first := matrixSum.entry at R, n, M, N, i, j with *
  have second := matrixSum.entry at R, n, N, M, i, j with *
  rw [first, second]
  ring

theorem matrixSum.assoc (M N P : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires matrixP : P ∈ squareMatrices(R, n)
  shows matrixSum(R, n, matrixSum(R, n, M, N), P) =
    matrixSum(R, n, M, matrixSum(R, n, N, P))
proof
  have sumMN := matrixSum.matrix at R, n, M, N with *
  have sumNP := matrixSum.matrix at R, n, N, P with *
  have left := matrixSum.matrix at R, n, matrixSum(R, n, M, N), P with *
  have right := matrixSum.matrix at R, n, M, matrixSum(R, n, N, P) with *
  apply squareMatrices.ext with left, right
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have entryN := squareMatrices.entry at R, n, N, i, j with *
  have entryP := squareMatrices.entry at R, n, P, i, j with *
  have innerL := matrixSum.entry at R, n, M, N, i, j with *
  have innerR := matrixSum.entry at R, n, N, P, i, j with *
  have outerL := matrixSum.entry at R, n, matrixSum(R, n, M, N), P, i, j with *
  have outerR := matrixSum.entry at R, n, M, matrixSum(R, n, N, P), i, j with *
  rw [outerL, outerR, innerL, innerR]
  ring

theorem matrixSum.zero_left (M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixSum(R, n, zeroMatrix(R, n), M) = M
proof
  have zero := zeroMatrix.matrix at R, n with *
  have sum := matrixSum.matrix at R, n, zeroMatrix(R, n), M with *
  apply squareMatrices.ext with sum, matrix
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have entryZ := zeroMatrix.entry at R, n, i, j with *
  have entry := matrixSum.entry at R, n, zeroMatrix(R, n), M, i, j with *
  rw [entry, entryZ]
  ring

theorem matrixSum.zero_right (M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixSum(R, n, M, zeroMatrix(R, n)) = M
proof
  have zero := zeroMatrix.matrix at R, n with *
  have sum := matrixSum.matrix at R, n, M, zeroMatrix(R, n) with *
  apply squareMatrices.ext with sum, matrix
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have entryZ := zeroMatrix.entry at R, n, i, j with *
  have entry := matrixSum.entry at R, n, M, zeroMatrix(R, n), i, j with *
  rw [entry, entryZ]
  ring

theorem matrixSum.neg_left (M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixSum(R, n, matrixNegative(R, n, M), M) = zeroMatrix(R, n)
proof
  have zero := zeroMatrix.matrix at R, n with *
  have negative := matrixNegative.matrix at R, n, M with *
  have sum := matrixSum.matrix at R, n, matrixNegative(R, n, M), M with *
  apply squareMatrices.ext with sum, zero
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have entryZ := zeroMatrix.entry at R, n, i, j with *
  have entryN := matrixNegative.entry at R, n, M, i, j with *
  have entry := matrixSum.entry at R, n, matrixNegative(R, n, M), M, i, j with *
  rw [entry, entryN, entryZ]
  ring

theorem matrixSum.neg_right (M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixSum(R, n, M, matrixNegative(R, n, M)) = zeroMatrix(R, n)
proof
  have zero := zeroMatrix.matrix at R, n with *
  have negative := matrixNegative.matrix at R, n, M with *
  have sum := matrixSum.matrix at R, n, M, matrixNegative(R, n, M) with *
  apply squareMatrices.ext with sum, zero
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have entryZ := zeroMatrix.entry at R, n, i, j with *
  have entryN := matrixNegative.entry at R, n, M, i, j with *
  have entry := matrixSum.entry at R, n, M, matrixNegative(R, n, M), i, j with *
  rw [entry, entryN, entryZ]
  ring

end AdditiveLaws

section MultiplicativeLaws
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)
notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem matrixProduct.entry_sum (M N i j : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixProduct(R, n, M, N)[i, j] =
    finiteRingSum(n, K, matrixProductWeights(n, K, M, N, i, j))
proof
  have entry := matrixProduct.entry at R, n, M, N, i, j with *
  rw entry
  unfold matrixProductEntry
  rfl

theorem matrixProduct.one_right (M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixProduct(R, n, M, oneMatrix(R, n)) = M
proof
  have parts := CommRing.parts with comm
  have one := oneMatrix.matrix at R, n with *
  have product := matrixProduct.matrix at R, n, M, oneMatrix(R, n) with *
  have shapeM := squareMatrices.membership.forward with matrix
  have shapeOne := squareMatrices.membership.forward with one
  have finite := Finite.natural at n
  apply squareMatrices.ext with product, matrix
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, oneMatrix(R, n), i, j with *
  have selector := coefficientSingle.function at n, R.carrier, R.zero, M[i, j], j with *
  have values : ∀ k ∈ n, matrixProductWeights(n, K, M, oneMatrix(R, n), i, j)(k) =
      coefficientSingle(n, R.carrier, R.zero, M[i, j], j)(k)
    intros k hk
    have entryK := squareMatrices.entry at R, n, M, i, k with *
    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, oneMatrix(R, n), i, j, k with *
    have unit := oneMatrix.entry at R, n, k, j with *
    have alternatives : k = j ∨ k ≠ j by tauto
    cases alternatives with same | different
    . have delta := singleValue.same at R.carrier, R.zero, R.one, j, k with *
      have selected := coefficientSingle.same at n, R.carrier, R.zero, M[i, j], j with *
      rw [weight, unit, delta, same, selected]
      ring
    . have delta := singleValue.other at R.carrier, R.zero, R.one, j, k with *
      have selected := coefficientSingle.other at n, R.carrier, R.zero, M[i, j], j, k with *
      rw [weight, unit, delta, selected]
      ring
  have same := finiteRingSum.congr with values
  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, M[i, j], j with *
  have entry := matrixProduct.entry_sum at R, n, M, oneMatrix(R, n), i, j with *
  cc

theorem matrixProduct.one_left (M : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows matrixProduct(R, n, oneMatrix(R, n), M) = M
proof
  have parts := CommRing.parts with comm
  have one := oneMatrix.matrix at R, n with *
  have product := matrixProduct.matrix at R, n, oneMatrix(R, n), M with *
  have shapeM := squareMatrices.membership.forward with matrix
  have shapeOne := squareMatrices.membership.forward with one
  have finite := Finite.natural at n
  apply squareMatrices.ext with product, matrix
  intros i hi j hj
  have entryM := squareMatrices.entry at R, n, M, i, j with *
  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, oneMatrix(R, n), M, i, j with *
  have selector := coefficientSingle.function at n, R.carrier, R.zero, M[i, j], i with *
  have values : ∀ k ∈ n, matrixProductWeights(n, K, oneMatrix(R, n), M, i, j)(k) =
      coefficientSingle(n, R.carrier, R.zero, M[i, j], i)(k)
    intros k hk
    have entryK := squareMatrices.entry at R, n, M, k, j with *
    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, oneMatrix(R, n), M, i, j, k with *
    have unit := oneMatrix.entry at R, n, i, k with *
    have alternatives : k = i ∨ k ≠ i by tauto
    cases alternatives with same | different
    . have equal : i = k by cc
      have delta := singleValue.same at R.carrier, R.zero, R.one, k, i with *
      have selected := coefficientSingle.same at n, R.carrier, R.zero, M[i, j], i with *
      rw [weight, unit, delta, same, selected]
      ring
    . have reverse : i ≠ k
        intro equal
        apply different
        cc
      have delta := singleValue.other at R.carrier, R.zero, R.one, k, i with *
      have selected := coefficientSingle.other at n, R.carrier, R.zero, M[i, j], i, k with *
      rw [weight, unit, delta, selected]
      ring
  have same := finiteRingSum.congr with values
  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, M[i, j], i with *
  have entry := matrixProduct.entry_sum at R, n, oneMatrix(R, n), M, i, j with *
  cc

theorem matrixProduct.sum_left (M N P : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires matrixP : P ∈ squareMatrices(R, n)
  shows matrixProduct(R, n, matrixSum(R, n, M, N), P) =
    matrixSum(R, n, matrixProduct(R, n, M, P), matrixProduct(R, n, N, P))
proof
  have parts := CommRing.parts with comm
  have sum := matrixSum.matrix at R, n, M, N with *
  have productM := matrixProduct.matrix at R, n, M, P with *
  have productN := matrixProduct.matrix at R, n, N, P with *
  have left := matrixProduct.matrix at R, n, matrixSum(R, n, M, N), P with *
  have right := matrixSum.matrix at R, n, matrixProduct(R, n, M, P),
    matrixProduct(R, n, N, P) with *
  have shapeM := squareMatrices.membership.forward with matrixM
  have shapeN := squareMatrices.membership.forward with matrixN
  have shapeP := squareMatrices.membership.forward with matrixP
  have shapeSum := squareMatrices.membership.forward with sum
  have finite := Finite.natural at n
  have oneIn : R[1] ∈ R := Ring.one_mem with *
  apply squareMatrices.ext with left, right
  intros i hi j hj
  have weightsM := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, P, i, j with *
  have weightsN := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, N, P, i, j with *
  have weightsSum := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, matrixSum(R, n, M, N), P, i, j with *
  have values : ∀ k ∈ n, matrixProductWeights(n, K, matrixSum(R, n, M, N), P, i, j)(k) =
      R[1] * matrixProductWeights(n, K, M, P, i, j)(k) + R[1] * matrixProductWeights(n, K, N, P, i, j)(k)
    intros k hk
    have entryM := squareMatrices.entry at R, n, M, i, k with *
    have entryN := squareMatrices.entry at R, n, N, i, k with *
    have entryP := squareMatrices.entry at R, n, P, k, j with *
    have weightM := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, P, i, j, k with *
    have weightN := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, N, P, i, j, k with *
    have weightSum := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, matrixSum(R, n, M, N), P, i, j, k with *
    have entrySum := matrixSum.entry at R, n, M, N, i, k with *
    rw [weightM, weightN, weightSum, entrySum]
    ring
  have linear := finiteRingSum.linear at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, matrixProductWeights(n, K, M, P, i, j),
    matrixProductWeights(n, K, N, P, i, j),
    matrixProductWeights(n, K, matrixSum(R, n, M, N), P, i, j), R[1], R[1] with *
  have closedM := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, matrixProductWeights(n, K, M, P, i, j) with *
  have closedN := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, matrixProductWeights(n, K, N, P, i, j) with *
  have entryL := matrixProduct.entry_sum at R, n, matrixSum(R, n, M, N), P, i, j with *
  have entryM := matrixProduct.entry_sum at R, n, M, P, i, j with *
  have entryN := matrixProduct.entry_sum at R, n, N, P, i, j with *
  have entryR := matrixSum.entry at R, n, matrixProduct(R, n, M, P),
    matrixProduct(R, n, N, P), i, j with *
  rw [entryL, entryR, entryM, entryN, linear]
  ring

theorem matrixProduct.sum_right (M N P : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires matrixP : P ∈ squareMatrices(R, n)
  shows matrixProduct(R, n, M, matrixSum(R, n, N, P)) =
    matrixSum(R, n, matrixProduct(R, n, M, N), matrixProduct(R, n, M, P))
proof
  have parts := CommRing.parts with comm
  have sum := matrixSum.matrix at R, n, N, P with *
  have productN := matrixProduct.matrix at R, n, M, N with *
  have productP := matrixProduct.matrix at R, n, M, P with *
  have left := matrixProduct.matrix at R, n, M, matrixSum(R, n, N, P) with *
  have right := matrixSum.matrix at R, n, matrixProduct(R, n, M, N),
    matrixProduct(R, n, M, P) with *
  have shapeM := squareMatrices.membership.forward with matrixM
  have shapeN := squareMatrices.membership.forward with matrixN
  have shapeP := squareMatrices.membership.forward with matrixP
  have shapeSum := squareMatrices.membership.forward with sum
  have finite := Finite.natural at n
  have oneIn : R[1] ∈ R := Ring.one_mem with *
  apply squareMatrices.ext with left, right
  intros i hi j hj
  have weightsN := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, N, i, j with *
  have weightsP := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, P, i, j with *
  have weightsSum := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, matrixSum(R, n, N, P), i, j with *
  have values : ∀ k ∈ n, matrixProductWeights(n, K, M, matrixSum(R, n, N, P), i, j)(k) =
      R[1] * matrixProductWeights(n, K, M, N, i, j)(k) + R[1] * matrixProductWeights(n, K, M, P, i, j)(k)
    intros k hk
    have entryM := squareMatrices.entry at R, n, M, i, k with *
    have entryN := squareMatrices.entry at R, n, N, k, j with *
    have entryP := squareMatrices.entry at R, n, P, k, j with *
    have weightN := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, N, i, j, k with *
    have weightP := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, P, i, j, k with *
    have weightSum := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, matrixSum(R, n, N, P), i, j, k with *
    have entrySum := matrixSum.entry at R, n, N, P, k, j with *
    rw [weightN, weightP, weightSum, entrySum]
    ring
  have linear := finiteRingSum.linear at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, matrixProductWeights(n, K, M, N, i, j),
    matrixProductWeights(n, K, M, P, i, j),
    matrixProductWeights(n, K, M, matrixSum(R, n, N, P), i, j), R[1], R[1] with *
  have closedN := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, matrixProductWeights(n, K, M, N, i, j) with *
  have closedP := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, matrixProductWeights(n, K, M, P, i, j) with *
  have entryL := matrixProduct.entry_sum at R, n, M, matrixSum(R, n, N, P), i, j with *
  have entryN := matrixProduct.entry_sum at R, n, M, N, i, j with *
  have entryP := matrixProduct.entry_sum at R, n, M, P, i, j with *
  have entryR := matrixSum.entry at R, n, matrixProduct(R, n, M, N),
    matrixProduct(R, n, M, P), i, j with *
  rw [entryL, entryR, entryN, entryP, linear]
  ring

end MultiplicativeLaws

-- The triple products behind associativity, as a double array over n × n.
defunique assocWeightValue (R : Set, n : Nat, M N P i j q : Set) (a ∈ Ring.carrier(R)) :=
  ∃ k ∈ n, ∃ l ∈ n, q = (k, l) ∧
    a = call2(Ring.mul(R), M[i, l], call2(Ring.mul(R), N[l, k], P[k, j]))
requires comm : CommRing(R)
requires matrixM : M ∈ squareMatrices(R, n)
requires matrixN : N ∈ squareMatrices(R, n)
requires matrixP : P ∈ squareMatrices(R, n)
requires row : i ∈ n
requires column : j ∈ n
requires pair : q ∈ n × n
proof
  obtain ⟨bound, k, hk, l, hl, shape⟩ := product.membership.forward at
    n, n, q with *
  have entryM := squareMatrices.entry at R, n, M, i, l with *
  have entryN := squareMatrices.entry at R, n, N, l, k with *
  have entryP := squareMatrices.entry at R, n, P, k, j with *
  have inner : N[l, k] * P[k, j] ∈ R := Ring.mul_mem with *
  have value : M[i, l] * (N[l, k] * P[k, j]) ∈ R := Ring.mul_mem with *
  refine ⟨M[i, l] * (N[l, k] * P[k, j]), value, k, hk, l, hl, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨k, hk, l, hl, shapeU, valueU⟩ := first
  obtain ⟨a, ha, b, hb, shapeV, valueV⟩ := second
  have equal : (k, l) = (a, b)
    cc
  have coordinates := orderedPair.injective at k, l, a, b with equal
  cc

defgraph assocWeights (R : Set, n : Nat, M N P i j : Set) (q ∈ n × n) : Ring.carrier(R) :=
  assocWeightValue(R, n, M, N, P, i, j, q)
requires comm : CommRing(R)
requires matrixM : M ∈ squareMatrices(R, n)
requires matrixN : N ∈ squareMatrices(R, n)
requires matrixP : P ∈ squareMatrices(R, n)
requires row : i ∈ n
requires column : j ∈ n
proof
  have selected := assocWeightValue.selected at R, n, M, N, P, i, j, q with *
  exact selected.left

theorem assocWeights.pair (R : Set, n : Nat, M N P i j k l : Set)
  requires comm : CommRing(R)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires matrixP : P ∈ squareMatrices(R, n)
  requires row : i ∈ n
  requires column : j ∈ n
  requires hk : k ∈ n
  requires hl : l ∈ n
  shows assocWeights(R, n, M, N, P, i, j)((k, l)) = M[i, l] * (N[l, k] * P[k, j])
proof
  have pair := product.pair at k, l, n, n with *
  have selected := assocWeightValue.selected at R, n, M, N, P, i, j, (k, l) with *
  obtain ⟨a, ha, b, hb, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := assocWeights.value at R, n, M, N, P, i, j, (k, l) with *
  cc

section Associativity
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)
notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem matrixProduct.assoc (M N P : Set)
  requires matrixM : M ∈ squareMatrices(R, n)
  requires matrixN : N ∈ squareMatrices(R, n)
  requires matrixP : P ∈ squareMatrices(R, n)
  shows matrixProduct(R, n, matrixProduct(R, n, M, N), P) =
    matrixProduct(R, n, M, matrixProduct(R, n, N, P))
proof
  have parts := CommRing.parts with comm
  have productMN := matrixProduct.matrix at R, n, M, N with *
  have productNP := matrixProduct.matrix at R, n, N, P with *
  have left := matrixProduct.matrix at R, n, matrixProduct(R, n, M, N), P with *
  have right := matrixProduct.matrix at R, n, M, matrixProduct(R, n, N, P) with *
  have shapeM := squareMatrices.membership.forward with matrixM
  have shapeN := squareMatrices.membership.forward with matrixN
  have shapeP := squareMatrices.membership.forward with matrixP
  have shapeMN := squareMatrices.membership.forward with productMN
  have shapeNP := squareMatrices.membership.forward with productNP
  have finite := Finite.natural at n
  apply squareMatrices.ext with left, right
  intros i hi j hj
  have array := assocWeights.function at R, n, M, N, P, i, j with *
  have transposed := transposedMatrix.function at n, n, R.carrier,
    assocWeights(R, n, M, N, P, i, j) with *
  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, assocWeights(R, n, M, N, P, i, j) with *
  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)) with *
  have weightsL := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, matrixProduct(R, n, M, N), P, i, j with *
  have weightsR := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, M, matrixProduct(R, n, N, P), i, j with *
  have leftRows : ∀ k ∈ n, matrixProductWeights(n, K, matrixProduct(R, n, M, N), P, i, j)(k) =
      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, assocWeights(R, n, M, N, P, i, j))(k)
    intros k hk
    have entryP := squareMatrices.entry at R, n, P, k, j with *
    have rowWeights := finiteRowWeights.function at n, n, R.carrier,
      assocWeights(R, n, M, N, P, i, j), k with *
    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, N, i, k with *
    have scaled : ∀ l ∈ n, finiteRowWeights(n, n, Ring.carrier(R), assocWeights(R, n, M, N, P, i, j), k)(l) =
        P[k, j] * matrixProductWeights(n, K, M, N, i, k)(l)
      intros l hl
      have entryM := squareMatrices.entry at R, n, M, i, l with *
      have entryN := squareMatrices.entry at R, n, N, l, k with *
      have rowWeight := finiteRowWeights.value at n, n, R.carrier,
        assocWeights(R, n, M, N, P, i, j), k, l with *
      have cell := assocWeights.pair at R, n, M, N, P, i, j, k, l with *
      have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
        R.neg, R.mul, R.one, M, N, i, k, l with *
      rw [rowWeight, cell, weight]
      ring
    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, matrixProductWeights(n, K, M, N, i, k),
      finiteRowWeights(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j), k), P[k, j] with *
    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, assocWeights(R, n, M, N, P, i, j), k with *
    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, matrixProduct(R, n, M, N), P, i, j, k with *
    have entryMN := matrixProduct.entry_sum at R, n, M, N, i, k with *
    have closed := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, matrixProductWeights(n, K, M, N, i, k) with *
    rw [weight, rowSum, scale, entryMN]
    ring
  have rightRows : ∀ l ∈ n, matrixProductWeights(n, K, M, matrixProduct(R, n, N, P), i, j)(l) =
      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, transposedMatrix(n, n, Ring.carrier(R), assocWeights(R, n, M, N, P, i, j)))(l)
    intros l hl
    have entryM := squareMatrices.entry at R, n, M, i, l with *
    have rowWeights := finiteRowWeights.function at n, n, R.carrier,
      transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l with *
    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, N, P, l, j with *
    have scaled : ∀ k ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), assocWeights(R, n, M, N, P, i, j)), l)(k) =
        M[i, l] * matrixProductWeights(n, K, N, P, l, j)(k)
      intros k hk
      have entryN := squareMatrices.entry at R, n, N, l, k with *
      have entryP := squareMatrices.entry at R, n, P, k, j with *
      have rowWeight := finiteRowWeights.value at n, n, R.carrier,
        transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l, k with *
      have swap := transposedMatrix.pair at n, n, R.carrier,
        assocWeights(R, n, M, N, P, i, j), k, l with *
      have cell := assocWeights.pair at R, n, M, N, P, i, j, k, l with *
      have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
        R.neg, R.mul, R.one, N, P, l, j, k with *
      rw [rowWeight, swap, cell, weight]
      ring
    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, matrixProductWeights(n, K, N, P, l, j),
      finiteRowWeights(n, n, R.carrier, transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l), M[i, l] with *
    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l with *
    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, M, matrixProduct(R, n, N, P), i, j, l with *
    have entryNP := matrixProduct.entry_sum at R, n, N, P, l, j with *
    rw [weight, rowSum, scale, entryNP]
    rfl
  have sameL := finiteRingSum.congr with leftRows
  have sameR := finiteRingSum.congr with rightRows
  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, assocWeights(R, n, M, N, P, i, j) with *
  have entryL := matrixProduct.entry_sum at R, n, matrixProduct(R, n, M, N), P, i, j with *
  have entryR := matrixProduct.entry_sum at R, n, M, matrixProduct(R, n, N, P), i, j with *
  unfold finiteDoubleSum at interchange
  cc

end Associativity

-- The ring laws over separate pieces, then the ring instance.
section Instances
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)
notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem matrixRing.engine
  shows IsRing(squareMatrices(R, n), matrixAddition(R, n), zeroMatrix(R, n),
    matrixNegation(R, n), matrixMultiplication(R, n), oneMatrix(R, n))
proof
  have addMagma : IsMagma(squareMatrices(R, n), matrixAddition(R, n))
    exact matrixAddition.function at R, n with *
  have mulMagma : IsMagma(squareMatrices(R, n), matrixMultiplication(R, n))
    exact matrixMultiplication.function at R, n with *
  have negF := matrixNegation.function at R, n with *
  have zero := zeroMatrix.matrix at R, n with *
  have one := oneMatrix.matrix at R, n with *
  have addAssoc : Associative(squareMatrices(R, n), matrixAddition(R, n))
    intros M hM N hN P hP
    have sumMN := matrixSum.matrix at R, n, M, N with *
    have sumNP := matrixSum.matrix at R, n, N, P with *
    have first := matrixAddition.apply at R, n, M, N with *
    have second := matrixAddition.apply at R, n, matrixSum(R, n, M, N), P with *
    have third := matrixAddition.apply at R, n, N, P with *
    have fourth := matrixAddition.apply at R, n, M, matrixSum(R, n, N, P) with *
    have assoc := matrixSum.assoc at R, n, M, N, P with *
    cc
  have addComm : Commutative(squareMatrices(R, n), matrixAddition(R, n))
    intros M hM N hN
    have first := matrixAddition.apply at R, n, M, N with *
    have second := matrixAddition.apply at R, n, N, M with *
    have swap := matrixSum.comm at R, n, M, N with *
    cc
  have addUnit : Identity(squareMatrices(R, n), matrixAddition(R, n), zeroMatrix(R, n))
    refine ⟨zero, ?_⟩
    intros M hM
    have first := matrixAddition.apply at R, n, zeroMatrix(R, n), M with *
    have second := matrixAddition.apply at R, n, M, zeroMatrix(R, n) with *
    have left := matrixSum.zero_left at R, n, M with *
    have right := matrixSum.zero_right at R, n, M with *
    constructor
    . cc
    . cc
  have addInverse : Inverse(squareMatrices(R, n), matrixAddition(R, n),
      zeroMatrix(R, n), matrixNegation(R, n))
    refine ⟨negF, ?_⟩
    intros M hM
    have negative := matrixNegative.matrix at R, n, M with *
    have value := matrixNegation.value at R, n, M with *
    have first := matrixAddition.apply at R, n, matrixNegative(R, n, M), M with *
    have second := matrixAddition.apply at R, n, M, matrixNegative(R, n, M) with *
    have left := matrixSum.neg_left at R, n, M with *
    have right := matrixSum.neg_right at R, n, M with *
    constructor
    . cc
    . cc
  have mulAssoc : Associative(squareMatrices(R, n), matrixMultiplication(R, n))
    intros M hM N hN P hP
    have productMN := matrixProduct.matrix at R, n, M, N with *
    have productNP := matrixProduct.matrix at R, n, N, P with *
    have first := matrixMultiplication.apply at R, n, M, N with *
    have second := matrixMultiplication.apply at R, n, matrixProduct(R, n, M, N), P with *
    have third := matrixMultiplication.apply at R, n, N, P with *
    have fourth := matrixMultiplication.apply at R, n, M, matrixProduct(R, n, N, P) with *
    have assoc := matrixProduct.assoc at R, n, M, N, P with *
    cc
  have mulUnit : Identity(squareMatrices(R, n), matrixMultiplication(R, n), oneMatrix(R, n))
    refine ⟨one, ?_⟩
    intros M hM
    have first := matrixMultiplication.apply at R, n, oneMatrix(R, n), M with *
    have second := matrixMultiplication.apply at R, n, M, oneMatrix(R, n) with *
    have left := matrixProduct.one_left at R, n, M with *
    have right := matrixProduct.one_right at R, n, M with *
    constructor
    . cc
    . cc
  have distributive : Distributive(squareMatrices(R, n), matrixAddition(R, n),
      matrixMultiplication(R, n))
    intros M hM N hN P hP
    have sumNP := matrixSum.matrix at R, n, N, P with *
    have sumMN := matrixSum.matrix at R, n, M, N with *
    have productMN := matrixProduct.matrix at R, n, M, N with *
    have productMP := matrixProduct.matrix at R, n, M, P with *
    have productNP := matrixProduct.matrix at R, n, N, P with *
    have addNP := matrixAddition.apply at R, n, N, P with *
    have addMN := matrixAddition.apply at R, n, M, N with *
    have mulLeft := matrixMultiplication.apply at R, n, M, matrixSum(R, n, N, P) with *
    have mulRight := matrixMultiplication.apply at R, n, matrixSum(R, n, M, N), P with *
    have mulMN := matrixMultiplication.apply at R, n, M, N with *
    have mulMP := matrixMultiplication.apply at R, n, M, P with *
    have mulNP := matrixMultiplication.apply at R, n, N, P with *
    have addLeft := matrixAddition.apply at R, n, matrixProduct(R, n, M, N),
      matrixProduct(R, n, M, P) with *
    have addRight := matrixAddition.apply at R, n, matrixProduct(R, n, M, P),
      matrixProduct(R, n, N, P) with *
    have left := matrixProduct.sum_right at R, n, M, N, P with *
    have right := matrixProduct.sum_left at R, n, M, N, P with *
    constructor
    . cc
    . cc
  unfold IsRing
  simp [IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]

instance matrixRing.ring
  shows Ring(matrixRing(R, n))
proof
  have engine := matrixRing.engine at R, n with comm
  unfold matrixRing
  exact Ring.of_parts with engine

end Instances

-- A matrix as a guard: (M : R ^ n × n) is Matrix(M, R, n, n), membership
-- in the matrix ring, opened to M ∈ Ring.carrier(matrixRing(R, n))
-- wherever local evidence is consulted, so (M N : R ^ n × n) carry
-- M + N, M * N, -M, and the constants matrixRing(R, n)[0] and
-- matrixRing(R, n)[1]; det(M) and adj(M) are the determinant and the
-- adjugate over R. The shape m × n is written for the guard's sake: this
-- layer has square matrices only, and Matrix(M, R, m, n) requires m = n.
predicate Matrix (M R m n : Set) := m = n ∧ M ∈ Ring.carrier(matrixRing(R, n))
notation guard "_ : _ ^ _ × _" => Matrix
notation function "det(M)" => determinant(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M) via hypothesis Matrix(M, R, m, n)
notation function "adj(M)" => adjugate(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M) via hypothesis Matrix(M, R, m, n)
notation infixl 60 "+" => call2(Ring.add(matrixRing(R, n)), _, _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))
notation infixl 70 "*" => call2(Ring.mul(matrixRing(R, n)), _, _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))
notation prefix 75 "-" => apply(Ring.neg(matrixRing(R, n)), _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))
notation infixl 60 "-" => Ring.sub(matrixRing(R, n), _, _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))

theorem Matrix.of_mem (M R n : Set)
  requires member : M ∈ Ring.carrier(matrixRing(R, n))
  shows M : R ^ n × n
proof
  unfold Matrix
  exact ⟨rfl, member⟩

theorem Matrix.mem_ring (M R n : Set)
  requires matrix : M : R ^ n × n
  shows M ∈ Ring.carrier(matrixRing(R, n))
proof
  assumption

theorem Matrix.square (M R n : Set)
  requires matrix : M : R ^ n × n
  shows M ∈ squareMatrices(R, n)
proof
  have member : M ∈ Ring.carrier(matrixRing(R, n)) by assumption
  rw matrixRing.carrierOf at member
  exact member

theorem Matrix.of_square (M R n : Set)
  requires matrix : M ∈ squareMatrices(R, n)
  shows M : R ^ n × n
proof
  unfold Matrix
  refine ⟨rfl, ?_⟩
  rw matrixRing.carrierOf
  exact matrix

theorem Matrix.function (M R n : Set)
  requires matrix : M : R ^ n × n
  shows M : n × n → Ring.carrier(R)
proof
  have square := Matrix.square with matrix
  exact squareMatrices.function with square

theorem Matrix.of_function (M R n : Set)
  requires function : M : n × n → Ring.carrier(R)
  shows M : R ^ n × n
proof
  have square := squareMatrices.of_function with function
  exact Matrix.of_square with square

theorem Matrix.entry (M R n i j : Set)
  requires matrix : M : R ^ n × n
  requires row : i ∈ n
  requires column : j ∈ n
  shows M[i, j] ∈ Ring.carrier(R)
proof
  have function := Matrix.function with matrix
  have pair := product.pair at i, j, n, n with *
  exact FunctionBetween.apply_closed with function, pair

theorem Matrix.ext (M N R n : Set)
  requires matrixM : M : R ^ n × n
  requires matrixN : N : R ^ n × n
  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]
  shows M = N
proof
  have functionM := Matrix.function with matrixM
  have functionN := Matrix.function with matrixN
  have values : ∀ p ∈ n × n, M(p) = N(p)
    intros p hp
    obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with hp
    rw shape
    exact entries with i, hi, j, hj
  exact FunctionBetween.ext with functionM, functionN, values