-- The determinant of a 3 × 3 matrix over a commutative ring as the
-- six-term Leibniz formula: the six permutations of 3 listed with their
-- signs, a finite sum over six listed points, and the expansion
-- 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.DeterminantThree
import PermutationSign
import DeterminantIdentity
import Combinatorics.Permutations

-- Peeling one point off the sum of a function restricted to a finite set.
theorem finiteRingSum.insert_restrict (V A add zero neg mul one f D a : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires function : f : D → A
  requires subset : insert(a, V) ⊆ D
  requires fresh : ¬(a ∈ V)
  shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one,
      restrict(f, insert(a, V))) =
    call2(add, finiteRingSum(V, A, add, zero, neg, mul, one, restrict(f, V)),
      f(a))
proof
  have weights := restrict.domain_function at f, D, A, insert(a, V)
    with function, subset
  have step := finiteRingSum.insert at V, A, add, zero, neg, mul, one,
    restrict(f, insert(a, V)), a with ring, finite, weights, fresh
  have inner : V ⊆ insert(a, V)
    intros x hx
    exact insert.contains with hx
  have nested := restrict.nested at f, V, insert(a, V) with inner
  have self := insert.self at a, V
  have value := restrict.domain_apply at f, D, A, insert(a, V), a
    with function, subset, self
  rw [step, nested, value]
  rfl

