Grace/Cumulus/Geometry/Absorption/Triples.g17

Open in Workbench Download source

Imports

Rotation.Vectors · Set.Tuple

Declarations

Source

1-- Explicit 3 × 3 real matrices: triples as functions on 3, the matrix2-- matrix3of(a, b, c, d, e, f, g, h, k) with the given rows as an element of3-- matrixRing(realRing, 3), its entries, and the entries of a product of4-- two 3 × 3 real matrices as sums of three terms5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Geometry.Absorption.Triples11import Rotation.Vectors12import Set.Tuple1314-- The index set 3 = {0, 1, 2}, as Rotation/Vectors states it.15theorem threeIndex.cases (i : Set)16  requires member : i ∈ 317  shows i = 0 ∨ i = 1 ∨ i = 218proof19  exact index.cases with member2021theorem threeIndex.zero_ne_one22  shows (0:N) ≠ (1:N)23proof24  exact index.zero_ne_one2526theorem threeIndex.zero_ne_two27  shows (0:N) ≠ (2:N)28proof29  exact index.zero_ne_two3031theorem threeIndex.one_ne_two32  shows (1:N) ≠ (2:N)33proof34  exact index.one_ne_two3536-- The operations of realRing read as the real operations.37theorem realRing.call_add (x y : Set)38  shows call2(Ring.add(realRing), x, y) = call2(realAdd, x, y)39proof40  simp [realRing, Ring.mk.add]4142theorem realRing.call_mul (x y : Set)43  shows call2(Ring.mul(realRing), x, y) = call2(realMul, x, y)44proof45  simp [realRing, Ring.mk.mul]4647theorem realRing.zero_eq48  shows Ring.zero(realRing) = realZero49proof50  simp [realRing, Ring.mk.zero]5152theorem realRing.one_eq53  shows Ring.one(realRing) = realOne54proof55  simp [realRing, Ring.mk.one]5657-- A finite ring sum over the index set 3 is the sum of its three terms.58theorem finiteRingSum.over_three (A add zero neg mul one w : Set)59  requires ring : IsCommRing(A, add, zero, neg, mul, one)60  requires weights : w : 3 → A61  shows finiteRingSum(3, A, add, zero, neg, mul, one, w) =62    call2(add, call2(add, call2(add, zero, w(0)), w(1)), w(2))63proof64  have enumeration := identity.bijective at 365  have indexed := finiteRingSum.enumeration at 3, A, add, zero, neg, mul, one,66    w, identity(3), 3 with ring, weights, enumeration67  have zeroIn : 0 ∈ 3 by typecheck68  have oneIn : 1 ∈ 3 by typecheck69  have twoIn : 2 ∈ 3 by typecheck70  have at0 := identity.apply at 0, 3 with zeroIn71  have at1 := identity.apply at 1, 3 with oneIn72  have at2 := identity.apply at 2, 3 with twoIn73  rw indexed74  simp [indexedRingSum, at0, at1, at2]7576-- A triple (a, b, c) as the function on 3 with those values.77defunique tripleValue (A a b c j : Set) (v ∈ A) :=78  (j = 0 ∧ v = a) ∨ (j = 1 ∧ v = b) ∨ (j = 2 ∧ v = c)79requires aIn : a ∈ A80requires bIn : b ∈ A81requires cIn : c ∈ A82requires index : j ∈ 383proof84  have alternatives := threeIndex.cases with index85  rcases alternatives with first | second | third86  . refine ⟨a, aIn, ?_⟩87    left88    exact ⟨first, rfl⟩89  . refine ⟨b, bIn, ?_⟩90    right91    left92    exact ⟨second, rfl⟩93  . refine ⟨c, cIn, ?_⟩94    right95    right96    exact ⟨third, rfl⟩97uniqueness98  intros u hu first v hv second99  have d01 := threeIndex.zero_ne_one100  have d02 := threeIndex.zero_ne_two101  have d12 := threeIndex.one_ne_two102  rcases first with firstZero | firstOne | firstTwo103  . obtain ⟨jZero, ua⟩ := firstZero104    rcases second with secondZero | secondOne | secondTwo105    . obtain ⟨kZero, va⟩ := secondZero106      cc107    . obtain ⟨kOne, vb⟩ := secondOne108      exfalso109      apply d01110      cc111    . obtain ⟨kTwo, vc⟩ := secondTwo112      exfalso113      apply d02114      cc115  . obtain ⟨jOne, ub⟩ := firstOne116    rcases second with secondZero | secondOne | secondTwo117    . obtain ⟨kZero, va⟩ := secondZero118      exfalso119      apply d01120      cc121    . obtain ⟨kOne, vb⟩ := secondOne122      cc123    . obtain ⟨kTwo, vc⟩ := secondTwo124      exfalso125      apply d12126      cc127  . obtain ⟨jTwo, uc⟩ := firstTwo128    rcases second with secondZero | secondOne | secondTwo129    . obtain ⟨kZero, va⟩ := secondZero130      exfalso131      apply d02132      cc133    . obtain ⟨kOne, vb⟩ := secondOne134      exfalso135      apply d12136      cc137    . obtain ⟨kTwo, vc⟩ := secondTwo138      cc139140defgraph triple (A a b c : Set) (j ∈ 3) : A := tripleValue(A, a, b, c, j)141requires aIn : a ∈ A142requires bIn : b ∈ A143requires cIn : c ∈ A144proof145  have selected := tripleValue.selected at A, a, b, c, j with *146  exact selected.left147148section TripleValues149variable (A a b c : Set)150hypothesis aIn : a ∈ A151hypothesis bIn : b ∈ A152hypothesis cIn : c ∈ A153154theorem triple.zero155  shows triple(A, a, b, c)(0) = a156proof157  have zeroIn : 0 ∈ 3 by typecheck158  have value := triple.value at A, a, b, c, 0 with *159  have selected := tripleValue.selected at A, a, b, c, 0 with *160  have d01 := threeIndex.zero_ne_one161  have d02 := threeIndex.zero_ne_two162  rw value163  obtain ⟨inA, property⟩ := selected164  rcases property with same | badOne | badTwo165  . exact same.right166  . exfalso167    exact d01 with badOne.left168  . exfalso169    exact d02 with badTwo.left170171theorem triple.one172  shows triple(A, a, b, c)(1) = b173proof174  have oneIn : 1 ∈ 3 by typecheck175  have value := triple.value at A, a, b, c, 1 with *176  have selected := tripleValue.selected at A, a, b, c, 1 with *177  have d01 := threeIndex.zero_ne_one178  have d12 := threeIndex.one_ne_two179  rw value180  obtain ⟨inA, property⟩ := selected181  rcases property with badZero | same | badTwo182  . exfalso183    have flipped := badZero.left184    symm at flipped185    exact d01 with flipped186  . exact same.right187  . exfalso188    exact d12 with badTwo.left189190theorem triple.two191  shows triple(A, a, b, c)(2) = c192proof193  have twoIn : 2 ∈ 3 by typecheck194  have value := triple.value at A, a, b, c, 2 with *195  have selected := tripleValue.selected at A, a, b, c, 2 with *196  have d02 := threeIndex.zero_ne_two197  have d12 := threeIndex.one_ne_two198  rw value199  obtain ⟨inA, property⟩ := selected200  rcases property with badZero | badOne | same201  . exfalso202    have flipped := badZero.left203    symm at flipped204    exact d02 with flipped205  . exfalso206    have flipped := badOne.left207    symm at flipped208    exact d12 with flipped209  . exact same.right210211end TripleValues212213-- The 3 × 3 matrix with the three given rows, rows being functions 3 → ℝ.214defgraph matrix3 (r0 r1 r2 : Set) (p ∈ 3 × 3) : ℝ :=215  triple(functionSpace(3, ℝ), r0, r1, r2)(fst(p))(snd(p))216requires row0 : r0 ∈ functionSpace(3, ℝ)217requires row1 : r1 ∈ functionSpace(3, ℝ)218requires row2 : r2 ∈ functionSpace(3, ℝ)219proof220  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member221  have rows := triple.function at functionSpace(3, ℝ), r0, r1, r2 with *222  rw [shape, fst.pair, snd.pair]223  have rowIn := FunctionBetween.apply_closed with rows, hi224  have rowFunction := functionSpace.mem_iff.forward with rowIn225  exact FunctionBetween.apply_closed with rowFunction, hj226227section MatrixRows228variable (r0 r1 r2 : Set)229hypothesis row0 : r0 ∈ functionSpace(3, ℝ)230hypothesis row1 : r1 ∈ functionSpace(3, ℝ)231hypothesis row2 : r2 ∈ functionSpace(3, ℝ)232233theorem matrix3.entry (i j : Set)234  requires hi : i ∈ 3235  requires hj : j ∈ 3236  shows matrix3(r0, r1, r2)[i, j] = triple(functionSpace(3, ℝ), r0, r1, r2)(i)(j)237proof238  have pair := product.pair at i, j, 3, 3 with *239  have value := matrix3.value at r0, r1, r2, (i, j) with *240  rw [value, fst.pair, snd.pair]241  rfl242243theorem matrix3.square244  shows matrix3(r0, r1, r2) ∈ squareMatrices(realRing, 3)245proof246  have function := matrix3.function at r0, r1, r2 with *247  rw ← realRing.carrierOf at function248  exact squareMatrices.of_function with function249250instance matrix3.matrix251  shows matrix3(r0, r1, r2) : realRing ^ 3 × 3252proof253  have square : matrix3(r0, r1, r2) ∈ squareMatrices(realRing, 3) := matrix3.square with *254  exact Matrix.of_square with square255256end MatrixRows257258-- A row of three reals, and the matrix with nine given real entries.259def row3 (a b c : Set) : Set := triple(ℝ, a, b, c)260def matrix3of (a b c d e f g h k : Set) : Set :=261  matrix3(row3(a, b, c), row3(d, e, f), row3(g, h, k))262263theorem row3.graph (a b c : Set)264  shows row3(a, b, c) = triple(ℝ, a, b, c)265proof266  simp [row3]267268theorem matrix3of.graph (a b c d e f g h k : Set)269  shows matrix3of(a, b, c, d, e, f, g, h, k) =270    matrix3(row3(a, b, c), row3(d, e, f), row3(g, h, k))271proof272  simp [matrix3of]273274instance row3.member (a b c : Real)275  shows row3(a, b, c) ∈ functionSpace(3, ℝ)276proof277  have function := triple.function at ℝ, a, b, c with *278  rw row3.graph279  exact functionSpace.mem_iff.backward with function280281section Entries282variable (a b c d e f g h k : Real)283284instance matrix3of.matrix285  shows matrix3of(a, b, c, d, e, f, g, h, k) : realRing ^ 3 × 3286proof287  rw matrix3of.graph288  exact matrix3.matrix with *289290theorem matrix3of.entry (i j : Set)291  requires hi : i ∈ 3292  requires hj : j ∈ 3293  shows matrix3of(a, b, c, d, e, f, g, h, k)[i, j] =294    triple(functionSpace(3, ℝ), row3(a, b, c), row3(d, e, f), row3(g, h, k))(i)(j)295proof296  rw matrix3of.graph297  exact matrix3.entry with *298299theorem matrix3of.entry00300  shows matrix3of(a, b, c, d, e, f, g, h, k)[0, 0] = a301proof302  have zeroIn : 0 ∈ 3 by typecheck303  rw [matrix3of.entry, triple.zero, row3.graph, triple.zero]304  rfl305306theorem matrix3of.entry01307  shows matrix3of(a, b, c, d, e, f, g, h, k)[0, 1] = b308proof309  have zeroIn : 0 ∈ 3 by typecheck310  have oneIn : 1 ∈ 3 by typecheck311  rw [matrix3of.entry, triple.zero, row3.graph, triple.one]312  rfl313314theorem matrix3of.entry02315  shows matrix3of(a, b, c, d, e, f, g, h, k)[0, 2] = c316proof317  have zeroIn : 0 ∈ 3 by typecheck318  have twoIn : 2 ∈ 3 by typecheck319  rw [matrix3of.entry, triple.zero, row3.graph, triple.two]320  rfl321322theorem matrix3of.entry10323  shows matrix3of(a, b, c, d, e, f, g, h, k)[1, 0] = d324proof325  have zeroIn : 0 ∈ 3 by typecheck326  have oneIn : 1 ∈ 3 by typecheck327  rw [matrix3of.entry, triple.one, row3.graph, triple.zero]328  rfl329330theorem matrix3of.entry11331  shows matrix3of(a, b, c, d, e, f, g, h, k)[1, 1] = e332proof333  have oneIn : 1 ∈ 3 by typecheck334  rw [matrix3of.entry, triple.one, row3.graph, triple.one]335  rfl336337theorem matrix3of.entry12338  shows matrix3of(a, b, c, d, e, f, g, h, k)[1, 2] = f339proof340  have oneIn : 1 ∈ 3 by typecheck341  have twoIn : 2 ∈ 3 by typecheck342  rw [matrix3of.entry, triple.one, row3.graph, triple.two]343  rfl344345theorem matrix3of.entry20346  shows matrix3of(a, b, c, d, e, f, g, h, k)[2, 0] = g347proof348  have zeroIn : 0 ∈ 3 by typecheck349  have twoIn : 2 ∈ 3 by typecheck350  rw [matrix3of.entry, triple.two, row3.graph, triple.zero]351  rfl352353theorem matrix3of.entry21354  shows matrix3of(a, b, c, d, e, f, g, h, k)[2, 1] = h355proof356  have oneIn : 1 ∈ 3 by typecheck357  have twoIn : 2 ∈ 3 by typecheck358  rw [matrix3of.entry, triple.two, row3.graph, triple.one]359  rfl360361theorem matrix3of.entry22362  shows matrix3of(a, b, c, d, e, f, g, h, k)[2, 2] = k363proof364  have twoIn : 2 ∈ 3 by typecheck365  rw [matrix3of.entry, triple.two, row3.graph, triple.two]366  rfl367368end Entries369370-- Entries of 3 × 3 real matrices are real, and a product entry is the371-- sum of three products.372section Products373variable (M N : realRing ^ 3 × 3)374375instance matrix3.entry_real (i j : Set)376  requires hi : i ∈ 3377  requires hj : j ∈ 3378  shows M[i, j] ∈ ℝ379proof380  have entry := Matrix.entry at M, realRing, 3, i, j with *381  rw realRing.carrierOf at entry382  exact entry383384theorem matrix3.mul_entry (i j : Set)385  requires hi : i ∈ 3386  requires hj : j ∈ 3387  shows call2(Ring.mul(matrixRing(realRing, 3)), M, N)[i, j] =388    (M[i, 0]:R) * (N[0, j]:R) + (M[i, 1]:R) * (N[1, j]:R) + (M[i, 2]:R) * (N[2, j]:R)389proof390  have comm := realRing.comm_ring391  have parts := CommRing.parts with comm392  have squareM := Matrix.square at M, realRing, 3 with assumption393  have squareN := Matrix.square at N, realRing, 3 with assumption394  have shapeM := squareMatrices.membership.forward with squareM395  have shapeN := squareMatrices.membership.forward with squareN396  have entry := matrixRing.mul_entry at realRing, 3, M, N, i, j with *397  have weights := matrixProductWeights.function at 3, Ring.carrier(realRing),398    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),399    Ring.mul(realRing), Ring.one(realRing), M, N, i, j with *400  have zeroIn : 0 ∈ 3 by typecheck401  have oneIn : 1 ∈ 3 by typecheck402  have twoIn : 2 ∈ 3 by typecheck403  have w0 := matrixProductWeights.value at 3, Ring.carrier(realRing),404    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),405    Ring.mul(realRing), Ring.one(realRing), M, N, i, j, 0 with *406  have w1 := matrixProductWeights.value at 3, Ring.carrier(realRing),407    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),408    Ring.mul(realRing), Ring.one(realRing), M, N, i, j, 1 with *409  have w2 := matrixProductWeights.value at 3, Ring.carrier(realRing),410    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing),411    Ring.mul(realRing), Ring.one(realRing), M, N, i, j, 2 with *412  have sum := finiteRingSum.over_three with parts, weights413  rw entry414  simp [matrixProductEntry]415  rw [realRing.call_add, realRing.call_add, realRing.call_add,416    realRing.call_mul, realRing.call_mul, realRing.call_mul, realRing.zero_eq]417  have m0 : M[i, 0] ∈ ℝ := matrix3.entry_real with *418  have m1 : M[i, 1] ∈ ℝ := matrix3.entry_real with *419  have m2 : M[i, 2] ∈ ℝ := matrix3.entry_real with *420  have n0 : N[0, j] ∈ ℝ := matrix3.entry_real with *421  have n1 : N[1, j] ∈ ℝ := matrix3.entry_real with *422  have n2 : N[2, j] ∈ ℝ := matrix3.entry_real with *423  ring424425instance matrix3.mul_matrix426  shows call2(Ring.mul(matrixRing(realRing, 3)), M, N) : realRing ^ 3 × 3427proof428  have comm := realRing.comm_ring429  have ring := matrixRing.ring at realRing, 3 with comm430  have mIn : M ∈ Ring.carrier(matrixRing(realRing, 3)) := Matrix.mem_ring with assumption431  have nIn : N ∈ Ring.carrier(matrixRing(realRing, 3)) := Matrix.mem_ring with assumption432  have productIn : call2(Ring.mul(matrixRing(realRing, 3)), M, N) ∈ Ring.carrier(matrixRing(realRing, 3)) :=433    Ring.mul_mem with *434  exact Matrix.of_mem with productIn435436end Products437438-- The 3 × 3 real matrices as a type: Matrix3(M) is the guard439-- M : realRing ^ 3 × 3, and M * N on such matrices is matrixMul3(M, N),440-- the product of the matrix ring.441class Matrix3 (M : Set) := Matrix(M, realRing, 3, 3)442def matrixMul3 (M N : Set) : Set := call2(Ring.mul(matrixRing(realRing, 3)), M, N)443notation infixl 70 "*" => matrixMul3 for Matrix3444445theorem matrixMul3.graph (M N : Set)446  shows matrixMul3(M, N) = call2(Ring.mul(matrixRing(realRing, 3)), M, N)447proof448  simp [matrixMul3]449450instance Matrix3.of_matrix (M : Set)451  requires matrix : M : realRing ^ 3 × 3452  shows Matrix3(M)453proof454  exact matrix455456theorem Matrix3.matrix (M : Matrix3)457  shows M : realRing ^ 3 × 3458proof459  have typed : Matrix3(M) by assumption460  unfold Matrix3 at typed461  exact typed462463instance Matrix3.mul (M N : Matrix3)464  shows Matrix3(matrixMul3(M, N))465proof466  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *467  have matrixN : N : realRing ^ 3 × 3 := Matrix3.matrix with *468  have product : call2(Ring.mul(matrixRing(realRing, 3)), M, N) : realRing ^ 3 × 3 :=469    matrix3.mul_matrix with *470  unfold Matrix3471  rw matrixMul3.graph472  exact product473474instance Matrix3.entry_real (M : Matrix3) (i j : Set)475  requires hi : i ∈ 3476  requires hj : j ∈ 3477  shows M[i, j] ∈ ℝ478proof479  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *480  exact matrix3.entry_real with *481482theorem Matrix3.mul_entry (M N : Matrix3) (i j : Set)483  requires hi : i ∈ 3484  requires hj : j ∈ 3485  shows matrixMul3(M, N)[i, j] =486    (M[i, 0]:R) * (N[0, j]:R) + (M[i, 1]:R) * (N[1, j]:R) + (M[i, 2]:R) * (N[2, j]:R)487proof488  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *489  have matrixN : N : realRing ^ 3 × 3 := Matrix3.matrix with *490  rw matrixMul3.graph491  exact matrix3.mul_entry with *492493instance Matrix3.one494  shows Matrix3(Ring.one(matrixRing(realRing, 3)))495proof496  have comm := realRing.comm_ring497  have ring := matrixRing.ring at realRing, 3 with comm498  have oneIn : Ring.one(matrixRing(realRing, 3)) ∈ Ring.carrier(matrixRing(realRing, 3)) :=499    Ring.one_mem with *500  unfold Matrix3501  exact Matrix.of_mem with oneIn502503theorem Matrix3.ext (M N : Matrix3)504  requires entries : ∀ i ∈ 3, ∀ j ∈ 3, M[i, j] = N[i, j]505  shows M = N506proof507  have comm := realRing.comm_ring508  have matrixM : M : realRing ^ 3 × 3 := Matrix3.matrix with *509  have matrixN : N : realRing ^ 3 × 3 := Matrix3.matrix with *510  exact matrixRing.ext with entries511512-- Two explicit matrices with the same entries are equal, the product of513-- two explicit matrices, and the identity matrix as an explicit matrix.514theorem matrix3of.congr (a b c d e f g h k l m n o p q r s u : Real)515  requires e00 : a = l516  requires e01 : b = m517  requires e02 : c = n518  requires e10 : d = o519  requires e11 : e = p520  requires e12 : f = q521  requires e20 : g = r522  requires e21 : h = s523  requires e22 : k = u524  shows matrix3of(a, b, c, d, e, f, g, h, k) = matrix3of(l, m, n, o, p, q, r, s, u)525proof526  rw [e00, e01, e02, e10, e11, e12, e20, e21, e22]527  rfl528529tactic matrix3of_entries := simp [matrix3of.entry00, matrix3of.entry01, matrix3of.entry02, matrix3of.entry10, matrix3of.entry11, matrix3of.entry12, matrix3of.entry20, matrix3of.entry21, matrix3of.entry22]530531theorem matrix3of.mul (a b c d e f g h k l m n o p q r s u : Real)532  shows matrixMul3(matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u)) =533    matrix3of(a * l + b * o + c * r, a * m + b * p + c * s, a * n + b * q + c * u,534      d * l + e * o + f * r, d * m + e * p + f * s, d * n + e * q + f * u,535      g * l + h * o + k * r, g * m + h * p + k * s, g * n + h * q + k * u)536proof537  have leftMatrix : matrix3of(a, b, c, d, e, f, g, h, k) : realRing ^ 3 × 3 :=538    matrix3of.matrix with *539  have rightMatrix : matrix3of(l, m, n, o, p, q, r, s, u) : realRing ^ 3 × 3 :=540    matrix3of.matrix with *541  have leftTyped : Matrix3(matrix3of(a, b, c, d, e, f, g, h, k)) :=542    Matrix3.of_matrix with leftMatrix543  have rightTyped : Matrix3(matrix3of(l, m, n, o, p, q, r, s, u)) :=544    Matrix3.of_matrix with rightMatrix545  have entries : ∀ i ∈ 3, ∀ j ∈ 3,546      matrixMul3(matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u))[i, j] =547      matrix3of(a * l + b * o + c * r, a * m + b * p + c * s, a * n + b * q + c * u,548        d * l + e * o + f * r, d * m + e * p + f * s, d * n + e * q + f * u,549        g * l + h * o + k * r, g * m + h * p + k * s, g * n + h * q + k * u)[i, j]550    intros i hi j hj551    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, hj552    rw entry553    have rows := threeIndex.cases with hi554    have columns := threeIndex.cases with hj555    rcases rows with rowZero | rowOne | rowTwo556    . rcases columns with columnZero | columnOne | columnTwo557      . rw [rowZero, columnZero]558        matrix3of_entries559      . rw [rowZero, columnOne]560        matrix3of_entries561      . rw [rowZero, columnTwo]562        matrix3of_entries563    . rcases columns with columnZero | columnOne | columnTwo564      . rw [rowOne, columnZero]565        matrix3of_entries566      . rw [rowOne, columnOne]567        matrix3of_entries568      . rw [rowOne, columnTwo]569        matrix3of_entries570    . rcases columns with columnZero | columnOne | columnTwo571      . rw [rowTwo, columnZero]572        matrix3of_entries573      . rw [rowTwo, columnOne]574        matrix3of_entries575      . rw [rowTwo, columnTwo]576        matrix3of_entries577  have e00 : a * l + b * o + c * r ∈ ℝ by typecheck578  have e01 : a * m + b * p + c * s ∈ ℝ by typecheck579  have e02 : a * n + b * q + c * u ∈ ℝ by typecheck580  have e10 : d * l + e * o + f * r ∈ ℝ by typecheck581  have e11 : d * m + e * p + f * s ∈ ℝ by typecheck582  have e12 : d * n + e * q + f * u ∈ ℝ by typecheck583  have e20 : g * l + h * o + k * r ∈ ℝ by typecheck584  have e21 : g * m + h * p + k * s ∈ ℝ by typecheck585  have e22 : g * n + h * q + k * u ∈ ℝ by typecheck586  have resultMatrix : matrix3of(a * l + b * o + c * r, a * m + b * p + c * s,587      a * n + b * q + c * u, d * l + e * o + f * r, d * m + e * p + f * s,588      d * n + e * q + f * u, g * l + h * o + k * r, g * m + h * p + k * s,589      g * n + h * q + k * u) : realRing ^ 3 × 3 :=590    matrix3of.matrix with *591  have productTyped : Matrix3(matrixMul3(matrix3of(a, b, c, d, e, f, g, h, k), matrix3of(l, m, n, o, p, q, r, s, u))) :=592    Matrix3.mul with leftTyped, rightTyped593  have resultTyped : Matrix3(matrix3of(a * l + b * o + c * r, a * m + b * p + c * s,594      a * n + b * q + c * u, d * l + e * o + f * r, d * m + e * p + f * s,595      d * n + e * q + f * u, g * l + h * o + k * r, g * m + h * p + k * s,596      g * n + h * q + k * u)) :=597    Matrix3.of_matrix with resultMatrix598  exact Matrix3.ext with productTyped, resultTyped, entries599600theorem matrix3of.one601  shows matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R)) =602    Ring.one(matrixRing(realRing, 3))603proof604  have zeroReal : (0:R) ∈ ℝ by typecheck605  have oneReal : (1:R) ∈ ℝ by typecheck606  have d01 := threeIndex.zero_ne_one607  have d02 := threeIndex.zero_ne_two608  have d12 := threeIndex.one_ne_two609  have entries : ∀ i ∈ 3, ∀ j ∈ 3,610      matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R))[i, j] =611      Ring.one(matrixRing(realRing, 3))[i, j]612    intros i hi j hj613    have comm := realRing.comm_ring614    have entry := matrixRing.one_entry at realRing, 3, i, j with *615    rw [entry, realRing.carrierOf, realRing.zero_eq, realRing.one_eq]616    have rows := threeIndex.cases with hi617    have columns := threeIndex.cases with hj618    rcases rows with rowZero | rowOne | rowTwo619    . rcases columns with columnZero | columnOne | columnTwo620      . rw [rowZero, columnZero, matrix3of.entry00, singleValue.same]621        rfl622      . have different : (0:N) ≠ (1:N) := d01623        rw [rowZero, columnOne, matrix3of.entry01, singleValue.other]624        rfl625      . have different : (0:N) ≠ (2:N) := d02626        rw [rowZero, columnTwo, matrix3of.entry02, singleValue.other]627        rfl628    . rcases columns with columnZero | columnOne | columnTwo629      . have different : (1:N) ≠ (0:N)630          intro same631          symm at same632          exact d01 with same633        rw [rowOne, columnZero, matrix3of.entry10, singleValue.other]634        rfl635      . rw [rowOne, columnOne, matrix3of.entry11, singleValue.same]636        rfl637      . have different : (1:N) ≠ (2:N) := d12638        rw [rowOne, columnTwo, matrix3of.entry12, singleValue.other]639        rfl640    . rcases columns with columnZero | columnOne | columnTwo641      . have different : (2:N) ≠ (0:N)642          intro same643          symm at same644          exact d02 with same645        rw [rowTwo, columnZero, matrix3of.entry20, singleValue.other]646        rfl647      . have different : (2:N) ≠ (1:N)648          intro same649          symm at same650          exact d12 with same651        rw [rowTwo, columnOne, matrix3of.entry21, singleValue.other]652        rfl653      . rw [rowTwo, columnTwo, matrix3of.entry22, singleValue.same]654        rfl655  have leftMatrix : matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R)) : realRing ^ 3 × 3 :=656    matrix3of.matrix with *657  have leftTyped : Matrix3(matrix3of((1:R), (0:R), (0:R), (0:R), (1:R), (0:R), (0:R), (0:R), (1:R))) :=658    Matrix3.of_matrix with leftMatrix659  have oneTyped : Matrix3(Ring.one(matrixRing(realRing, 3))) := Matrix3.one660  exact Matrix3.ext with leftTyped, oneTyped, entries661