-- Finite products in commutative rings, independent of enumeration (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.FiniteProduct
import SumSupport

def indexedRingProduct (w f mul u1 : Set, n : Nat) → Set
  | w, f, mul, u1, zero => u1
  | w, f, mul, u1, succ(k) => call2(mul, indexedRingProduct(w, f, mul, u1, k), w(f(k)))

def matchingProductRow (A u1 mul w f x : Set, n : Nat) → Set
  | A, u1, mul, w, f, x, zero => u1
  | A, u1, mul, w, f, x, succ(k) => call2(mul, matchingProductRow(A, u1, mul, w, f, x, k), singleValue(A, u1, w(x), x, f(k)))

def matchingProductTotal (A u1 mul w f g : Set, n m : Nat) → Set
  | A, u1, mul, w, f, g, n, zero => u1
  | A, u1, mul, w, f, g, n, succ(k) => call2(mul, matchingProductTotal(A, u1, mul, w, f, g, n, k), matchingProductRow(A, u1, mul, w, f, g(k), n))
  descends m

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

theorem indexedRingProduct.closed (f : Set, n : Nat)
  shows WeightedValues(w, f, A, n) → indexedRingProduct(w, f, mul, one, n) ∈ A
proof
  induction n
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    intro values
    rw indexedRingProduct
    exact IsMonoid.unit_in_carrier with multiplicative
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    intro values
    have prefix := WeightedValues.prefix at w, f, A, k with *
    have last := WeightedValues.last at w, f, A, k with *
    have previous := ih with prefix
    rw indexedRingProduct
    exact IsRing.mul_closed with ordinary, previous, last

theorem matchingProductRow.closed (f x : Set, n : Nat)
  requires value : w(x) ∈ A
  shows matchingProductRow(A, one, mul, w, f, x, n) ∈ A
proof
  induction n
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    rwa matchingProductRow
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    have last := singleValue.closed at A, one, w(x), x, f(k) with *
    rw matchingProductRow
    exact IsRing.mul_closed with ordinary, ih, last

theorem matchingProductTotal.closed (f g : Set, n m : Nat)
  shows WeightedValues(w, g, A, m) → matchingProductTotal(A, one, mul, w, f, g, n, m) ∈ A
proof
  induction m
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    intro values
    rw matchingProductTotal
    exact IsMonoid.unit_in_carrier with multiplicative
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    intro values
    have prefix := WeightedValues.prefix at w, g, A, k with *
    have last := WeightedValues.last at w, g, A, k with *
    have previous := ih with prefix
    have row := matchingProductRow.closed at A, add, zero, neg, mul, one, w, f, g(k), n with *
    rw matchingProductTotal
    exact IsRing.mul_closed with ordinary, previous, row

theorem matchingProductRow.absent (f x : Set, n : Nat)
  requires value : w(x) ∈ A
  shows (∀ i ∈ n, f(i) ≠ x) → matchingProductRow(A, one, mul, w, f, x, n) = one
proof
  induction n
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    intro absent
    rw matchingProductRow
    rfl
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    intro absent
    have prefix : ∀ i ∈ k, f(i) ≠ x
      intros i before
      have included := membership.into_successor at i, k with *
      exact absent with i, included
    have last := absent with k, membership.self_successor at k with *
    have previous := ih with prefix
    have entry := singleValue.other at A, one, w(x), x, f(k) with *
    rw [matchingProductRow, previous, entry]
    ring

theorem matchingProductRow.unique (f x : Set, n : Nat)
  requires value : w(x) ∈ A
  shows DistinctValues(f, n) → Occurs(f, n, x) → matchingProductRow(A, one, mul, w, f, x, n) = w(x)
proof
  induction n
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    intros distinct occurs
    rcases occurs with ⟨i, impossible, same⟩
    exfalso
    simp [nat.zero, set.empty]
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    intros distinct occurs
    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto
    cases alternatives with last | other
    . have fresh := DistinctValues.last_fresh at f, k with *
      have absent : ∀ i ∈ k, f(i) ≠ x
        intros i before equal
        have different := fresh with i, before
        rw ← last at equal
        exact different with equal
      have previous := matchingProductRow.absent at A, add, zero, neg, mul, one, w, f, x, k with *
      have entry := singleValue.same at A, one, w(x), x, f(k) with *
      rw [matchingProductRow, previous, entry]
      ring
    . obtain ⟨position, before, equal⟩ := Occurs.forward at f, succ(k), x with occurs
      have shape := membership.successor_forward{n := k} with before
      have earlier : position ∈ k
        cases shape with inside | atLast
        . exact inside
        . exfalso
          rw atLast at equal
          exact other with equal
      have prefix := DistinctValues.prefix at f, k with *
      have occurrence : Occurs(f, k, x)
        unfold Occurs
        refine ⟨position, earlier, equal⟩
      have previous := ih with prefix, occurrence
      have entry := singleValue.other at A, one, w(x), x, f(k) with *
      rw [matchingProductRow, previous, entry]
      ring

theorem matchingProductWeight.symmetric (x y : Set)
  requires xValue : w(x) ∈ A
  requires yValue : w(y) ∈ A
  shows singleValue(A, one, w(x), x, y) = singleValue(A, one, w(y), y, x)
proof
  have ordinary := IsCommRing.ring with ring
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have alternatives : x = y ∨ x ≠ y by tauto
  cases alternatives with same | different
  . rw same
    rfl
  . have reverse : y ≠ x
      intro equal
      have impossible : x = y by cc
      exact different with impossible
    have left := singleValue.other at A, one, w(x), x, y with *
    have right := singleValue.other at A, one, w(y), y, x with *
    cc

theorem matchingProductTotal.empty_left (f g : Set, m : Nat)
  shows matchingProductTotal(A, one, mul, w, f, g, (0:Nat), m) = one
proof
  induction m
  | zero =>
    rw matchingProductTotal
    rfl
  | succ(k) using ih =>
    rw [matchingProductTotal, matchingProductRow, ih]
    ring

theorem matchingProductTotal.extend_left (f g : Set, n m : Nat)
  requires value : w(f(n)) ∈ A
  shows WeightedValues(w, g, A, m) →
    matchingProductTotal(A, one, mul, w, f, g, succ(n), m) =
    matchingProductTotal(A, one, mul, w, f, g, n, m) * matchingProductRow(A, one, mul, w, g, f(n), m)
proof
  induction m
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    intro values
    simp [matchingProductTotal, matchingProductRow]
    ring
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    intro values
    have prefix := WeightedValues.prefix at w, g, A, k with *
    have last := WeightedValues.last at w, g, A, k with *
    have previous := ih with prefix
    have symmetric := matchingProductWeight.symmetric at A, add, zero, neg, mul, one, w, g(k), f(n) with *
    have totalBound := matchingProductTotal.closed at A, add, zero, neg, mul, one, w, f, g, n, k with *
    have totalIn := totalBound with prefix
    have rowLeftIn := matchingProductRow.closed at A, add, zero, neg, mul, one, w, g, f(n), k with *
    have rowRightIn := matchingProductRow.closed at A, add, zero, neg, mul, one, w, f, g(k), n with *
    have entryIn := singleValue.closed at A, one, w(f(n)), f(n), g(k) with *
    rw [matchingProductTotal, matchingProductTotal, matchingProductRow, matchingProductRow, previous, symmetric]
    ring

theorem matchingProductTotal.transpose (f g : Set, m n : Nat)
  requires valuesG : WeightedValues(w, g, A, m)
  shows WeightedValues(w, f, A, n) →
    matchingProductTotal(A, one, mul, w, f, g, n, m) = matchingProductTotal(A, one, mul, w, g, f, m, n)
proof
  induction n
  | zero =>
    intro valuesF
    have empty := matchingProductTotal.empty_left at A, add, zero, neg, mul, one, w, f, g, m with *
    rw [empty, matchingProductTotal]
    rfl
  | succ(k) using ih =>
    intro valuesF
    have prefix := WeightedValues.prefix at w, f, A, k with *
    have last := WeightedValues.last at w, f, A, k with *
    have previous := ih with prefix
    have extended := matchingProductTotal.extend_left at A, add, zero, neg, mul, one, w, f, g, k, m with *
    rw [extended, matchingProductTotal, previous]
    rfl

theorem matchingProductTotal.product (f g : Set, n m : Nat)
  requires distinct : DistinctValues(f, n)
  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j))) →
    matchingProductTotal(A, one, mul, w, f, g, n, m) = indexedRingProduct(w, g, mul, one, m)
