Grace/Cumulus/Cardinal/Product.g17

Open in Workbench Download source

Imports

Sum

Declarations

Source

1-- Cartesian products and cardinal multiplication2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.Product8import Sum910-- The direct product of two set-valued function graphs. The graph is a11-- bounded Separation subset of (A × B) × (C × D).12def productMap (f g A B C D : Set) : Set := { p ∈ (A × B) × (C × D) | ∃ x ∈ A, ∃ y ∈ B, ∃ z ∈ C, ∃ w ∈ D, relates(f, x, z) ∧ relates(g, y, w) ∧ p = ((x, y) ↦ (z, w)) }1314theorem productMap.relates (f g A B C D x y z w : Set)15  requires hx : x ∈ A16  requires hy : y ∈ B17  requires hz : z ∈ C18  requires hw : w ∈ D19  requires hf : relates(f, x, z)20  requires hg : relates(g, y, w)21  shows relates(productMap(f, g, A, B, C, D), (x, y), (z, w))22proof23  simp [relates, productMap.membership, product.pair]2425theorem productMap.factors (f g A B C D u v : Set)26  requires h : relates(productMap(f, g, A, B, C, D), u, v)27  shows ∃ x ∈ A, ∃ y ∈ B, ∃ z ∈ C, ∃ w ∈ D, u = (x, y) ∧ v = (z, w) ∧ relates(f, x, z) ∧ relates(g, y, w)28proof29  unfold relates at h30  obtain ⟨bounded, x, hxA, y, hyB, z, hzC, w, hwD, hf, hg, pairShape⟩ := productMap.membership.forward with h31  obtain (source, target) := orderedPair.injective with pairShape32  refine ⟨x, hxA, y, hyB, z, hzC, w, hwD, source, target, hf, hg⟩3334theorem productMap.relation (f g A B C D : Set)35  shows RelationBetween(productMap(f, g, A, B, C, D), A × B, C × D)36proof37  simp [RelationBetween, Subset]3839theorem productMap.total (f g A B C D : Set)40  requires hf : f : A → C41  requires hg : g : B → D42  shows TotalBetween(productMap(f, g, A, B, C, D), A × B, C × D)43proof44  intros u hu45  obtain ⟨sourceBound, x, hxA, y, hyB, sourceShape⟩ := product.membership.forward with hu46  obtain ⟨z, hzC, hfxz⟩ := FunctionBetween.exists_value with hf, hxA47  obtain ⟨w, hwD, hgyw⟩ := FunctionBetween.exists_value with hg, hyB48  witness (z, w)49  constructor50  . have targetPair := product.pair at z, w, C, D51    exact targetPair with hzC, hwD52  . rw sourceShape53    exact productMap.relates with hxA, hyB, hzC, hwD, hfxz, hgyw5455theorem productMap.functional (f g A B C D : Set)56  requires hf : f : A → C57  requires hg : g : B → D58  shows Functional(productMap(f, g, A, B, C, D))59proof60  intros u v huv q huq61  obtain ⟨x1, hx1A, y1, hy1B, z1, hz1C, w1, hw1D, source1, target1, hfxz1, hgyw1⟩ := productMap.factors with huv62  obtain ⟨x2, hx2A, y2, hy2B, z2, hz2C, w2, hw2D, source2, target2, hfxz2, hgyw2⟩ := productMap.factors with huq63  rw source1 at source264  obtain (sameX, sameY) := orderedPair.injective with source265  rw ← sameX at hfxz266  rw ← sameY at hgyw267  have fUnique := FunctionBetween.functional with hf, x1, z1, hfxz1, z2, hfxz268  have gUnique := FunctionBetween.functional with hg, y1, w1, hgyw1, w2, hgyw269  rw [target1, target2, fUnique, gUnique]70  rfl7172theorem productMap.function (f g A B C D : Set)73  requires hf : f : A → C74  requires hg : g : B → D75  shows productMap(f, g, A, B, C, D) : A × B → C × D76proof77  constructor78  . exact productMap.relation at f, g, A, B, C, D79  . constructor80    . have functional := productMap.functional at f, g, A, B, C, D81      exact functional with hf, hg82    . exact productMap.total with hf, hg8384theorem productMap.apply (f g A B C D x y : Set)85  requires functionF : f : A → C86  requires functionG : g : B → D87  requires hx : x ∈ A88  requires hy : y ∈ B89  shows productMap(f, g, A, B, C, D)((x, y)) = (f(x), g(y))90proof91  have function := productMap.function with functionF, functionG92  have input := product.pair with hx, hy93  have valueF := FunctionBetween.apply_closed with hx94  have valueG := FunctionBetween.apply_closed with hy95  have output := product.pair with valueF, valueG96  have edgeF := FunctionBetween.relates_apply with hx97  have edgeG := FunctionBetween.relates_apply with hy98  have edge := productMap.relates with hx, hy99  exact FunctionBetween.apply_value with *100101theorem productMap.injective (f g A B C D : Set)102  requires hf : InjectiveBetween(f, A, C)103  requires hg : InjectiveBetween(g, B, D)104  shows InjectiveBetween(productMap(f, g, A, B, C, D), A × B, C × D)105proof106  constructor107  . have fFunction := Injective.function with hf108    have gFunction := Injective.function with hg109    exact productMap.function with fFunction, gFunction110  . intros u hu v hv q hq huq hvq111    obtain ⟨x1, hx1A, y1, hy1B, z1, hz1C, w1, hw1D, source1, target1, hfxz1, hgyw1⟩ := productMap.factors with huq112    obtain ⟨x2, hx2A, y2, hy2B, z2, hz2C, w2, hw2D, source2, target2, hfxz2, hgyw2⟩ := productMap.factors with hvq113    rw target1 at target2114    obtain (sameZ, sameW) := orderedPair.injective with target2115    rw ← sameZ at hfxz2116    rw ← sameW at hgyw2117    have sameX := Injective.cancel with hf, hx1A, hx2A, hz1C, hfxz1, hfxz2118    have sameY := Injective.cancel with hg, hy1B, hy2B, hw1D, hgyw1, hgyw2119    rw [source1, source2, sameX, sameY]120    rfl121122theorem productMap.surjective (f g A B C D : Set)123  requires hf : SurjectiveBetween(f, A, C)124  requires hg : SurjectiveBetween(g, B, D)125  shows SurjectiveBetween(productMap(f, g, A, B, C, D), A × B, C × D)126proof127  constructor128  . have fFunction := Surjective.function with hf129    have gFunction := Surjective.function with hg130    exact productMap.function with fFunction, gFunction131  . intros q hq132    obtain ⟨targetBound, z, hzC, w, hwD, targetShape⟩ := product.membership.forward with hq133    rcases hf with (fFunctionAgain, fOnto)134    specialize fOnto with z, hzC135    obtain ⟨x, hxA, hfxz⟩ := fOnto136    rcases hg with (gFunctionAgain, gOnto)137    specialize gOnto with w, hwD138    obtain ⟨y, hyB, hgyw⟩ := gOnto139    witness (x, y)140    constructor141    . have sourcePair := product.pair at x, y, A, B142      exact sourcePair with hxA, hyB143    . rw targetShape144      exact productMap.relates with hxA, hyB, hzC, hwD, hfxz, hgyw145146theorem productMap.bijective (f g A B C D : Set)147  requires hf : BijectiveBetween(f, A, C)148  requires hg : BijectiveBetween(g, B, D)149  shows BijectiveBetween(productMap(f, g, A, B, C, D), A × B, C × D)150proof151  --! Split the product bijection into its two obligations.152  --| Each coordinate is transported by its own set-valued graph.153  constructor154  . --! Injectivity coordinatewise155    have fInjective := Bijective.injective with hf156    have gInjective := Bijective.injective with hg157    exact productMap.injective with fInjective, gInjective158  . --! Surjectivity coordinatewise159    have fSurjective := Bijective.surjective with hf160    have gSurjective := Bijective.surjective with hg161    exact productMap.surjective with fSurjective, gSurjective162163theorem Equipotent.product (A B C D : Set)164  requires hAC : A ≃ C165  requires hBD : B ≃ D166  shows (A × B) ≃ (C × D)167proof168  obtain (f, hf) := hAC169  obtain (g, hg) := hBD170  witness productMap(f, g, A, B, C, D)171  exact productMap.bijective with hf, hg172173theorem product.zero_left (A : Set)174  shows 0 × A = 0175proof176  ext p177  constructor178  . intro hp179    obtain ⟨bounded, x, hxZero, rest⟩ := product.membership.forward with hp180    rw nat.zero at hxZero181    simp182  . intro hp183    rw nat.zero at hp184    simp185186-- Adding the new point m to the first factor adds one complete row. This187-- graph separates the old rectangle from that row by the existing sum tags.188def productStepMap (m n : Set) : Set := { p ∈ (succ(m) × n) × ((m × n) ⊎ n) | (∃ x ∈ m, ∃ y ∈ n, p = ((x, y) ↦ inl((x, y)))) ∨ (∃ y ∈ n, p = ((m, y) ↦ inr(y))) }189190theorem productStepMap.relates_old {m : Nat} (n x y : Set)191  requires hx : x ∈ m192  requires hy : y ∈ n193  shows relates(productStepMap(m, n), (x, y), inl((x, y)))194proof195  unfold relates196  apply productStepMap.membership.backward197  constructor198  . apply product.pair at (x, y), inl((x, y)), succ(m) × n, (m × n) ⊎ n199    . apply product.pair at x, y, succ(m), n200      . apply membership.successor_set{n := m}.backward at x201        left202        exact hx203      . exact hy204    . have pairMember := product.pair with hx, hy205      exact disjointSum.left with pairMember206  . left207    refine ⟨x, hx, y, hy, rfl⟩208209theorem productStepMap.relates_new {m : Nat} (n y : Set)210  requires hy : y ∈ n211  shows relates(productStepMap(m, n), (m, y), inr(y))212proof213  unfold relates214  apply productStepMap.membership.backward215  constructor216  . apply product.pair at (m, y), inr(y), succ(m) × n, (m × n) ⊎ n217    . apply product.pair at m, y, succ(m), n218      . apply membership.successor_set{n := m}.backward at m219        right220        rfl221      . exact hy222    . have tagged := disjointSum.right at y, m × n, n223      exact tagged with hy224  . right225    refine ⟨y, hy, rfl⟩226227theorem productStepMap.factors (m n u v : Set)228  requires h : relates(productStepMap(m, n), u, v)229  shows (∃ x ∈ m, ∃ y ∈ n, u = (x, y) ∧ v = inl((x, y))) ∨ (∃ y ∈ n, u = (m, y) ∧ v = inr(y))230proof231  unfold relates at h232  obtain (bounded, alternatives) := productStepMap.membership.forward with h233  cases alternatives with old | newest234  . obtain (x, hx) := old235    rcases hx with ⟨hxM, y, hyN, pairShape⟩236    obtain (source, target) := orderedPair.injective with pairShape237    left238    refine ⟨x, hxM, y, hyN, source, target⟩239  . obtain (yNew, hyNew) := newest240    rcases hyNew with (hyNewN, pairShapeNew)241    obtain (sourceNew, targetNew) := orderedPair.injective with pairShapeNew242    right243    refine ⟨yNew, hyNewN, sourceNew, targetNew⟩244245theorem productStepMap.relation (m n : Set)246  shows RelationBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)247proof248  simp [RelationBetween, Subset]249250theorem productStepMap.total {m : Nat} (n : Set)251  shows TotalBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)252proof253  intros u hu254  obtain ⟨bounded, x, hxSucc, y, hyN, source⟩ := product.membership.forward with hu255  have successorShape := membership.successor_set{n := m}.forward with hxSucc256  cases successorShape with old | newest257  . witness inl((x, y))258    constructor259    . have pairMember := product.pair with old, hyN260      exact disjointSum.left with pairMember261    . rw source262      exact productStepMap.relates_old{m := m} at n, x, y263  . witness inr(y)264    constructor265    . have tagged := disjointSum.right at y, m × n, n266      exact tagged with hyN267    . rw [source, newest]268      exact productStepMap.relates_new{m := m} at n, y269270theorem productStepMap.functional {m : Nat} (n : Set)271  shows Functional(productStepMap(m, n))272proof273  intros u v huv q huq274  have first := productStepMap.factors with huv275  have second := productStepMap.factors with huq276  cases first with firstOld | firstNew277  . cases second with secondOld | secondNew278    . obtain (x1, hx1) := firstOld279      rcases hx1 with ⟨hx1M, y1, hy1N, source1, target1⟩280      obtain ⟨x2, hx2M, y2, hy2N, source2, target2⟩ := secondOld281      rw source1 at source2282      obtain (sameX, sameY) := orderedPair.injective with source2283      rw [target1, target2, sameX, sameY]284      rfl285    . obtain (xOld, hxOld) := firstOld286      rcases hxOld with ⟨hxOldM, yOld, hyOldN, sourceOld, targetOld⟩287      obtain ⟨yNew, hyNewN, sourceNew, targetNew⟩ := secondNew288      rw sourceOld at sourceNew289      have sameFirst := orderedPair.first with sourceNew290      rw sameFirst at hxOldM291      have irreflexive := membership.irreflexive with hxOldM292      contradiction293  . cases second with secondOldAfterNew | secondNewAfterNew294    . obtain (yNewFirst, hyNewFirst) := firstNew295      rcases hyNewFirst with ⟨hyNewFirstN, sourceNewFirst, targetNewFirst⟩296      obtain ⟨xOldSecond, hxOldSecondM, yOldSecond, hyOldSecondN, sourceOldSecond, targetOldSecond⟩ := secondOldAfterNew297      rw sourceOldSecond at sourceNewFirst298      have sameFirstReverse := orderedPair.first with sourceNewFirst299      rw sameFirstReverse at hxOldSecondM300      have irreflexiveReverse := membership.irreflexive with hxOldSecondM301      contradiction302    . obtain (yNew1, hyNew1) := firstNew303      rcases hyNew1 with ⟨hyNew1N, sourceNew1, targetNew1⟩304      obtain ⟨yNew2, hyNew2N, sourceNew2, targetNew2⟩ := secondNewAfterNew305      rw sourceNew1 at sourceNew2306      obtain (sameM, sameYNew) := orderedPair.injective with sourceNew2307      rw [targetNew1, targetNew2, sameYNew]308      rfl309310theorem productStepMap.function {m : Nat} (n : Set)311  shows productStepMap(m, n) : succ(m) × n → (m × n) ⊎ n312proof313  constructor314  . exact productStepMap.relation at m, n315  . constructor316    . exact productStepMap.functional{m := m} at n317    . exact productStepMap.total{m := m} at n318319theorem productStepMap.injective {m : Nat} (n : Set)320  shows InjectiveBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)321proof322  constructor323  . exact productStepMap.function{m := m} at n324  . intros u hu v hv q hq huq hvq325    have first := productStepMap.factors with huq326    have second := productStepMap.factors with hvq327    cases first with firstOld | firstNew328    . cases second with secondOld | secondNew329      . obtain (x1, hx1) := firstOld330        rcases hx1 with ⟨hx1M, y1, hy1N, source1, target1⟩331        obtain ⟨x2, hx2M, y2, hy2N, source2, target2⟩ := secondOld332        rw target1 at target2333        have samePair := inl.injective with target2334        rw source1335        rwa source2336      . obtain (xOld, hxOld) := firstOld337        rcases hxOld with ⟨hxOldM, yOld, hyOldN, sourceOld, targetOld⟩338        obtain ⟨yNew, hyNewN, sourceNew, targetNew⟩ := secondNew339        rw targetOld at targetNew340        have impossible := tags.disjoint with targetNew341        contradiction342    . cases second with secondOldAfterNew | secondNewAfterNew343      . obtain (yNewFirst, hyNewFirst) := firstNew344        rcases hyNewFirst with ⟨hyNewFirstN, sourceNewFirst, targetNewFirst⟩345        obtain ⟨xOldSecond, hxOldSecondM, yOldSecond, hyOldSecondN, sourceOldSecond, targetOldSecond⟩ := secondOldAfterNew346        rw targetOldSecond at targetNewFirst347        have impossibleReverse := tags.disjoint with targetNewFirst348        contradiction349      . obtain (yNew1, hyNew1) := firstNew350        rcases hyNew1 with ⟨hyNew1N, sourceNew1, targetNew1⟩351        obtain ⟨yNew2, hyNew2N, sourceNew2, targetNew2⟩ := secondNewAfterNew352        rw targetNew1 at targetNew2353        have sameY := inr.injective with targetNew2354        rw [sourceNew1, sourceNew2, sameY]355        rfl356357theorem productStepMap.surjective {m : Nat} (n : Set)358  shows SurjectiveBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)359proof360  constructor361  . exact productStepMap.function{m := m} at n362  . intros q hq363    have targetShape := disjointSum.membership.forward with hq364    cases targetShape with old | newest365    . obtain (pairXY, hpairXY) := old366      rcases hpairXY with (pairMember, qShape)367      obtain ⟨pairBound, x, hxM, y, hyN, pairShape⟩ := product.membership.forward with pairMember368      witness (x, y)369      constructor370      . apply product.pair at x, y, succ(m), n371        . apply membership.successor_set{n := m}.backward at x372          left373          exact hxM374        . exact hyN375      . rw [qShape, pairShape]376        exact productStepMap.relates_old{m := m} at n, x, y377    . obtain (yNew, hyNew) := newest378      rcases hyNew with (hyNewN, qShapeNew)379      witness (m, yNew)380      constructor381      . apply product.pair at m, yNew, succ(m), n382        . apply membership.successor_set{n := m}.backward at m383          right384          rfl385        . exact hyNewN386      . rw qShapeNew387        exact productStepMap.relates_new{m := m} at n, yNew388389theorem productStepMap.bijective {m : Nat} (n : Set)390  shows BijectiveBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)391proof392  --! Split a successor rectangle into its old part and newest row.393  --| The tags make the two images disjoint without imposing an order on n.394  constructor395  . --! Each tagged output has one source pair396    exact productStepMap.injective{m := m} at n397  . --! Every old pair ∨ newest-row element is reached398    exact productStepMap.surjective{m := m} at n399400-- Recursively assemble the concrete graph witnessing m × n ≃ m*n. At a401-- successor, productStepMap exposes the old rectangle plus one row, sumMap402-- transports the induction hypothesis, and natSumEquiv packs the two blocks403-- into the next native numeral.404def natProductEquiv (m n : Nat) → Set405  | zero, n => identity(0)406  | succ(m), n => compose(natSumEquiv(m * n, n), compose(sumMap(natProductEquiv(m, n), identity(n), m × n, n, m * n, n), productStepMap(m, n), succ(m) × n, (m × n) ⊎ n, (m * n) ⊎ n), succ(m) × n, (m * n) ⊎ n, m * n + n)407408theorem BijectiveBetween.codomain_eq (f X Y Z : Set)409  requires h : BijectiveBetween(f, X, Y)410  requires hYZ : Y = Z411  shows BijectiveBetween(f, X, Z)412proof413  simp414415theorem natProductEquiv.bijective (n m : Nat)416  shows BijectiveBetween(natProductEquiv(m, n), m × n, mul(m, n))417proof418  induction m419  | zero =>420    rw [natProductEquiv, mul, product.zero_left]421    exact identity.bijective422  | succ(k) using ih =>423    --! Decompose the successor rectangle.424    --| The old rectangle and newest row are separated by productStepMap.425    rw [natProductEquiv, mul]426    --! Transport the old block and the new row.427    have step := productStepMap.bijective{m := k} at n428    have identityN := identity.bijective at n429    have lifted := sumMap.bijective with ih, identityN430    have middle := compose.bijective with step, lifted431    --! Pack the two finite blocks into multiplication.432    apply BijectiveBetween.codomain_eq at compose(natSumEquiv(k * n, n), compose(sumMap(natProductEquiv(k, n), identity(n), k × n, n, k * n, n), productStepMap(k, n), succ(k) × n, (k × n) ⊎ n, (k * n) ⊎ n), succ(k) × n, (k * n) ⊎ n, k * n + n), succ(k) × n, k * n + n, n + k * n433    . apply compose.bijective at natSumEquiv(k * n, n), compose(sumMap(natProductEquiv(k, n), identity(n), k × n, n, k * n, n), productStepMap(k, n), succ(k) × n, (k × n) ⊎ n, (k * n) ⊎ n), succ(k) × n, (k * n) ⊎ n, k * n + n434      . exact middle435      . apply natSumEquiv.bijective at n, mul(k, n)436    . apply Grace.Core.Nat.Algebra.add.commutative at n, mul(k, n)437438theorem Equipotent.nat_product (m n : Set)439  requires hm : Nat(m)440  requires hn : Nat(n)441  shows (m × n) ≃ mul(m, n)442proof443  witness natProductEquiv(m, n)444  exact natProductEquiv.bijective with hn, hm445446theorem HasCardinality.product (A B m n : Set)447  requires hA : HasCardinality(A, m)448  requires hB : HasCardinality(B, n)449  shows HasCardinality(A × B, mul(m, n))450proof451  rcases hA with (hm, equipotentA)452  rcases hB with (hn, equipotentB)453  constructor454  . exact Grace.Core.Nat.Algebra.mul.closed at n, m455  . --! Lift the two cardinal witnesses coordinatewise.456    have lifted := Equipotent.product with equipotentA, equipotentB457    --! Identify the finite rectangle with native multiplication.458    have numeric := Equipotent.nat_product with hm, hn459    exact Equipotent.transitive with lifted, numeric460461theorem Finite.product (A B : Set)462  requires finiteA : Finite(A)463  requires finiteB : Finite(B)464  shows Finite(A × B)465proof466  obtain (m, hA) := finiteA467  obtain (n, hB) := finiteB468  witness mul(m, n)469  exact HasCardinality.product with hA, hB470471-- The canonical exchange of two Cartesian factors.472defunique swappedPair (A B p : Set) (q ∈ B × A) :=473  ∃ x ∈ A, ∃ y ∈ B, p = (x, y) ∧ q = (y, x)474requires pair : p ∈ A × B475proof476  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair477  have output := product.pair with hy, hx478  refine ⟨(y, x), output, x, hx, y, hy, shape, rfl⟩479uniqueness480  intros u hu first v hv second481  obtain ⟨a, ha, b, hb, shapeU, valueU⟩ := first482  obtain ⟨c, hc, d, hd, shapeV, valueV⟩ := second483  have equal : (a, b) = (c, d) by cc484  have coordinates := orderedPair.injective with equal485  cc486487defgraph productSwap (A B : Set) (p ∈ A × B) : B × A := swappedPair(A, B, p)488proof489  have selected := swappedPair.selected with member490  exact selected.left491492theorem productSwap.pair (A B x y : Set)493  requires hx : x ∈ A494  requires hy : y ∈ B495  shows productSwap(A, B)((x, y)) = (y, x)496proof497  have pair := product.pair at x, y, A, B with *498  have selected := swappedPair.selected with pair499  obtain ⟨a, ha, b, hb, shape, output⟩ := selected.right500  have coordinates := orderedPair.injective with shape501  have value := productSwap.value with pair502  cc503504theorem productSwap.involution (A B p : Set)505  requires pair : p ∈ A × B506  shows productSwap(B, A)(productSwap(A, B)(p)) = p507proof508  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair509  have first := productSwap.pair with hx, hy510  have second := productSwap.pair with hy, hx511  cc512513theorem productSwap.bijective (A B : Set)514  shows BijectiveBetween(productSwap(A, B), A × B, B × A)515proof516  have function := productSwap.function at A, B517  have reverse := productSwap.function at B, A518  constructor519  . unfold InjectiveBetween520    refine ⟨function, _⟩521    intros x hx y hy z hz edgeX edgeY522    have valueX := FunctionBetween.apply_value at productSwap(A, B), A × B, B × A, x, z with *523    have valueY := FunctionBetween.apply_value at productSwap(A, B), A × B, B × A, y, z with *524    have inverseX := productSwap.involution with hx525    have inverseY := productSwap.involution with hy526    cc527  . unfold SurjectiveBetween528    refine ⟨function, _⟩529    intros z hz530    have input := FunctionBetween.apply_closed at productSwap(B, A), B × A, A × B, z with *531    have inverse := productSwap.involution with hz532    have edge := FunctionBetween.relates_apply at productSwap(A, B), A × B, B × A, productSwap(B, A)(z) with *533    refine ⟨productSwap(B, A)(z), input, _⟩534    rwa inverse at edge535