-- The sum of a function over six listed points.
theorem finiteRingSum.six (A add zero neg mul one f D p q r s t u : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires function : f : D → A
  requires subset : insert(u, insert(t, insert(s, insert(r, insert(q, {p}))))) ⊆ D
  requires freshQ : ¬(q ∈ {p})
  requires freshR : ¬(r ∈ insert(q, {p}))
  requires freshS : ¬(s ∈ insert(r, insert(q, {p})))
  requires freshT : ¬(t ∈ insert(s, insert(r, insert(q, {p}))))
  requires freshU : ¬(u ∈ insert(t, insert(s, insert(r, insert(q, {p})))))
  shows finiteRingSum(insert(u, insert(t, insert(s, insert(r, insert(q, {p}))))),
      A, add, zero, neg, mul, one,
      restrict(f, insert(u, insert(t, insert(s, insert(r, insert(q, {p}))))))) =
    call2(add, call2(add, call2(add, call2(add, call2(add, f(p), f(q)), f(r)),
      f(s)), f(t)), f(u))
proof
  have finite1 := Finite.singleton at p
  have finite2 := Finite.insert at {p}, q with finite1
  have finite3 := Finite.insert at insert(q, {p}), r with finite2
  have finite4 := Finite.insert at insert(r, insert(q, {p})), s with finite3
  have finite5 := Finite.insert at insert(s, insert(r, insert(q, {p}))), t
    with finite4
  have sub5 : insert(t, insert(s, insert(r, insert(q, {p})))) ⊆ D
    intros x hx
    exact subset with x, (insert.contains with hx)
  have sub4 : insert(s, insert(r, insert(q, {p}))) ⊆ D
    intros x hx
    exact sub5 with x, (insert.contains with hx)
  have sub3 : insert(r, insert(q, {p})) ⊆ D
    intros x hx
    exact sub4 with x, (insert.contains with hx)
  have sub2 : insert(q, {p}) ⊆ D
    intros x hx
    exact sub3 with x, (insert.contains with hx)
  have sub1 : {p} ⊆ D
    intros x hx
    exact sub2 with x, (insert.contains with hx)
  have step6 := finiteRingSum.insert_restrict at
    insert(t, insert(s, insert(r, insert(q, {p})))), A, add, zero, neg, mul, one,
    f, D, u with ring, finite5, function, subset, freshU
  have step5 := finiteRingSum.insert_restrict at
    insert(s, insert(r, insert(q, {p}))), A, add, zero, neg, mul, one,
    f, D, t with ring, finite4, function, sub5, freshT
  have step4 := finiteRingSum.insert_restrict at
    insert(r, insert(q, {p})), A, add, zero, neg, mul, one,
    f, D, s with ring, finite3, function, sub4, freshS
  have step3 := finiteRingSum.insert_restrict at
    insert(q, {p}), A, add, zero, neg, mul, one,
    f, D, r with ring, finite2, function, sub3, freshR
  have step2 := finiteRingSum.insert_restrict at
    {p}, A, add, zero, neg, mul, one, f, D, q with ring, finite1, function, sub2, freshQ
  have weights1 := restrict.domain_function at f, D, A, {p} with function, sub1
  have step1 := finiteRingSum.singleton at A, add, zero, neg, mul, one,
    restrict(f, {p}), p with ring, weights1
  have selfP := singleton.self at p
  have valueP := restrict.domain_apply at f, D, A, {p}, p with function, sub1, selfP
  rw [step6, step5, step4, step3, step2, step1, valueP]
  rfl

-- Two functions with different values at a point are different.
theorem apply.distinct (p q x a b : Set)
  requires hp : p(x) = a
  requires hq : q(x) = b
  requires different : a ≠ b
  shows p ≠ q
proof
  intro same
  rw [same, hq] at hp
  symm at hp
  exact different with hp

-- The three indices and their distinctness.
theorem three.zero_mem
  shows 0 ∈ 3
proof
  typecheck

theorem three.one_mem
  shows 1 ∈ 3
proof
  typecheck

theorem three.two_mem
  shows 2 ∈ 3
proof
  typecheck

theorem three.zero_ne_one
  shows 0 ≠ 1
proof
  intro equal
  arith

theorem three.zero_ne_two
  shows 0 ≠ 2
proof
  intro equal
  arith

theorem three.one_ne_two
  shows 1 ≠ 2
proof
  intro equal
  arith

theorem three.one_ne_zero
  shows 1 ≠ 0
proof
  intro equal
  arith

theorem three.two_ne_zero
  shows 2 ≠ 0
proof
  intro equal
  arith

theorem three.two_ne_one
  shows 2 ≠ 1
proof
  intro equal
  arith

-- The six permutations of 3: the identity, the three transpositions, and
-- the two three-cycles as composites of transpositions.
def swapZeroOne : Set := transposition(3, 0, 1)
def swapZeroTwo : Set := transposition(3, 0, 2)
def swapOneTwo : Set := transposition(3, 1, 2)
def cycleForward : Set := compose(swapZeroOne, swapOneTwo, 3, 3, 3)
def cycleBackward : Set := compose(swapZeroOne, swapZeroTwo, 3, 3, 3)

theorem swapZeroOne.permutation
  shows swapZeroOne ∈ permutations(3)
proof
  unfold swapZeroOne
  exact permutations.transposition at 3, 0, 1 with three.zero_mem, three.one_mem

theorem swapZeroTwo.permutation
  shows swapZeroTwo ∈ permutations(3)
proof
  unfold swapZeroTwo
  exact permutations.transposition at 3, 0, 2 with three.zero_mem, three.two_mem

theorem swapOneTwo.permutation
  shows swapOneTwo ∈ permutations(3)
proof
  unfold swapOneTwo
  exact permutations.transposition at 3, 1, 2 with three.one_mem, three.two_mem

theorem cycleForward.permutation
  shows cycleForward ∈ permutations(3)
proof
  unfold cycleForward
  exact permutations.compose at 3, swapOneTwo, swapZeroOne
    with swapOneTwo.permutation, swapZeroOne.permutation

theorem cycleBackward.permutation
  shows cycleBackward ∈ permutations(3)
proof
  unfold cycleBackward
  exact permutations.compose at 3, swapZeroTwo, swapZeroOne
    with swapZeroTwo.permutation, swapZeroOne.permutation

theorem swapZeroOne.values
  shows swapZeroOne(0) = 1 ∧ swapZeroOne(1) = 0 ∧ swapZeroOne(2) = 2
proof
  have first := transposition.first at 3, 0, 1 with three.zero_mem, three.one_mem
  have second := transposition.second at 3, 0, 1 with three.zero_mem, three.one_mem
  have other := transposition.other at 3, 0, 1, 2
    with three.zero_mem, three.one_mem, three.two_mem, three.two_ne_zero, three.two_ne_one
  unfold swapZeroOne
  exact ⟨first, second, other⟩

theorem swapZeroTwo.values
  shows swapZeroTwo(0) = 2 ∧ swapZeroTwo(1) = 1 ∧ swapZeroTwo(2) = 0
proof
  have first := transposition.first at 3, 0, 2 with three.zero_mem, three.two_mem
  have second := transposition.second at 3, 0, 2 with three.zero_mem, three.two_mem
  have other := transposition.other at 3, 0, 2, 1
    with three.zero_mem, three.two_mem, three.one_mem, three.one_ne_zero, three.one_ne_two
  unfold swapZeroTwo
  exact ⟨first, other, second⟩

theorem swapOneTwo.values
  shows swapOneTwo(0) = 0 ∧ swapOneTwo(1) = 2 ∧ swapOneTwo(2) = 1
proof
  have first := transposition.first at 3, 1, 2 with three.one_mem, three.two_mem
  have second := transposition.second at 3, 1, 2 with three.one_mem, three.two_mem
  have other := transposition.other at 3, 1, 2, 0
    with three.one_mem, three.two_mem, three.zero_mem, three.zero_ne_one, three.zero_ne_two
  unfold swapOneTwo
  exact ⟨other, first, second⟩

theorem cycleForward.values
  shows cycleForward(0) = 1 ∧ cycleForward(1) = 2 ∧ cycleForward(2) = 0
proof
  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values
  obtain ⟨b0, b1, b2⟩ := swapOneTwo.values
  have outer := permutations.function with swapZeroOne.permutation
  have inner := permutations.function with swapOneTwo.permutation
  have at0 := compose.apply at swapZeroOne, swapOneTwo, 3, 3, 3, 0
    with inner, outer, three.zero_mem
  have at1 := compose.apply at swapZeroOne, swapOneTwo, 3, 3, 3, 1
    with inner, outer, three.one_mem
  have at2 := compose.apply at swapZeroOne, swapOneTwo, 3, 3, 3, 2
    with inner, outer, three.two_mem
  unfold cycleForward
  rw [at0, at1, at2, b0, b1, b2, a0, a1, a2]
  exact ⟨rfl, rfl, rfl⟩

theorem cycleBackward.values
  shows cycleBackward(0) = 2 ∧ cycleBackward(1) = 0 ∧ cycleBackward(2) = 1
proof
  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values
  obtain ⟨b0, b1, b2⟩ := swapZeroTwo.values
  have outer := permutations.function with swapZeroOne.permutation
  have inner := permutations.function with swapZeroTwo.permutation
  have at0 := compose.apply at swapZeroOne, swapZeroTwo, 3, 3, 3, 0
    with inner, outer, three.zero_mem
  have at1 := compose.apply at swapZeroOne, swapZeroTwo, 3, 3, 3, 1
    with inner, outer, three.one_mem
  have at2 := compose.apply at swapZeroOne, swapZeroTwo, 3, 3, 3, 2
    with inner, outer, three.two_mem
  unfold cycleBackward
  rw [at0, at1, at2, b0, b1, b2, a0, a1, a2]
  exact ⟨rfl, rfl, rfl⟩

theorem identity.three_values
  shows identity(3)(0) = 0 ∧ identity(3)(1) = 1 ∧ identity(3)(2) = 2
proof
  have at0 := identity.apply at 0, 3 with three.zero_mem
  have at1 := identity.apply at 1, 3 with three.one_mem
  have at2 := identity.apply at 2, 3 with three.two_mem
  exact ⟨at0, at1, at2⟩

-- The six are pairwise distinct, each pair separated by a value.
theorem permutations.three_distinct
  shows swapZeroOne ≠ identity(3) ∧ swapZeroTwo ≠ identity(3) ∧
    swapOneTwo ≠ identity(3) ∧ cycleForward ≠ identity(3) ∧
    cycleBackward ≠ identity(3) ∧ swapZeroTwo ≠ swapZeroOne ∧
    swapOneTwo ≠ swapZeroOne ∧ cycleForward ≠ swapZeroOne ∧
    cycleBackward ≠ swapZeroOne ∧ swapOneTwo ≠ swapZeroTwo ∧
    cycleForward ≠ swapZeroTwo ∧ cycleBackward ≠ swapZeroTwo ∧
    cycleForward ≠ swapOneTwo ∧ cycleBackward ≠ swapOneTwo ∧
    cycleBackward ≠ cycleForward
proof
  obtain ⟨i0, i1, i2⟩ := identity.three_values
  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values
  obtain ⟨b0, b1, b2⟩ := swapZeroTwo.values
  obtain ⟨c0, c1, c2⟩ := swapOneTwo.values
  obtain ⟨f0, f1, f2⟩ := cycleForward.values
  obtain ⟨g0, g1, g2⟩ := cycleBackward.values
  have dAI := apply.distinct with a0, i0, three.one_ne_zero
  have dBI := apply.distinct with b0, i0, three.two_ne_zero
  have dCI := apply.distinct with c1, i1, three.two_ne_one
  have dFI := apply.distinct with f0, i0, three.one_ne_zero
  have dGI := apply.distinct with g0, i0, three.two_ne_zero
  have dBA := apply.distinct with b0, a0, three.two_ne_one
  have dCA := apply.distinct with c0, a0, three.zero_ne_one
  have dFA := apply.distinct with f1, a1, three.two_ne_zero
  have dGA := apply.distinct with g0, a0, three.two_ne_one
  have dCB := apply.distinct with c0, b0, three.zero_ne_two
  have dFB := apply.distinct with f0, b0, three.one_ne_two
  have dGB := apply.distinct with g1, b1, three.zero_ne_one
  have dFC := apply.distinct with f0, c0, three.one_ne_zero
  have dGC := apply.distinct with g0, c0, three.two_ne_zero
  have dGF := apply.distinct with g0, f0, three.two_ne_one
  exact ⟨dAI, dBI, dCI, dFI, dGI, dBA, dCA, dFA, dGA, dCB, dFB, dGB, dFC, dGC, dGF⟩

-- Each of the six is new to the ones listed before it.
theorem permutations.three_fresh
  shows ¬(swapZeroOne ∈ {identity(3)}) ∧
    ¬(swapZeroTwo ∈ insert(swapZeroOne, {identity(3)})) ∧
    ¬(swapOneTwo ∈ insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))) ∧
    ¬(cycleForward ∈ insert(swapOneTwo, insert(swapZeroTwo,
      insert(swapZeroOne, {identity(3)})))) ∧
    ¬(cycleBackward ∈ insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))