proof
  induction m
  | zero =>
    intros values covered
    simp [matchingProductTotal, indexedRingProduct]
  | succ(k) using ih =>
    intros values covered
    have prefix : ∀ j ∈ k, Occurs(f, n, g(j))
      intros j before
      have included := membership.into_successor at j, k with *
      exact covered with j, included
    have last := covered with k, membership.self_successor at k with *
    have valuePrefix := WeightedValues.prefix at w, g, A, k with *
    have valueLast := WeightedValues.last at w, g, A, k with *
    have row := matchingProductRow.unique at A, add, zero, neg, mul, one, w, f, g(k), n with *
    have previous := ih with valuePrefix, prefix
    rw [matchingProductTotal, indexedRingProduct, previous, row]
    rfl

theorem indexedRingProduct.same_entries (f g : Set, n m : Nat)
  requires valuesF : WeightedValues(w, f, A, n)
  requires valuesG : WeightedValues(w, g, A, m)
  requires distinctF : DistinctValues(f, n)
  requires distinctG : DistinctValues(g, m)
  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i))
  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j))
  shows indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(w, g, mul, one, m)
proof
  have left := matchingProductTotal.product at A, add, zero, neg, mul, one, w, g, f, m, n with *
  have right := matchingProductTotal.product at A, add, zero, neg, mul, one, w, f, g, n, m with *
  have transpose := matchingProductTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *
  rw [← left, ← right]
  symm
  exact transpose with valuesF

