Grace/Cumulus/Cardinal/NaturalSumLaws.g17

Open in Workbench Download source

Imports

Pigeonhole

Declarations

Source

1-- Sums of naturals over finite sets: disjoint unions add, removing a point2-- takes its weight off, a subset sums to no more, the sums over a point and3-- over a pair, reindexing along a bijection, and the sum of w(d) · u(e) over4-- a product set as the product of the two sums5-- 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.Cardinal.NaturalSumLaws11import Pigeonhole1213-- The weighted pairs of a subset, of a union, and of disjoint sets.14theorem weightedPairs.monotone (S T w : Set)15  requires subset : S ⊆ T16  shows weightedPairs(S, w) ⊆ weightedPairs(T, w)17proof18  intros p hp19  have parts := weightedPairs.membership.forward with hp20  obtain ⟨v, hv, i, hi, shape⟩ := parts.right21  have bound := parts.left22  rw shape at bound23  have coordinates := product.pair_membership.forward with bound24  have hvT := subset with v, hv25  have boundT : p ∈ T × ℕ26    rw shape27    exact product.pair with hvT, coordinates.right28  exact weightedPairs.membership.backward with29    ⟨boundT, v, hvT, i, hi, shape⟩3031theorem weightedPairs.union (A B w : Set)32  shows weightedPairs(A ∪ B, w) = weightedPairs(A, w) ∪ weightedPairs(B, w)33proof34  have leftSubset := union2.subset_left at A, B35  have rightSubset := union2.subset_right at A, B36  have leftInside := weightedPairs.monotone at A, A ∪ B, w with leftSubset37  have rightInside := weightedPairs.monotone at B, A ∪ B, w with rightSubset38  ext p39  constructor40  . intro hp41    have parts := weightedPairs.membership.forward with hp42    obtain ⟨v, hv, i, hi, shape⟩ := parts.right43    have bound := parts.left44    rw shape at bound45    have coordinates := product.pair_membership.forward with bound46    have split := union2.membership.forward with hv47    apply union2.membership.backward48    cases split with inA | inB49    . left50      have boundA : p ∈ A × ℕ51        rw shape52        exact product.pair with inA, coordinates.right53      exact weightedPairs.membership.backward with54        ⟨boundA, v, inA, i, hi, shape⟩55    . right56      have boundB : p ∈ B × ℕ57        rw shape58        exact product.pair with inB, coordinates.right59      exact weightedPairs.membership.backward with60        ⟨boundB, v, inB, i, hi, shape⟩61  . intro hp62    have split := union2.membership.forward with hp63    cases split with inA | inB64    . exact leftInside with p, inA65    . exact rightInside with p, inB6667theorem weightedPairs.disjoint (A B w : Set)68  requires disjoint : Disjoint(A, B)69  shows Disjoint(weightedPairs(A, w), weightedPairs(B, w))70proof71  have apart := Disjoint.iff.forward with disjoint72  apply Disjoint.iff.backward73  intros p hp hp274  have parts := weightedPairs.membership.forward with hp75  obtain ⟨v, hv, i, hi, shape⟩ := parts.right76  have parts2 := weightedPairs.membership.forward with hp277  obtain ⟨u, hu, j, hj, shape2⟩ := parts2.right78  rw shape at shape279  have coordinates := orderedPair.injective with shape280  have same := coordinates.left81  have notB := apart with v, hv82  rw ← same at hu83  exact notB with hu8485-- Disjoint unions add up.86theorem natSum.union_disjoint (A B w : Set)87  requires finiteA : Finite(A)88  requires finiteB : Finite(B)89  requires weightsA : ∀ v ∈ A, w(v) ∈ ℕ90  requires weightsB : ∀ v ∈ B, w(v) ∈ ℕ91  requires disjoint : Disjoint(A, B)92  shows natSum(A ∪ B, w) = natSum(A, w) + natSum(B, w)93proof94  have sizeA : cardinality(A) = cardinality(A) by rfl95  have sizeB : cardinality(B) = cardinality(B) by rfl96  have correctA := cardinality.correct with finiteA97  have cardNatA := correctA.left98  have correctB := cardinality.correct with finiteB99  have cardNatB := correctB.left100  have pairsA := weightedPairs.finite with finiteA, sizeA, weightsA101  have pairsB := weightedPairs.finite with finiteB, sizeB, weightsB102  have apart := weightedPairs.disjoint at A, B, w with disjoint103  have added := cardinality.union_disjoint with pairsA, pairsB, apart104  have split := weightedPairs.union at A, B, w105  unfold natSum106  rw split107  exact added108109-- Removing a point from the index set takes its weight off the sum.110theorem natSum.remove (V w a : Set)111  requires finite : Finite(V)112  requires member : a ∈ V113  requires weights : ∀ v ∈ V, w(v) ∈ ℕ114  shows natSum(V, w) = natSum(V ∖ {a}, w) + w(a)115proof116  have restSubset := difference.subset_left at V, {a}117  have restFinite := Finite.difference at V, {a} with finite118  have restWeights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ119    intros v hv120    exact weights with v, (restSubset with v, hv)121  have weight := weights with a, member122  have fresh : ¬a ∈ V ∖ {a} by simp123  have inserted := natSum.insert with restFinite, restWeights, weight, fresh124  rwa (insert.restore with member) at inserted125126-- A subset sums to no more.127theorem natSum.monotone (S T w : Set)128  requires finite : Finite(T)129  requires subset : S ⊆ T130  requires weights : ∀ v ∈ T, w(v) ∈ ℕ131  shows natSum(S, w) ≤ natSum(T, w)132proof133  have size : cardinality(T) = cardinality(T) by rfl134  have correct := cardinality.correct with finite135  have cardNat := correct.left136  have pairsFinite := weightedPairs.finite with finite, size, weights137  have inside := weightedPairs.monotone at S, T, w with subset138  have bounded := cardinality.monotone with pairsFinite, inside139  simp [natSum]140141-- The sum over a point and over a pair.142theorem natSum.singleton (w a : Set)143  requires weight : w(a) ∈ ℕ144  shows natSum({a}, w) = w(a)145proof146  have asInsert : {a} = insert(a, ∅)147    ext x148    simp [insert.membership]149  have finite := Finite.empty150  have weights : ∀ v ∈ ∅, w(v) ∈ ℕ151    intros v hv152    exfalso153    exact empty.membership with v, hv154  have fresh : ¬a ∈ ∅ := empty.membership at a155  have inserted := natSum.insert with finite, weights, weight, fresh156  have weightNat := nat.omega.backward with weight157  rw [asInsert, inserted, natSum.empty]158  exact add.left_unit at w(a)159160theorem natSum.pair (w a b : Set)161  requires weightA : w(a) ∈ ℕ162  requires weightB : w(b) ∈ ℕ163  requires distinct : a ≠ b164  shows natSum({a, b}, w) = w(a) + w(b)165proof166  have asInsert : {a, b} = insert(a, {b})167    ext x168    simp [insert.membership, pair.membership]169  have finite := Finite.singleton at b170  have weights : ∀ v ∈ {b}, w(v) ∈ ℕ171    intros v hv172    have same := singleton.membership.forward with hv173    rw same174    exact weightB175  have fresh : ¬a ∈ {b}176    intro inside177    have same := singleton.membership.forward with inside178    exact distinct with same179  have inserted := natSum.insert with finite, weights, weightA, fresh180  have single := natSum.singleton with weightB181  have aNat := nat.omega.backward with weightA182  have bNat := nat.omega.backward with weightB183  rw [asInsert, inserted, single]184  exact add.commutative at w(a), w(b)185186-- A sum of vanishing weights vanishes: no weighted pair exists.187theorem natSum.zero_weights (V w : Set)188  requires zero : ∀ v ∈ V, w(v) = 0189  shows natSum(V, w) = 0190proof191  have none : weightedPairs(V, w) = ∅192    apply Subset.antisymmetric193    . intros p hp194      have parts := weightedPairs.membership.forward with hp195      obtain ⟨v, hv, i, hi, _⟩ := parts.right196      have vanish := zero with v, hv197      rw [vanish, nat.zero] at hi198      exfalso199      exact empty.membership at i with hi200    . exact empty.subset at weightedPairs(V, w)201  unfold natSum202  rw none203  exact cardinality.empty204205-- A sum may be restricted to a subset outside which the weights vanish.206theorem natSum.restrict (V S w : Set)207  requires finite : Finite(V)208  requires subset : S ⊆ V209  requires weights : ∀ v ∈ V, w(v) ∈ ℕ210  requires outside : ∀ v ∈ V ∖ S, w(v) = 0211  shows natSum(V, w) = natSum(S, w)212proof213  have finiteS := Finite.subset with finite, subset214  have restSubset := difference.subset_left at V, S215  have finiteRest := Finite.subset with finite, restSubset216  have weightsS : ∀ v ∈ S, w(v) ∈ ℕ217    intros v hv218    exact weights with v, (subset with v, hv)219  have weightsRest : ∀ v ∈ V ∖ S, w(v) ∈ ℕ220    intros v hv221    exact weights with v, (restSubset with v, hv)222  have apart : Disjoint(S, V ∖ S) := Disjoint.difference_right at V, S223  have cover : S ∪ (V ∖ S) = V := difference.union2_of_subset with subset224  have split := natSum.union_disjoint225    with finiteS, finiteRest, weightsS, weightsRest, apart226  have vanish := natSum.zero_weights at V ∖ S, w with outside227  have natural := natSum.natural with finiteS, weightsS228  have unit := add.right_unit at natSum(S, w)229  rw [cover, vanish, unit] at split230  exact split231232-- A sum of even weights is even.233theorem natSum.even_of_even_weights_of_size (w : Set, n : Nat)234  shows ∀ V, Finite(V) → cardinality(V) = n →235    (∀ v ∈ V, w(v) ∈ ℕ) → (∀ v ∈ V, Even(w(v))) →236    Even(natSum(V, w))237proof238  induction n239  | zero =>240    intros V finite size weights even241    have has := cardinality.correct with finite242    rw size at has243    have empty := HasCardinality.empty_of_zero at V with has244    rw [empty, natSum.empty]245    exact Even.zero246  | succ(k) using ih =>247    intros V finite size weights even248    have has := cardinality.correct with finite249    rw size at has250    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has251    have removed := cardinality.remove with finite, ha252    rw size at removed253    have smaller := Naturals.injective.succ with removed254    have restSize : cardinality(V ∖ {a}) = k255      symm256      exact smaller257    have restSubset := difference.subset_left at V, {a}258    have restFinite := Finite.subset with finite, restSubset259    have restWeights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ260      intros v hv261      have parts := difference.singleton_membership.forward with hv262      exact weights with v, parts.left263    have restEven : ∀ v ∈ V ∖ {a}, Even(w(v))264      intros v hv265      have parts := difference.singleton_membership.forward with hv266      exact even with v, parts.left267    have rest := ih with V ∖ {a}, restFinite, restSize, restWeights, restEven268    have fresh : ¬a ∈ V ∖ {a}269      intro inside270      have parts := difference.singleton_membership.forward with inside271      apply parts.right272      rfl273    have restore := insert.restore with ha274    have weightA := weights with a, ha275    have evenA := even with a, ha276    have inserted := natSum.insert at V ∖ {a}, w, a277      with restFinite, restWeights, weightA, fresh278    rw restore at inserted279    rw inserted280    exact Even.add with rest, evenA281282-- Reindexing: a bijection f : S → T carries the weighted pairs of the283-- pulled-back weights v(s) = w(f(s)) onto those of w.284285286-- The same for a finite set, with no size parameter.287theorem natSum.even_of_even_weights (V w : Set)288  requires finite : Finite(V)289  requires weights : ∀ v ∈ V, w(v) ∈ ℕ290  requires even : ∀ v ∈ V, Even(w(v))291  shows Even(natSum(V, w))292proof293  have correct := cardinality.correct with finite294  have natural := correct.left295  have size : cardinality(V) = cardinality(V) by rfl296  exact natSum.even_of_even_weights_of_size at w, cardinality(V)297    with natural, V, finite, size, weights, even298299defgraph reindexPairs (f S T v w : Set) (p ∈ weightedPairs(S, v)) :300    weightedPairs(T, w) := (f(fst(p)), snd(p))301requires fFunction : f : S → T302requires values : ∀ s ∈ S, v(s) = w(f(s))303proof304  have parts := weightedPairs.membership.forward with member305  obtain ⟨s, hs, i, hi, shape⟩ := parts.right306  have bound := parts.left307  rw shape at bound308  have coordinates := product.pair_membership.forward with bound309  have image := FunctionBetween.apply_closed with fFunction, hs310  have equal := values with s, hs311  rw equal at hi312  have boundT : (f(s), i) ∈ T × ℕ :=313    product.pair with image, coordinates.right314  have same : (f(s), i) = (f(s), i) by rfl315  rw [shape, fst.pair, snd.pair]316  exact weightedPairs.membership.backward with317    ⟨boundT, f(s), image, i, hi, same⟩318319theorem reindexPairs.pair (f S T v w s i : Set)320  requires fFunction : f : S → T321  requires values : ∀ s ∈ S, v(s) = w(f(s))322  requires member : (s, i) ∈ weightedPairs(S, v)323  shows reindexPairs(f, S, T, v, w)((s, i)) = (f(s), i)324proof325  have value := reindexPairs.value at f, S, T, v, w, (s, i) with fFunction,326    values, member327  rw [value, fst.pair, snd.pair]328  rfl329330theorem reindexPairs.injective (f S T v w : Set)331  requires injective : InjectiveBetween(f, S, T)332  requires values : ∀ s ∈ S, v(s) = w(f(s))333  shows InjectiveBetween(reindexPairs(f, S, T, v, w), weightedPairs(S, v),334    weightedPairs(T, w))335proof336  have fFunction := Injective.function with injective337  have function := reindexPairs.function at f, S, T, v, w with fFunction, values338  refine ⟨function, _⟩339  intros x hx y hy z hz relatesX relatesY340  have partsX := weightedPairs.membership.forward with hx341  obtain ⟨s, hs, i, hi, shapeX⟩ := partsX.right342  have partsY := weightedPairs.membership.forward with hy343  obtain ⟨t, ht, j, hj, shapeY⟩ := partsY.right344  have valueX := FunctionBetween.apply_value with function, hx, relatesX345  have valueY := FunctionBetween.apply_value with function, hy, relatesY346  rw shapeX at hx347  rw shapeY at hy348  rw shapeX at valueX349  rw shapeY at valueY350  have pairX := reindexPairs.pair with fFunction, values, hx351  have pairY := reindexPairs.pair with fFunction, values, hy352  have same : (f(s), i) = (f(t), j) by cc353  have coordinates := orderedPair.injective with same354  have imageS := FunctionBetween.relates_apply with fFunction, hs355  have imageT := FunctionBetween.relates_apply with fFunction, ht356  have imageIn := FunctionBetween.apply_closed with fFunction, hs357  rw coordinates.left at imageS358  rw coordinates.left at imageIn359  have sameInput : s = t := Injective.cancel with *360  rw [shapeX, shapeY, sameInput, coordinates.right]361  rfl362363theorem reindexPairs.surjective (f S T v w : Set)364  requires bijective : BijectiveBetween(f, S, T)365  requires values : ∀ s ∈ S, v(s) = w(f(s))366  shows SurjectiveBetween(reindexPairs(f, S, T, v, w), weightedPairs(S, v),367    weightedPairs(T, w))368proof369  have injective := Bijective.injective with bijective370  have surjective := Bijective.surjective with bijective371  have fFunction := Injective.function with injective372  have function := reindexPairs.function at f, S, T, v, w with fFunction, values373  refine ⟨function, _⟩374  intros z hz375  have parts := weightedPairs.membership.forward with hz376  obtain ⟨t, ht, j, hj, shape⟩ := parts.right377  have bound := parts.left378  rw shape at bound379  have coordinates := product.pair_membership.forward with bound380  obtain ⟨s, hs, relatesS⟩ := surjective.right with t, ht381  have image := FunctionBetween.apply_value with fFunction, hs, relatesS382  have equal := values with s, hs383  rw image at equal384  rw ← equal at hj385  have boundS : (s, j) ∈ S × ℕ := product.pair with hs, coordinates.right386  have same : (s, j) = (s, j) by rfl387  have memberS : (s, j) ∈ weightedPairs(S, v) :=388    weightedPairs.membership.backward with ⟨boundS, s, hs, j, hj, same⟩389  have value := reindexPairs.pair with fFunction, values, memberS390  have relates := FunctionBetween.relates_apply with function, memberS391  rw [value, image, ← shape] at relates392  exact ⟨(s, j), memberS, relates⟩393394theorem reindexPairs.bijective (f S T v w : Set)395  requires bijective : BijectiveBetween(f, S, T)396  requires values : ∀ s ∈ S, v(s) = w(f(s))397  shows BijectiveBetween(reindexPairs(f, S, T, v, w), weightedPairs(S, v),398    weightedPairs(T, w))399proof400  have injective := Bijective.injective with bijective401  have pairsInjective := reindexPairs.injective with injective, values402  have pairsSurjective := reindexPairs.surjective with bijective, values403  exact ⟨pairsInjective, pairsSurjective⟩404405-- The sum of w over T is the sum over S of the pulled-back weights.406theorem natSum.reindex (f S T v w : Set)407  requires finite : Finite(S)408  requires bijective : BijectiveBetween(f, S, T)409  requires weights : ∀ t ∈ T, w(t) ∈ ℕ410  requires values : ∀ s ∈ S, v(s) = w(f(s))411  shows natSum(T, w) = natSum(S, v)412proof413  have injective := Bijective.injective with bijective414  have fFunction := Injective.function with injective415  have weightsS : ∀ s ∈ S, v(s) ∈ ℕ416    intros s hs417    have equal := values with s, hs418    have image := FunctionBetween.apply_closed with fFunction, hs419    rw equal420    exact weights with f(s), image421  have size : cardinality(S) = cardinality(S) by rfl422  have correct := cardinality.correct with finite423  have cardNat := correct.left424  have pairsFinite := weightedPairs.finite with finite, size, weightsS425  have pairsBijective := reindexPairs.bijective with bijective, values426  have same := cardinality.bijective with pairsFinite, pairsBijective427  unfold natSum428  rw same429430-- The weight (d, e) ↦ w(d) · u(e) on a product set.431defgraph weightProduct (D E w u : Set) (q ∈ D × E) : ℕ :=432  w(fst(q)) * u(snd(q))433requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ434requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ435proof436  obtain ⟨bound, d, hd, e, he, shape⟩ :=437    product.membership.forward with member438  have dNat := nat.omega.backward with (weightsD with d, hd)439  have eNat := nat.omega.backward with (weightsE with e, he)440  have productNat : Nat(w(d) * u(e)) by typecheck441  rw [shape, fst.pair, snd.pair]442  exact nat.omega.forward with productNat443444theorem weightProduct.pair (D E w u d e : Set)445  requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ446  requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ447  requires hd : d ∈ D448  requires he : e ∈ E449  shows weightProduct(D, E, w, u)((d, e)) = w(d) * u(e)450proof451  have pairMember := product.pair with hd, he452  have value := weightProduct.value at D, E, w, u, (d, e) with weightsD,453    weightsE, pairMember454  rw [value, fst.pair, snd.pair]455  rfl456457-- The weighted pairs of a product: ((d, i), (e, j)) ↦ ((d, e), k) with k the458-- position of (i, j) in the enumeration of w(d) × u(e) by w(d) · u(e).459defgraph productPairs (D E w u : Set)460    (q ∈ weightedPairs(D, w) × weightedPairs(E, u)) :461    weightedPairs(D × E, weightProduct(D, E, w, u)) :=462  ((fst(fst(q)), fst(snd(q))),463    natProductEquiv(w(fst(fst(q))), u(fst(snd(q))))((snd(fst(q)), snd(snd(q)))))464requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ465requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ466proof467  obtain ⟨bound, x, hx, y, hy, shape⟩ :=468    product.membership.forward with member469  have partsX := weightedPairs.membership.forward with hx470  obtain ⟨d, hd, i, hi, shapeX⟩ := partsX.right471  have partsY := weightedPairs.membership.forward with hy472  obtain ⟨e, he, j, hj, shapeY⟩ := partsY.right473  have dNat := nat.omega.backward with (weightsD with d, hd)474  have eNat := nat.omega.backward with (weightsE with e, he)475  have equiv := natProductEquiv.bijective at u(e), w(d)476  have equivFunction := Injective.function with (Bijective.injective with equiv)477  have pairIJ := product.pair with hi, hj478  have kMember := FunctionBetween.apply_closed with equivFunction, pairIJ479  have naturals := natural.member at w(d) * u(e)480  have kNat := naturals with natProductEquiv(w(d), u(e))((i, j)), kMember481  have kIn := nat.omega.forward with kNat482  have weightValue := weightProduct.pair with weightsD, weightsE, hd, he483  rw ← weightValue at kMember484  have deMember := product.pair with hd, he485  have boundQ := product.pair with deMember, kIn486  have same : ((d, e), natProductEquiv(w(d), u(e))((i, j))) =487    ((d, e), natProductEquiv(w(d), u(e))((i, j))) by rfl488  rw [shape, shapeX, shapeY]489  simp [fst.pair, snd.pair]490  exact weightedPairs.membership.backward with491    ⟨boundQ, (d, e), deMember, natProductEquiv(w(d), u(e))((i, j)), kMember,492      same⟩493494theorem productPairs.pair (D E w u d i e j : Set)495  requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ496  requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ497  requires hx : (d, i) ∈ weightedPairs(D, w)498  requires hy : (e, j) ∈ weightedPairs(E, u)499  shows productPairs(D, E, w, u)(((d, i), (e, j))) =500    ((d, e), natProductEquiv(w(d), u(e))((i, j)))501proof502  have pairMember := product.pair with hx, hy503  have value := productPairs.value at D, E, w, u, ((d, i), (e, j)) with504    weightsD, weightsE, pairMember505  rw value506  simp [fst.pair, snd.pair]507508theorem productPairs.injective (D E w u : Set)509  requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ510  requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ511  shows InjectiveBetween(productPairs(D, E, w, u),512    weightedPairs(D, w) × weightedPairs(E, u),513    weightedPairs(D × E, weightProduct(D, E, w, u)))514proof515  have function := productPairs.function at D, E, w, u with weightsD, weightsE516  refine ⟨function, _⟩517  intros x hx y hy z hz relatesX relatesY518  obtain ⟨boundX, x1, hx1, x2, hx2, shapeX⟩ :=519    product.membership.forward with hx520  obtain ⟨boundY, y1, hy1, y2, hy2, shapeY⟩ :=521    product.membership.forward with hy522  have partsX1 := weightedPairs.membership.forward with hx1523  obtain ⟨d, hd, i, hi, shapeX1⟩ := partsX1.right524  have partsX2 := weightedPairs.membership.forward with hx2525  obtain ⟨e, he, j, hj, shapeX2⟩ := partsX2.right526  have partsY1 := weightedPairs.membership.forward with hy1527  obtain ⟨d2, hd2, i2, hi2, shapeY1⟩ := partsY1.right528  have partsY2 := weightedPairs.membership.forward with hy2529  obtain ⟨e2, he2, j2, hj2, shapeY2⟩ := partsY2.right530  have valueX := FunctionBetween.apply_value with function, hx, relatesX531  have valueY := FunctionBetween.apply_value with function, hy, relatesY532  rw shapeX1 at hx1533  rw shapeX2 at hx2534  rw shapeY1 at hy1535  rw shapeY2 at hy2536  rw [shapeX, shapeX1, shapeX2] at valueX537  rw [shapeY, shapeY1, shapeY2] at valueY538  have pairX := productPairs.pair with weightsD, weightsE, hx1, hx2539  have pairY := productPairs.pair with weightsD, weightsE, hy1, hy2540  have same : ((d, e), natProductEquiv(w(d), u(e))((i, j))) =541    ((d2, e2), natProductEquiv(w(d2), u(e2))((i2, j2))) by cc542  have outer := orderedPair.injective with same543  have inner := orderedPair.injective with outer.left544  have dEqual := inner.left545  have eEqual := inner.right546  have positions := outer.right547  rw [← dEqual, ← eEqual] at positions548  rw ← dEqual at hi2549  rw ← eEqual at hj2550  have dNat := nat.omega.backward with (weightsD with d, hd)551  have eNat := nat.omega.backward with (weightsE with e, he)552  have equiv := natProductEquiv.bijective at u(e), w(d)553  have equivInjective := Bijective.injective with equiv554  have equivFunction := Injective.function with equivInjective555  have pairIJ := product.pair with hi, hj556  have pairIJ2 := product.pair with hi2, hj2557  have relatesIJ := FunctionBetween.relates_apply with equivFunction, pairIJ558  have relatesIJ2 := FunctionBetween.relates_apply with equivFunction, pairIJ2559  have kMember := FunctionBetween.apply_closed with equivFunction, pairIJ2560  rw positions at relatesIJ561  have sameInput := Injective.cancel at natProductEquiv(w(d), u(e)),562    w(d) × u(e), w(d) * u(e), (i, j), (i2, j2),563    natProductEquiv(w(d), u(e))((i2, j2)) with equivInjective, pairIJ,564      pairIJ2, kMember, relatesIJ, relatesIJ2565  have coordinates := orderedPair.injective with sameInput566  rw [shapeX, shapeY, shapeX1, shapeX2, shapeY1, shapeY2, ← dEqual,567    ← eEqual, ← coordinates.left, ← coordinates.right]568  rfl569570theorem productPairs.surjective (D E w u : Set)571  requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ572  requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ573  shows SurjectiveBetween(productPairs(D, E, w, u),574    weightedPairs(D, w) × weightedPairs(E, u),575    weightedPairs(D × E, weightProduct(D, E, w, u)))576proof577  have function := productPairs.function at D, E, w, u with weightsD, weightsE578  refine ⟨function, _⟩579  intros z hz580  have parts := weightedPairs.membership.forward with hz581  obtain ⟨p, hp, k, hk, shape⟩ := parts.right582  obtain ⟨boundP, d, hd, e, he, shapeP⟩ :=583    product.membership.forward with hp584  have weightValue := weightProduct.pair with weightsD, weightsE, hd, he585  rw [shapeP, weightValue] at hk586  have dNat := nat.omega.backward with (weightsD with d, hd)587  have eNat := nat.omega.backward with (weightsE with e, he)588  have equiv := natProductEquiv.bijective at u(e), w(d)589  have equivSurjective := Bijective.surjective with equiv590  have equivFunction := Injective.function with (Bijective.injective with equiv)591  obtain ⟨r, hr, relatesR⟩ := equivSurjective.right with k, hk592  obtain ⟨boundR, i, hi, j, hj, shapeR⟩ :=593    product.membership.forward with hr594  have iNat := natural.member at w(d) with i, hi595  have jNat := natural.member at u(e) with j, hj596  have iIn := nat.omega.forward with iNat597  have jIn := nat.omega.forward with jNat598  have boundX := product.pair with hd, iIn599  have boundY := product.pair with he, jIn600  have sameX : (d, i) = (d, i) by rfl601  have sameY : (e, j) = (e, j) by rfl602  have memberX : (d, i) ∈ weightedPairs(D, w) :=603    weightedPairs.membership.backward with ⟨boundX, d, hd, i, hi, sameX⟩604  have memberY : (e, j) ∈ weightedPairs(E, u) :=605    weightedPairs.membership.backward with ⟨boundY, e, he, j, hj, sameY⟩606  have memberQ := product.pair with memberX, memberY607  have value := productPairs.pair with weightsD, weightsE, memberX, memberY608  have kValue := FunctionBetween.apply_value with equivFunction, hr, relatesR609  rw shapeR at kValue610  have relates := FunctionBetween.relates_apply with function, memberQ611  rw [value, kValue, ← shapeP, ← shape] at relates612  exact ⟨((d, i), (e, j)), memberQ, relates⟩613614theorem productPairs.bijective (D E w u : Set)615  requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ616  requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ617  shows BijectiveBetween(productPairs(D, E, w, u),618    weightedPairs(D, w) × weightedPairs(E, u),619    weightedPairs(D × E, weightProduct(D, E, w, u)))620proof621  have injective := productPairs.injective with weightsD, weightsE622  have surjective := productPairs.surjective with weightsD, weightsE623  exact ⟨injective, surjective⟩624625-- The sum of w(d) · u(e) over D × E is the product of the two sums.626theorem natSum.product (D E w u : Set)627  requires finiteD : Finite(D)628  requires finiteE : Finite(E)629  requires weightsD : ∀ d ∈ D, w(d) ∈ ℕ630  requires weightsE : ∀ e ∈ E, u(e) ∈ ℕ631  shows natSum(D × E, weightProduct(D, E, w, u)) = natSum(D, w) * natSum(E, u)632proof633  have sizeD : cardinality(D) = cardinality(D) by rfl634  have sizeE : cardinality(E) = cardinality(E) by rfl635  have correctD := cardinality.correct with finiteD636  have cardNatD := correctD.left637  have correctE := cardinality.correct with finiteE638  have cardNatE := correctE.left639  have pairsD := weightedPairs.finite with finiteD, sizeD, weightsD640  have pairsE := weightedPairs.finite with finiteE, sizeE, weightsE641  have pairsFinite := Finite.product with pairsD, pairsE642  have bijective := productPairs.bijective with weightsD, weightsE643  have same := cardinality.bijective with pairsFinite, bijective644  have countD := cardinality.correct with pairsD645  have countE := cardinality.correct with pairsE646  have countProduct := HasCardinality.product with countD, countE647  have productValue := cardinality.eq_of_has with countProduct648  unfold natSum649  rw [← same, productValue]650  rfl651