proof
  obtain ⟨dAI, dBI, dCI, dFI, dGI, dBA, dCA, dFA, dGA, dCB, dFB, dGB, dFC, dGC, dGF⟩ :=
    permutations.three_distinct
  constructor
  . intro member
    have equal := singleton.membership.forward with member
    exact dAI with equal
  constructor
  . intro member
    have alternatives0 := insert.membership.forward with member
    rcases alternatives0 with equal0 | rest0
    . exact dBA with equal0
    . have equal := singleton.membership.forward with rest0
      exact dBI with equal
  constructor
  . intro member
    have alternatives0 := insert.membership.forward with member
    rcases alternatives0 with equal0 | rest0
    . exact dCB with equal0
    . have alternatives1 := insert.membership.forward with rest0
      rcases alternatives1 with equal1 | rest1
      . exact dCA with equal1
      . have equal := singleton.membership.forward with rest1
        exact dCI with equal
  constructor
  . intro member
    have alternatives0 := insert.membership.forward with member
    rcases alternatives0 with equal0 | rest0
    . exact dFC with equal0
    . have alternatives1 := insert.membership.forward with rest0
      rcases alternatives1 with equal1 | rest1
      . exact dFB with equal1
      . have alternatives2 := insert.membership.forward with rest1
        rcases alternatives2 with equal2 | rest2
        . exact dFA with equal2
        . have equal := singleton.membership.forward with rest2
          exact dFI with equal
  . intro member
    have alternatives0 := insert.membership.forward with member
    rcases alternatives0 with equal0 | rest0
    . exact dGF with equal0
    . have alternatives1 := insert.membership.forward with rest0
      rcases alternatives1 with equal1 | rest1
      . exact dGC with equal1
      . have alternatives2 := insert.membership.forward with rest1
        rcases alternatives2 with equal2 | rest2
        . exact dGB with equal2
        . have alternatives3 := insert.membership.forward with rest2
          rcases alternatives3 with equal3 | rest3
          . exact dGA with equal3
          . have equal := singleton.membership.forward with rest3
            exact dGI with equal