theorem indexedRingProduct.reindex (V f g : Set, n m : Nat)
  requires weights : w : V → A
  requires enumerationF : BijectiveBetween(f, n, V)
  requires enumerationG : BijectiveBetween(g, m, V)
  shows indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(w, g, mul, one, m)
proof
  have injF := Bijective.injective with enumerationF
  have injG := Bijective.injective with enumerationG
  have surjF := Bijective.surjective with enumerationF
  have surjG := Bijective.surjective with enumerationG
  have fnF := Injective.function with injF
  have fnG := Injective.function with injG
  have distinctF := Injective.distinct_values with injF
  have distinctG := Injective.distinct_values with injG
  have valuesF : WeightedValues(w, f, A, n)
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact FunctionBetween.apply_closed with *
  have valuesG : WeightedValues(w, g, A, m)
    intros j hj
    have member := FunctionBetween.apply_closed with *
    exact FunctionBetween.apply_closed with *
  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i))
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact Surjective.occurs with *
  have coveredG : ∀ j ∈ m, Occurs(f, n, g(j))
    intros j hj
    have member := FunctionBetween.apply_closed with *
    exact Surjective.occurs with *
  exact indexedRingProduct.same_entries with *

theorem indexedRingProduct.mul (v h f : Set, n : Nat)
  shows WeightedValues(w, f, A, n) → WeightedValues(v, f, A, n) →
    (∀ i ∈ n, h(f(i)) = w(f(i)) * v(f(i))) →
    indexedRingProduct(h, f, mul, one, n) = indexedRingProduct(w, f, mul, one, n) * indexedRingProduct(v, f, mul, one, n)
proof
  induction n
  | zero =>
    intros valuesW valuesV equations
    simp [indexedRingProduct]
    ring
  | succ(k) using ih =>
    intros valuesW valuesV equations
    have prefixW := WeightedValues.prefix at w, f, A, k with *
    have prefixV := WeightedValues.prefix at v, f, A, k with *
    have lastW := WeightedValues.last at w, f, A, k with *
    have lastV := WeightedValues.last at v, f, A, k with *
    have prefix : ∀ i ∈ k, h(f(i)) = w(f(i)) * v(f(i))
      intros i hi
      have next := membership.into_successor at i, k with *
      exact equations with i, next
    have last := equations with k, membership.self_successor at k with *
    have previous := ih with prefixW, prefixV, prefix
    have closureW := indexedRingProduct.closed at A, add, zero, neg, mul, one, w, f, k with *
    have productW := closureW with prefixW
    have closureV := indexedRingProduct.closed at A, add, zero, neg, mul, one, v, f, k with *
    have productV := closureV with prefixV
    rw [indexedRingProduct, indexedRingProduct, indexedRingProduct, previous, last]
    ring

end Rings

