-- The sum over a product set is the double sum: push forward along the
-- first projection, and each fibre {x} × Y is a copy of Y
-- 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.ProductSetSum
import Regrouping
import FiniteDoubleSum

theorem finiteRingSum.product_set (X Y A add zero neg mul one u : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finiteX : Finite(X)
  requires finiteY : Finite(Y)
  requires matrix : u : X × Y → A
  shows finiteRingSum(X × Y, A, add, zero, neg, mul, one, u) =
    finiteDoubleSum(X, Y, A, add, zero, neg, mul, one, u)
proof
  have finiteXY := Finite.product with finiteX, finiteY
  have projection := firstProjection.function at X, Y
  have ordinary := IsCommRing.ring with ring
  have zeroIn : zero ∈ A := IsRing.zero_in_carrier with ordinary
  have push := finitePushforward.sum at X × Y, X, A, add, zero, neg, mul, one,
    firstProjection(X, Y), u with ring, matrix, finiteXY, finiteX, projection
  have pushFunction := finitePushforward.function at X × Y, X, A, add, zero, neg, mul, one,
    firstProjection(X, Y), u with ring, finiteXY, matrix
  have rows := finiteRowSums.function at X, Y, A, add, zero, neg, mul, one, u
    with ring, finiteY, matrix
  have values : ∀ x ∈ X,
      finitePushforward(X × Y, X, A, add, zero, neg, mul, one, firstProjection(X, Y), u)(x) =
      finiteRowSums(X, Y, A, add, zero, neg, mul, one, u)(x)
    intros x hx
    have pushValue := finitePushforward.value at X × Y, X, A, add, zero, neg, mul, one,
      firstProjection(X, Y), u, x with ring, finiteXY, matrix, hx
    have rowValue := finiteRowSums.value at X, Y, A, add, zero, neg, mul, one, u, x
      with ring, finiteY, matrix, hx
    have pushWeights := pushforwardWeights.function at X × Y, A, add, zero, neg, mul, one,
      firstProjection(X, Y), u, x with ring, matrix
    have rowWeights := finiteRowWeights.function at X, Y, A, u, x with matrix, hx
    have fibreSubset : {x} × Y ⊆ X × Y
      intros p hp
      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp
      have aIs := singleton.membership.forward with ha
      rw [shape, aIs]
      exact product.pair with hx, hy
    have fibreWeights := restrict.domain_function at u, X × Y, A, {x} × Y with matrix, fibreSubset
    have agreement : ∀ p ∈ {x} × Y,
        pushforwardWeights(X × Y, A, add, zero, neg, mul, one, firstProjection(X, Y), u, x)(p) =
        restrict(u, {x} × Y)(p)
      intros p hp
      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp
      have aIs := singleton.membership.forward with ha
      have inXY := fibreSubset with p, hp
      have weight := pushforwardWeights.value at X × Y, A, add, zero, neg, mul, one,
        firstProjection(X, Y), u, x, p with ring, matrix, inXY
      have restricted := restrict.domain_apply at u, X × Y, A, {x} × Y, p
        with matrix, fibreSubset, hp
      have first : firstProjection(X, Y)(p) = x
        rw [shape, aIs]
        exact firstProjection.pair at X, Y, x, y with hx, hy
      have coefficient := FunctionBetween.apply_closed with matrix, inXY
      symm at first
      have same := singleValue.same at A, zero, u(p), firstProjection(X, Y)(p), x
        with zeroIn, coefficient, first
      rw [weight, restricted, same]
      rfl
    have vanishing : ∀ p ∈ X × Y, ¬(p ∈ {x} × Y) →
        pushforwardWeights(X × Y, A, add, zero, neg, mul, one, firstProjection(X, Y), u, x)(p) =
        zero
      intros p hp outside
      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp
      have weight := pushforwardWeights.value at X × Y, A, add, zero, neg, mul, one,
        firstProjection(X, Y), u, x, p with ring, matrix, hp
      have first : firstProjection(X, Y)(p) = a
        rw shape
        exact firstProjection.pair at X, Y, a, y with ha, hy
      have different : x ≠ firstProjection(X, Y)(p)
        intro equal
        rw [first] at equal
        have inFibre : p ∈ {x} × Y
          rw [shape, equal]
          exact product.pair with (singleton.self at a), hy
        exact outside with inFibre
      have coefficient := FunctionBetween.apply_closed with matrix, hp
      have other := singleValue.other at A, zero, u(p), firstProjection(X, Y)(p), x
        with zeroIn, coefficient, different
      rw [weight, other]
      rfl
    have fibreSum := finiteRingSum.zero_extension at X × Y, {x} × Y, A, add, zero, neg, mul, one,
      pushforwardWeights(X × Y, A, add, zero, neg, mul, one, firstProjection(X, Y), u, x),
      restrict(u, {x} × Y) with ring, finiteXY, pushWeights, fibreWeights, fibreSubset,
      agreement, vanishing
    have finiteFibre := Finite.subset with finiteXY, fibreSubset
    have copy := secondProjection.bijective_singleton at x, Y
    have copyValues : ∀ p ∈ {x} × Y, restrict(u, {x} × Y)(p) =
        finiteRowWeights(X, Y, A, u, x)(secondProjection({x}, Y)(p))
      intros p hp
      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp
      have aIs := singleton.membership.forward with ha
      have restricted := restrict.domain_apply at u, X × Y, A, {x} × Y, p
        with matrix, fibreSubset, hp
      have second : secondProjection({x}, Y)(p) = y
        rw shape
        exact secondProjection.pair at {x}, Y, a, y with ha, hy
      have rowWeight := finiteRowWeights.value at X, Y, A, u, x, y with matrix, hx, hy
      rw [restricted, second, rowWeight, shape, aIs]
      rfl
    have reindexed := finiteRingSum.reindex at {x} × Y, Y, A, add, zero, neg, mul, one,
      restrict(u, {x} × Y), finiteRowWeights(X, Y, A, u, x), secondProjection({x}, Y)
      with ring, finiteFibre, fibreWeights, rowWeights, copy, copyValues
    rw [pushValue, rowValue, fibreSum, reindexed]
    rfl
  have congruent := finiteRingSum.congr at X, A, add, zero, neg, mul, one,
    finitePushforward(X × Y, X, A, add, zero, neg, mul, one, firstProjection(X, Y), u),
    finiteRowSums(X, Y, A, add, zero, neg, mul, one, u)
    with ring, finiteX, pushFunction, rows, values
  unfold finiteDoubleSum
  rw [← push, congruent]
  rfl