-- The six listed permutations are all of them: they are six distinct
-- permutations of 3, and 3 has 3! = 6 permutations.
theorem permutations.three
  shows permutations(3) = insert(cycleBackward, insert(cycleForward,
    insert(swapOneTwo, insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))
proof
  obtain ⟨freshA, freshB, freshC, freshF, freshG⟩ := permutations.three_fresh
  have finite := permutations.finite at 3 with (Finite.natural at 3)
  have subset : insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))) ⊆ permutations(3)
    intros p hp
    have alternatives0 := insert.membership.forward with hp
    rcases alternatives0 with equal0 | rest0
    . rw equal0
      exact cycleBackward.permutation
    . have alternatives1 := insert.membership.forward with rest0
      rcases alternatives1 with equal1 | rest1
      . rw equal1
        exact cycleForward.permutation
      . have alternatives2 := insert.membership.forward with rest1
        rcases alternatives2 with equal2 | rest2
        . rw equal2
          exact swapOneTwo.permutation
        . have alternatives3 := insert.membership.forward with rest2
          rcases alternatives3 with equal3 | rest3
          . rw equal3
            exact swapZeroTwo.permutation
          . have alternatives4 := insert.membership.forward with rest3
            rcases alternatives4 with equal4 | rest4
            . rw equal4
              exact swapZeroOne.permutation
            . have equal := singleton.membership.forward with rest4
              rw equal
              exact permutations.identity at 3
  have finite1 := Finite.singleton at identity(3)
  have finite2 := Finite.insert at {identity(3)}, swapZeroOne with finite1
  have finite3 := Finite.insert at insert(swapZeroOne, {identity(3)}), swapZeroTwo
    with finite2
  have finite4 := Finite.insert at insert(swapZeroTwo, insert(swapZeroOne,
    {identity(3)})), swapOneTwo with finite3
  have finite5 := Finite.insert at insert(swapOneTwo, insert(swapZeroTwo,
    insert(swapZeroOne, {identity(3)}))), cycleForward with finite4
  have count1 := cardinality.singleton at identity(3)
  have count2 := cardinality.insert at {identity(3)}, swapZeroOne with finite1, freshA
  have count3 := cardinality.insert at insert(swapZeroOne, {identity(3)}), swapZeroTwo
    with finite2, freshB
  have count4 := cardinality.insert at insert(swapZeroTwo, insert(swapZeroOne,
    {identity(3)})), swapOneTwo with finite3, freshC
  have count5 := cardinality.insert at insert(swapOneTwo, insert(swapZeroTwo,
    insert(swapZeroOne, {identity(3)}))), cycleForward with finite4, freshF
  have count6 := cardinality.insert at insert(cycleForward, insert(swapOneTwo,
    insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))), cycleBackward
    with finite5, freshG
  have same : cardinality(insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))) =
      cardinality(permutations(3))
    rw [count6, count5, count4, count3, count2, count1, permutations.three_count]
    compute
  have equal := cardinality.eq_subset with finite, subset, same
  symm at equal
  exact equal