defunique finiteRingProduct (V A add zero neg mul one w : Set) (product ∈ A) :=
  ∃ n, Nat(n) ∧ ∃ f, BijectiveBetween(f, n, V) ∧ product = indexedRingProduct(w, f, mul, one, n)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires finite : Finite(V)
requires weights : w : V → A
proof
  obtain ⟨n, natural, equivalent⟩ := finite
  obtain ⟨f, bijective⟩ := equivalent
  have enumeration := converse.bijective at f, V, n with bijective
  have function := converse.function_of_bijective at f, V, n with bijective
  have values := WeightedValues.of_functions with weights, function
  have closure := indexedRingProduct.closed at A, add, zero, neg, mul, one, w, converse(f, V, n), n with *
  have productIn := closure with values
  witness indexedRingProduct(w, converse(f, V, n), mul, one, n)
  refine ⟨productIn, n, natural, converse(f, V, n), enumeration, rfl⟩
uniqueness
  intros u uIn first v vIn second
  obtain ⟨n, naturalN, f, enumerationF, valueF⟩ := first
  obtain ⟨m, naturalM, g, enumerationG, valueG⟩ := second
  have same := indexedRingProduct.reindex at A, add, zero, neg, mul, one, w, V, f, g, n, m with *
  cc

notation scoped finiteRingProduct(V, R, w) => finiteRingProduct(V, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, w)

theorem finiteRingProduct.closed (V A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : V → A
  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) ∈ A
proof
  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *
  exact selected.left

theorem finiteRingProduct.enumeration (V A add zero neg mul one w f : Set, n : Nat)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : V → A
  requires enumeration : BijectiveBetween(f, n, V)
  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = indexedRingProduct(w, f, mul, one, n)
proof
  have reverse := converse.bijective with enumeration
  have cardinality : HasCardinality(V, n)
    unfold HasCardinality
    refine ⟨assumption, ?_⟩
    unfold Equipotent
    refine ⟨converse(f, n, V), reverse⟩
  have finite := Finite.from_cardinality with cardinality
  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *
  obtain ⟨m, naturalM, g, enumerationG, value⟩ := selected.right
  have same := indexedRingProduct.reindex at A, add, zero, neg, mul, one, w, V, g, f, m, n with *
  cc

theorem indexedRingProduct.congr (w v f g mul one : Set, n : Nat)
  shows (∀ i ∈ n, w(f(i)) = v(g(i))) → indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(v, g, mul, one, n)
proof
  induction n
  | zero =>
    intro values
    simp [indexedRingProduct]
  | succ(k) using ih =>
    intro values
    have prefix : ∀ i ∈ k, w(f(i)) = v(g(i))
      intros i before
      have included := membership.into_successor at i, k with *
      exact values with i, included
    have last := values with k, membership.self_successor at k with *
    have previous := ih with prefix
    rw [indexedRingProduct, indexedRingProduct, previous, last]
    rfl

theorem finiteRingProduct.congr (V A add zero neg mul one w v : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weightsW : w : V → A
  requires weightsV : v : V → A
  requires values : ∀ x ∈ V, w(x) = v(x)
  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = finiteRingProduct(V, A, add, zero, neg, mul, one, v)
proof
  have equal := FunctionBetween.ext with weightsW, weightsV, values
  rw equal
  rfl

theorem indexedRingProduct.one (A add zero neg mul one w f : Set, n : Nat)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows (∀ i ∈ n, w(f(i)) = one) → indexedRingProduct(w, f, mul, one, n) = one
proof
  induction n
  | zero =>
    intro values
    rw indexedRingProduct
    rfl
  | succ(k) using ih =>
    intro values
    have prefix : ∀ i ∈ k, w(f(i)) = one
      intros i before
      have included := membership.into_successor at i, k with *
      exact values with i, included
    have last := values with k, membership.self_successor at k with *
    have previous := ih with prefix
    rw [indexedRingProduct, previous, last]
    ring

theorem finiteRingProduct.one (V A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : V → A
  requires values : ∀ x ∈ V, w(x) = one
  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = one
proof
  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *
  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have unitValues : ∀ i ∈ n, w(f(i)) = one
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact values with f(i), member
  have unitProduct := indexedRingProduct.one at A, add, zero, neg, mul, one, w, f, n with *
  rw equation
  exact unitProduct with unitValues

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

theorem matchingProductRow.one (f x : Set, n : Nat)
  requires neutral : w(x) = one
  shows matchingProductRow(A, one, mul, w, f, x, n) = one
proof
  induction n
  | zero =>
    rw matchingProductRow
    rfl
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have multiplicative := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with multiplicative
    have value : w(x) ∈ A by rwa neutral
    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto
    have entry : singleValue(A, one, w(x), x, f(k)) = one
      cases alternatives with same | different
      . have selected := singleValue.same at A, one, w(x), x, f(k) with *
        cc
      . exact singleValue.other at A, one, w(x), x, f(k) with *
    rw [matchingProductRow, ih, entry]
    ring

theorem matchingProductRow.covered_or_one (f x : Set, n : Nat)
  requires value : w(x) ∈ A
  requires distinct : DistinctValues(f, n)
  requires covered : Occurs(f, n, x) ∨ w(x) = one
  shows matchingProductRow(A, one, mul, w, f, x, n) = w(x)
proof
  cases covered with occurs | neutral
  . have unique := matchingProductRow.unique at A, add, zero, neg, mul, one, w, f, x, n with *
    exact unique with distinct, occurs
  . have empty := matchingProductRow.one at A, add, zero, neg, mul, one, w, f, x, n with *
    cc

theorem matchingProductTotal.support_product (f g : Set, n m : Nat)
  requires distinct : DistinctValues(f, n)
  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = one) →
    matchingProductTotal(A, one, mul, w, f, g, n, m) = indexedRingProduct(w, g, mul, one, m)
proof
  induction m
  | zero =>
    intros values covered
    simp [matchingProductTotal, indexedRingProduct]
  | succ(k) using ih =>
    intros values covered
    have prefix : ∀ j ∈ k, Occurs(f, n, g(j)) ∨ w(g(j)) = one
      intros j before
      have included := membership.into_successor at j, k with *
      exact covered with j, included
    have last := covered with k, membership.self_successor at k with *
    have valuePrefix := WeightedValues.prefix at w, g, A, k with *
    have valueLast := WeightedValues.last at w, g, A, k with *
    have row := matchingProductRow.covered_or_one at A, add, zero, neg, mul, one, w, f, g(k), n with *
    have previous := ih with valuePrefix, prefix
    rw [matchingProductTotal, indexedRingProduct, previous, row]
    rfl

theorem indexedRingProduct.same_nonunit_entries (f g : Set, n m : Nat)
  requires valuesF : WeightedValues(w, f, A, n)
  requires valuesG : WeightedValues(w, g, A, m)
  requires distinctF : DistinctValues(f, n)
  requires distinctG : DistinctValues(g, m)
  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = one
  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = one
  shows indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(w, g, mul, one, m)
proof
  have left := matchingProductTotal.support_product at A, add, zero, neg, mul, one, w, g, f, m, n with *, valuesF, coveredF
  have right := matchingProductTotal.support_product at A, add, zero, neg, mul, one, w, f, g, n, m with *, valuesG, coveredG
  have transpose := matchingProductTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *
  rw [← left, ← right]
  symm
  exact transpose with valuesF

end Rings

theorem finiteRingProduct.restrict (V S A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : V → A
  requires subset : S ⊆ V
  requires neutral : ∀ x ∈ V, ¬(x ∈ S) → w(x) = one
  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) =
    finiteRingProduct(S, A, add, zero, neg, mul, one, restrict(w, S))
proof
  have finiteS := Finite.subset with finite, subset
  have closed : ∀ x ∈ S, w(x) ∈ A
    intros x hx
    have included := subset
    have member := included with x, hx
    exact FunctionBetween.apply_closed with *
  have restricted := restrict.function with *
  have selectedV := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *
  have selectedS := finiteRingProduct.selected at S, A, add, zero, neg, mul, one, restrict(w, S) with *
  obtain ⟨n, naturalN, f, enumerationF, equationV⟩ := selectedV.right
  obtain ⟨m, naturalM, g, enumerationG, equationS⟩ := selectedS.right
  have injF := Bijective.injective with enumerationF
  have injG := Bijective.injective with enumerationG
  have surjF := Bijective.surjective with enumerationF
  have surjG := Bijective.surjective with enumerationG
  have functionF := Injective.function with injF
  have functionG := Injective.function with injG
  have distinctF := Injective.distinct_values with injF
  have distinctG := Injective.distinct_values with injG
  have valuesF := WeightedValues.of_functions with weights, functionF
  have valuesG : WeightedValues(w, g, A, m)
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact closed with g(i), member
  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = one
    intros i hi
    have member := FunctionBetween.apply_closed with *
    have alternatives : f(i) ∈ S ∨ ¬(f(i) ∈ S) by tauto
    cases alternatives with inside | outside
    . left
      exact Surjective.occurs with *
    . right
      exact neutral with f(i), member, outside
  have coveredG : ∀ i ∈ m, Occurs(f, n, g(i)) ∨ w(g(i)) = one
    intros i hi
    have inS := FunctionBetween.apply_closed with *
    have included := subset
    have inV := included with g(i), inS
    left
    exact Surjective.occurs with *
  have same := indexedRingProduct.same_nonunit_entries with valuesF, valuesG, distinctF, distinctG, coveredF, coveredG
  have pointwise : ∀ i ∈ m, w(g(i)) = restrict(w, S)(g(i))
    intros i hi
    have inS := FunctionBetween.apply_closed with *
    symm
    exact restrict.apply with *
  have congr := indexedRingProduct.congr at w, restrict(w, S), g, g, mul, one, m with naturalM
  have equal := congr with pointwise
  cc

theorem finiteRingProduct.reindex (D E A add zero neg mul one w v f : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : E → A
  requires bijective : BijectiveBetween(f, D, E)
  requires values : ∀ d ∈ D, w(d) = v(f(d))
  shows finiteRingProduct(D, A, add, zero, neg, mul, one, w) = finiteRingProduct(E, A, add, zero, neg, mul, one, v)
proof
  have selected := finiteRingProduct.selected at D, A, add, zero, neg, mul, one, w with *
  obtain ⟨n, natural, g, enumeration, equation⟩ := selected.right
  have composed := compose.bijective at f, g, n, D, E with *
  have injF := Bijective.injective with bijective
  have injG := Bijective.injective with enumeration
  have functionF := Injective.function with injF
  have functionG := Injective.function with injG
  have equationV := finiteRingProduct.enumeration at E, A, add, zero, neg, mul, one, v, compose(f, g, n, D, E), n with *
  have pointwise : ∀ i ∈ n, w(g(i)) = v(compose(f, g, n, D, E)(i))
    intros i hi
    have member := FunctionBetween.apply_closed at g, n, D, i with *
    have value := values with g(i), member
    have composite := compose.apply at f, g, n, D, E, i with *
    cc
  have congr := indexedRingProduct.congr at w, v, g, compose(f, g, n, D, E), mul, one, n with natural
  have same := congr with pointwise
  cc

-- The smaller-domain weights may be represented by any agreeing graph.
theorem finiteRingProduct.unit_extension (D S A add zero neg mul one w v : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : S → A
  requires subset : S ⊆ D
  requires agreement : ∀ s ∈ S, w(s) = v(s)
  requires neutral : ∀ d ∈ D, ¬(d ∈ S) → w(d) = one
  shows finiteRingProduct(D, A, add, zero, neg, mul, one, w) = finiteRingProduct(S, A, add, zero, neg, mul, one, v)
proof
  have closed : ∀ s ∈ S, w(s) ∈ A
    intros s hs
    have value := FunctionBetween.apply_closed with *
    have equal := agreement with s, hs
    rwa equal
  have restricted := restrict.function with *
  have same : restrict(w, S) = v
    apply FunctionBetween.ext with restricted, weightsV
    intros s hs
    have value := restrict.apply with *
    have equal := agreement with s, hs
    cc
  have product := finiteRingProduct.restrict with *
  rwa same at product


theorem finiteRingProduct.empty (A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : ∅ → A
  shows finiteRingProduct(∅, A, add, zero, neg, mul, one, w) = one
proof
  have finite := Finite.empty
  have values : ∀ x ∈ ∅, w(x) = one
    intros x impossible
    exfalso
    exact set.empty with impossible
  exact finiteRingProduct.one with ring, finite, weights, values

theorem finiteRingProduct.insert (V A add zero neg mul one w a : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : insert(a, V) → A
  requires fresh : ¬(a ∈ V)
  shows finiteRingProduct(insert(a, V), A, add, zero, neg, mul, one, w) =
    call2(mul, finiteRingProduct(V, A, add, zero, neg, mul, one, restrict(w, V)), w(a))
proof
  have subset : V ⊆ insert(a, V)
    intros x hx
    exact insert.contains with hx
  have closed : ∀ x ∈ V, w(x) ∈ A
    intros x hx
    have member := insert.contains at x, a, V with hx
    exact FunctionBetween.apply_closed at w, insert(a, V), A, x with *
  have restricted := restrict.function at w, insert(a, V), A, V, A with *
  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, restrict(w, V) with *
  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have nFresh := membership.irreflexive at n
  have extended := adjoinMap.bijective with enumeration, nFresh, fresh
  have successor := natural.successor_as_insert with natural
  rw ← successor at extended
  have extendedInjective := Bijective.injective with extended
  have extendedFunction := Injective.function with extendedInjective
  have extendedProduct := finiteRingProduct.enumeration at insert(a, V), A, add, zero, neg, mul, one, w, adjoinMap(f, n, a), succ(n) with *
  have oldValues : ∀ i ∈ n, w(adjoinMap(f, n, a)(i)) = restrict(w, V)(f(i))
    intros i hi
    have oldMember := FunctionBetween.apply_closed at f, n, V, i with *
    have oldEdge := FunctionBetween.relates_apply at f, n, V, i with *
    have edge := adjoinMap.relates_old at f, n, a, i, f(i) with oldEdge
    have next := membership.into_successor at i, n with *
    have value := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), i, f(i) with *
    have restrictedValue := restrict.apply at w, insert(a, V), A, V, A, f(i) with *
    cc
  have congr := indexedRingProduct.congr at w, restrict(w, V), adjoinMap(f, n, a), f, mul, one, n with natural
  have prefix := congr with oldValues
  have newIndex := membership.self_successor with natural
  have newEdge := adjoinMap.relates_new at f, n, a
  have newValue := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), n, a with *
  rw [extendedProduct, indexedRingProduct, prefix, newValue, equation]
  rfl

theorem finiteRingProduct.singleton (A add zero neg mul one w x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : {x} → A
  shows finiteRingProduct({x}, A, add, zero, neg, mul, one, w) = w(x)
proof
  have same : insert(x, ∅) = {x}
    ext y
    simp
  have empty := Finite.empty
  have fresh : ¬(x ∈ ∅) by exact set.empty at x
  have extended : w : insert(x, ∅) → A by rwa same
  have subset : ∅ ⊆ insert(x, ∅) by simp [Subset, set.empty]
  have closed : ∀ y ∈ ∅, w(y) ∈ A
    intros y hy
    exfalso
    exact set.empty with hy
  have restricted := restrict.function with *
  have emptyProduct := finiteRingProduct.empty with *
  have inserted := finiteRingProduct.insert with *
  have member : x ∈ {x} by simp [singleton.membership]
  have value := FunctionBetween.apply_closed with *
  rw same at inserted
  rw [inserted, emptyProduct]
  ring

theorem finiteRingProduct.mul (D A add zero neg mul one w v h : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : D → A
  requires weightsH : h : D → A
  requires equations : ∀ x ∈ D, h(x) = call2(mul, w(x), v(x))
  shows finiteRingProduct(D, A, add, zero, neg, mul, one, h) = call2(mul, finiteRingProduct(D, A, add, zero, neg, mul, one, w), finiteRingProduct(D, A, add, zero, neg, mul, one, v))
proof
  have selected := finiteRingProduct.selected at D, A, add, zero, neg, mul, one, w with *
  obtain ⟨n, natural, f, enumeration, valueW⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have valuesW := WeightedValues.of_functions with weightsW, function
  have valuesV := WeightedValues.of_functions with weightsV, function
  have valueV := finiteRingProduct.enumeration at D, A, add, zero, neg, mul, one, v, f, n with *
  have valueH := finiteRingProduct.enumeration at D, A, add, zero, neg, mul, one, h, f, n with *
  have pointwise : ∀ i ∈ n, h(f(i)) = call2(mul, w(f(i)), v(f(i)))
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact equations with f(i), member
  have multiply := indexedRingProduct.mul with *, valuesW, valuesV, pointwise
  cc