section Signs
variable (A add zero neg mul one : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)

-- A transposition has sign -1: it is the exchange of the identity.
theorem permutationSign.transposition (n : Nat) (a b : Set)
  requires ha : a ∈ n
  requires hb : b ∈ n
  requires distinct : a ≠ b
  shows permutationSign(n, R, transposition(n, a, b)) = R[-R[1]]
proof
  have idPerm := permutations.identity at n
  have exchange := permutationSign.exchange at A, add, zero, neg, mul, one, n, a, b,
    identity(n) with ring, ha, hb, distinct, idPerm
  have value := permutationExchange.value at n, a, b, identity(n) with ha, hb, idPerm
  have swapFunction := transposition.function at n, a, b with ha, hb
  have left := compose.identity_left at transposition(n, a, b), n, n with swapFunction
  have signOne := permutationSign.identity at A, add, zero, neg, mul, one, n with ring
  rw [value, left, signOne] at exchange
  exact exchange

end Signs

-- The signs of the six permutations of 3: the identity has sign 1, the
-- transpositions -1, and the three-cycles, each one exchange away from a
-- transposition, -(-1).
theorem permutations.three_signs (A add zero neg mul one : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows permutationSign(3, A, add, zero, neg, mul, one, identity(3)) = one ∧
    permutationSign(3, A, add, zero, neg, mul, one, swapZeroOne) = neg(one) ∧
    permutationSign(3, A, add, zero, neg, mul, one, swapZeroTwo) = neg(one) ∧
    permutationSign(3, A, add, zero, neg, mul, one, swapOneTwo) = neg(one) ∧
    permutationSign(3, A, add, zero, neg, mul, one, cycleForward) = neg(neg(one)) ∧
    permutationSign(3, A, add, zero, neg, mul, one, cycleBackward) = neg(neg(one))
proof
  have signI := permutationSign.identity at A, add, zero, neg, mul, one, 3 with ring
  have signA := permutationSign.transposition at A, add, zero, neg, mul, one, 3, 0, 1
    with ring, three.zero_mem, three.one_mem, three.zero_ne_one
  have signB := permutationSign.transposition at A, add, zero, neg, mul, one, 3, 0, 2
    with ring, three.zero_mem, three.two_mem, three.zero_ne_two
  have signC := permutationSign.transposition at A, add, zero, neg, mul, one, 3, 1, 2
    with ring, three.one_mem, three.two_mem, three.one_ne_two
  have signSwap : permutationSign(3, A, add, zero, neg, mul, one, swapZeroOne) = neg(one)
    simp [swapZeroOne]
  have exchangeF := permutationSign.exchange at A, add, zero, neg, mul, one, 3, 1, 2,
    swapZeroOne with ring, three.one_mem, three.two_mem, three.one_ne_two,
    swapZeroOne.permutation
  have valueF := permutationExchange.value at 3, 1, 2, swapZeroOne
    with three.one_mem, three.two_mem, swapZeroOne.permutation
  have exchangeG := permutationSign.exchange at A, add, zero, neg, mul, one, 3, 0, 2,
    swapZeroOne with ring, three.zero_mem, three.two_mem, three.zero_ne_two,
    swapZeroOne.permutation
  have valueG := permutationExchange.value at 3, 0, 2, swapZeroOne
    with three.zero_mem, three.two_mem, swapZeroOne.permutation
  have signF : permutationSign(3, A, add, zero, neg, mul, one, cycleForward) =
      neg(neg(one))
    unfold cycleForward
    unfold swapOneTwo
    rw ← valueF
    rw [exchangeF, signSwap]
    rfl
  have signG : permutationSign(3, A, add, zero, neg, mul, one, cycleBackward) =
      neg(neg(one))
    unfold cycleBackward
    unfold swapZeroTwo
    rw ← valueG
    rw [exchangeG, signSwap]
    rfl
  unfold swapZeroOne
  unfold swapZeroTwo
  unfold swapOneTwo
  exact ⟨signI, signA, signB, signC, signF, signG⟩

-- The product of the entries picked by a permutation of 3.
theorem permutationEntries.three_product (A add zero neg mul one M p : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires matrix : RingMatrix(3, A, M)
  requires permutation : p ∈ permutations(3)
  shows finiteRingProduct(3, A, add, zero, neg, mul, one, permutationEntries(3, A, M, p)) =
    call2(mul, call2(mul, call2(mul, one, M[0, p(0)]), M[1, p(1)]), M[2, p(2)])
proof
  have bijective := permutations.bijective with permutation
  have weights := permutationEntries.function at 3, A, M, p with matrix, bijective
  have enumeration := identity.bijective at 3
  have indexed := finiteRingProduct.enumeration at 3, A, add, zero, neg, mul, one,
    permutationEntries(3, A, M, p), identity(3), 3 with ring, weights, enumeration
  obtain ⟨i0, i1, i2⟩ := identity.three_values
  have e0 := permutationEntries.value at 3, A, M, p, 0 with matrix, bijective, three.zero_mem
  have e1 := permutationEntries.value at 3, A, M, p, 1 with matrix, bijective, three.one_mem
  have e2 := permutationEntries.value at 3, A, M, p, 2 with matrix, bijective, three.two_mem
  rw indexed
  simp [indexedRingProduct, i0, i1, i2, e0, e1, e2]

-- The determinant of a 3 × 3 matrix is the sum of its six signed
-- permutation products, listed as the identity, the three transpositions,
-- and the two three-cycles.
theorem determinant.three (A add zero neg mul one M : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires matrix : RingMatrix(3, A, M)
  shows determinant(3, A, add, zero, neg, mul, one, M) =
    call2(add, call2(add, call2(add, call2(add, call2(add,
      call2(mul, one,
        call2(mul, call2(mul, call2(mul, one, M[0, 0]), M[1, 1]), M[2, 2])),
      call2(mul, neg(one),
        call2(mul, call2(mul, call2(mul, one, M[0, 1]), M[1, 0]), M[2, 2]))),
      call2(mul, neg(one),
        call2(mul, call2(mul, call2(mul, one, M[0, 2]), M[1, 1]), M[2, 0]))),
      call2(mul, neg(one),
        call2(mul, call2(mul, call2(mul, one, M[0, 0]), M[1, 2]), M[2, 1]))),
      call2(mul, neg(neg(one)),
        call2(mul, call2(mul, call2(mul, one, M[0, 1]), M[1, 2]), M[2, 0]))),
      call2(mul, neg(neg(one)),
        call2(mul, call2(mul, call2(mul, one, M[0, 2]), M[1, 0]), M[2, 1])))
proof
  have finite := Finite.natural at 3
  have terms := determinantTerms.function at 3, A, add, zero, neg, mul, one, M
    with ring, finite, matrix
  obtain ⟨freshA, freshB, freshC, freshF, freshG⟩ := permutations.three_fresh
  obtain ⟨signI, signA, signB, signC, signF, signG⟩ :=
    permutations.three_signs at A, add, zero, neg, mul, one with ring
  obtain ⟨i0, i1, i2⟩ := identity.three_values
  obtain ⟨a0, a1, a2⟩ := swapZeroOne.values
  obtain ⟨b0, b1, b2⟩ := swapZeroTwo.values
  obtain ⟨c0, c1, c2⟩ := swapOneTwo.values
  obtain ⟨f0, f1, f2⟩ := cycleForward.values
  obtain ⟨g0, g1, g2⟩ := cycleBackward.values
  have idPerm := permutations.identity at 3
  have termI := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, identity(3)
    with ring, finite, matrix, idPerm
  have termA := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, swapZeroOne
    with ring, finite, matrix, swapZeroOne.permutation
  have termB := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, swapZeroTwo
    with ring, finite, matrix, swapZeroTwo.permutation
  have termC := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, swapOneTwo
    with ring, finite, matrix, swapOneTwo.permutation
  have termF := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, cycleForward
    with ring, finite, matrix, cycleForward.permutation
  have termG := determinantTerms.value at 3, A, add, zero, neg, mul, one, M, cycleBackward
    with ring, finite, matrix, cycleBackward.permutation
  have productI := permutationEntries.three_product at A, add, zero, neg, mul, one, M,
    identity(3) with ring, matrix, idPerm
  have productA := permutationEntries.three_product at A, add, zero, neg, mul, one, M,
    swapZeroOne with ring, matrix, swapZeroOne.permutation
  have productB := permutationEntries.three_product at A, add, zero, neg, mul, one, M,
    swapZeroTwo with ring, matrix, swapZeroTwo.permutation
  have productC := permutationEntries.three_product at A, add, zero, neg, mul, one, M,
    swapOneTwo with ring, matrix, swapOneTwo.permutation
  have productF := permutationEntries.three_product at A, add, zero, neg, mul, one, M,
    cycleForward with ring, matrix, cycleForward.permutation
  have productG := permutationEntries.three_product at A, add, zero, neg, mul, one, M,
    cycleBackward with ring, matrix, cycleBackward.permutation
  rw [i0, i1, i2] at productI
  rw [a0, a1, a2] at productA
  rw [b0, b1, b2] at productB
  rw [c0, c1, c2] at productC
  rw [f0, f1, f2] at productF
  rw [g0, g1, g2] at productG
  have listed := permutations.three
  rw listed at terms
  have whole : insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))) ⊆
      insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)})))))
    intros x hx
    exact hx
  have six := finiteRingSum.six at A, add, zero, neg, mul, one,
    determinantTerms(3, A, add, zero, neg, mul, one, M),
    insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))),
    identity(3), swapZeroOne, swapZeroTwo, swapOneTwo, cycleForward, cycleBackward
    with ring, terms, whole, freshA, freshB, freshC, freshF, freshG
  have listedFinite : Finite(insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))))
    rw ← listed
    exact permutations.finite at 3 with finite
  have restricted := restrict.domain_function at
    determinantTerms(3, A, add, zero, neg, mul, one, M),
    insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))), A,
    insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))) with terms, whole
  have values : ∀ x ∈ insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
      insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))),
      determinantTerms(3, A, add, zero, neg, mul, one, M)(x) =
      restrict(determinantTerms(3, A, add, zero, neg, mul, one, M),
        insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
        insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))))(x)
    intros x hx
    have value := restrict.domain_apply at
      determinantTerms(3, A, add, zero, neg, mul, one, M),
      insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
        insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))), A,
      insert(cycleBackward, insert(cycleForward, insert(swapOneTwo,
        insert(swapZeroTwo, insert(swapZeroOne, {identity(3)}))))), x with terms, whole, hx
    symm at value
    exact value
  have congruent := finiteRingSum.congr with ring, listedFinite, terms, restricted, values
  simp [determinant]