Grace/Cumulus/FixedPoint/KuhnNeighbour.g17

Open in Workbench Download source

Imports

KuhnSimplex · Set.Transposition

Declarations

Source

1-- The neighbour of a Kuhn simplex across an interior face: swapping two2-- consecutive steps of the order keeps every vertex but one3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.FixedPoint.KuhnNeighbour9import KuhnSimplex10import Set.Transposition1112-- The order with steps a and a + 1 exchanged.13def swapped (n upd a : Set) : Set := compose(upd, transposition(n, a, succ(a)), n, n, n)1415theorem swapped.bijective (n upd a : Set)16  requires bijective : BijectiveBetween(upd, n, n)17  requires ha : a ∈ n18  requires hb : succ(a) ∈ n19  shows BijectiveBetween(swapped(n, upd, a), n, n)20proof21  have swap := transposition.bijective with ha, hb22  unfold swapped23  exact compose.bijective with swap, bijective2425-- Initial segments below a, or containing both a and a + 1, are fixed by26-- the transposition.27theorem transposition.image_below (n : Nat) (a k : Set)28  requires ha : a ∈ n29  requires hb : succ(a) ∈ n30  requires hk : k ⊆ a31  shows functionImage(transposition(n, a, succ(a)), k, n) = k32proof33  have naturals := natural.member at n34  have aNat := naturals with ha35  have aInside := Ordinal.member_subset with (Ordinal.natural at n), ha36  have function := Injective.function with (Bijective.injective with (transposition.bijective at n, a, succ(a) with ha, hb))37  ext y38  constructor39  . intro hy40    simp [functionImage.membership] at hy41    obtain ⟨inN, x, hx, shape⟩ := hy42    have hxa := hk with x, hx43    have xNat := naturals with (aInside with x, hxa)44    have below := Less.of_membership with hxa45    have notFirst : x ≠ a by arith46    have notSecond : x ≠ succ(a) by arith47    have fixed := transposition.other with ha, hb, (aInside with x, hxa), notFirst, notSecond48    rwa [shape, fixed]49  . intro hy50    have hya := hk with y, hy51    have yNat := naturals with (aInside with y, hya)52    have below := Less.of_membership with hya53    have notFirst : y ≠ a by arith54    have notSecond : y ≠ succ(a) by arith55    have inN := aInside with y, hya56    have fixed := transposition.other with ha, hb, inN, notFirst, notSecond57    simp [functionImage.membership]5859theorem transposition.image_above (n : Nat) (a k : Set)60  requires ha : a ∈ n61  requires hb : succ(a) ∈ n62  requires hk : k ⊆ n63  requires aIn : a ∈ k64  requires bIn : succ(a) ∈ k65  shows functionImage(transposition(n, a, succ(a)), k, n) = k66proof67  have bijective := transposition.bijective with ha, hb68  have function := Injective.function with (Bijective.injective with bijective)69  have first := transposition.first with ha, hb70  have second := transposition.second with ha, hb71  have closed : ∀ x ∈ k, transposition(n, a, succ(a))(x) ∈ k72    intros x hx73    have split : x = a ∨ x ≠ a by tauto74    cases split with isA | notA75    . rw [isA, first]76      exact bIn77    . have split2 : x = succ(a) ∨ x ≠ succ(a) by tauto78      cases split2 with isB | notB79      . rw [isB, second]80        exact aIn81      . have fixed := transposition.other with ha, hb, (hk with x, hx), notA, notB82        rwa fixed83  ext y84  constructor85  . intro hy86    simp [functionImage.membership] at hy87    obtain ⟨inN, x, hx, shape⟩ := hy88    rw shape89    exact closed with x, hx90  . intro hy91    have preimage := closed with y, hy92    have involution := transposition.involution with ha, hb93    have back : transposition(n, a, succ(a))(transposition(n, a, succ(a))(y)) = y94      exact involution.right with y, (hk with y, hy)95    simp [functionImage.membership]96    constructor97    . exact hk with y, hy98    . witness transposition(n, a, succ(a))(y)99      constructor100      . exact preimage101      . symm102        exact back103104-- Raised sets under the swapped order agree except at step a + 1.105theorem raised.swapped (n : Nat) (upd a k : Set)106  requires updBijective : BijectiveBetween(upd, n, n)107  requires ha : a ∈ n108  requires hb : succ(a) ∈ n109  requires hk : k ⊆ n110  shows raised(n, swapped(n, upd, a), k) = functionImage(upd, functionImage(transposition(n, a, succ(a)), k, n), n)111proof112  have updFunction := Injective.function with (Bijective.injective with updBijective)113  have swap := transposition.bijective with ha, hb114  have swapFunction := Injective.function with (Bijective.injective with swap)115  have same : raised(n, swapped(n, upd, a), k) = functionImage(compose(upd, transposition(n, a, succ(a)), n, n, n), k, n)116    unfold raised117    unfold swapped118    rfl119  rw same120  exact functionImage.compose with swapFunction, updFunction, hk121122theorem raised.swapped_below (n : Nat) (upd a k : Set)123  requires updBijective : BijectiveBetween(upd, n, n)124  requires ha : a ∈ n125  requires hb : succ(a) ∈ n126  requires hk : k ⊆ a127  shows raised(n, swapped(n, upd, a), k) = raised(n, upd, k)128proof129  have aInside := Ordinal.member_subset with (Ordinal.natural at n), ha130  have inside := Subset.transitive with hk, aInside131  have step := raised.swapped with updBijective, ha, hb, inside132  have image := transposition.image_below with ha, hb, hk133  rw [step, image]134  have same : raised(n, upd, k) = functionImage(upd, k, n)135    unfold raised136    rfl137  rw same138  rfl139140theorem raised.swapped_above (n : Nat) (upd a k : Set)141  requires updBijective : BijectiveBetween(upd, n, n)142  requires ha : a ∈ n143  requires hb : succ(a) ∈ n144  requires hk : k ⊆ n145  requires aIn : a ∈ k146  requires bIn : succ(a) ∈ k147  shows raised(n, swapped(n, upd, a), k) = raised(n, upd, k)148proof149  have step := raised.swapped with updBijective, ha, hb, hk150  have image := transposition.image_above with ha, hb, hk, aIn, bIn151  rw [step, image]152  have same : raised(n, upd, k) = functionImage(upd, k, n)153    unfold raised154    rfl155  rw same156  rfl157158-- Vertices other than the (a + 1)-st agree; that one differs.159theorem kuhnVertex.swapped_same (n : Nat) (base upd a k : Set)160  requires baseFunction : base : n → ℕ161  requires updBijective : BijectiveBetween(upd, n, n)162  requires ha : a ∈ n163  requires hb : succ(a) ∈ n164  requires hk : k ∈ succ(n)165  requires different : k ≠ succ(a)166  shows kuhnVertex(n, base, swapped(n, upd, a))(k) = kuhnVertex(n, base, upd)(k)167proof168  have naturals := natural.member at n169  have aNat := naturals with ha170  have kNat := natural.member at succ(n) with hk171  have kInside := kuhnVertex.index_subset with hk172  have sameRaised : raised(n, swapped(n, upd, a), k) = raised(n, upd, k)173    have order := Ordinal.trichotomy with (Ordinal.natural at k), succ(a), (Ordinal.natural at succ(a))174    cases order with below | rest175    . have kBelow := kuhnVertex.index_subset with below176      exact raised.swapped_below with updBijective, ha, hb, kBelow177    . cases rest with same | above178      . exfalso179        exact different with same180      . have aIn : a ∈ k181          have self := bootstrap.succ.self at a182          have inside := Ordinal.member_subset with (Ordinal.natural at k), above183          exact inside with a, self184        exact raised.swapped_above with updBijective, ha, hb, kInside, aIn, above185  have f1 := kuhnVertex.function_on at n, base, swapped(n, upd, a), k with baseFunction, hk186  have f2 := kuhnVertex.function_on at n, base, upd, k with baseFunction, hk187  apply FunctionBetween.ext with f1, f2188  intros j hj189  have c1 := kuhnVertex.coordinate at n, base, swapped(n, upd, a), k, j with baseFunction, hk, hj190  have c2 := kuhnVertex.coordinate at n, base, upd, k, j with baseFunction, hk, hj191  rw [c1, c2, sameRaised]192  rfl193194theorem transposition.image_step (n : Nat) (a : Set)195  requires ha : a ∈ n196  requires hb : succ(a) ∈ n197  shows functionImage(transposition(n, a, succ(a)), succ(a), n) = insert(succ(a), a)198proof199  have naturals := natural.member at n200  have aNat := naturals with ha201  have aInside := Ordinal.member_subset with (Ordinal.natural at n), ha202  have bijective := transposition.bijective with ha, hb203  have function := Injective.function with (Bijective.injective with bijective)204  have first := transposition.first with ha, hb205  have self := bootstrap.succ.self at a206  ext y207  constructor208  . intro hy209    simp [functionImage.membership] at hy210    obtain ⟨inN, x, hx, shape⟩ := hy211    have split := bootstrap.succ.membership.forward with hx212    apply insert.membership.backward213    cases split with below | same214    . right215      have xNat := naturals with (aInside with x, below)216      have less := Less.of_membership with below217      have notFirst : x ≠ a by arith218      have notSecond : x ≠ succ(a) by arith219      have fixed := transposition.other with ha, hb, (aInside with x, below), notFirst, notSecond220      rwa [shape, fixed]221    . left222      rw [shape, same, first]223      rfl224  . intro hy225    have split := insert.membership.forward with hy226    cases split with same | below227    . rw same228      simp [functionImage.membership]229      constructor230      . exact hb231      . witness a232        constructor233        . exact self234        . symm235          exact first236    . have xNat := naturals with (aInside with y, below)237      have less := Less.of_membership with below238      have notFirst : y ≠ a by arith239      have notSecond : y ≠ succ(a) by arith240      have inN := aInside with y, below241      have fixed := transposition.other with ha, hb, inN, notFirst, notSecond242      have inSucc := membership.into_successor with below243      simp [functionImage.membership]244245theorem kuhnVertex.swapped_differs (n : Nat) (base upd a : Set)246  requires baseFunction : base : n → ℕ247  requires updBijective : BijectiveBetween(upd, n, n)248  requires ha : a ∈ n249  requires hb : succ(a) ∈ n250  shows kuhnVertex(n, base, swapped(n, upd, a))(succ(a)) ≠ kuhnVertex(n, base, upd)(succ(a))251proof252  have updInjective := Bijective.injective with updBijective253  have updFunction := Injective.function with updInjective254  have bIn := membership.into_successor with hb255  have coordinate := FunctionBetween.apply_closed with updFunction, hb256  have c1 := kuhnVertex.coordinate at n, base, swapped(n, upd, a), succ(a), upd(succ(a)) with baseFunction, bIn, coordinate257  have c2 := kuhnVertex.coordinate at n, base, upd, succ(a), upd(succ(a)) with baseFunction, bIn, coordinate258  have bInside := Ordinal.member_subset with (Ordinal.natural at n), hb259  have step := raised.swapped with updBijective, ha, hb, bInside260  have image := transposition.image_step with ha, hb261  rw image at step262  have inRaised : upd(succ(a)) ∈ raised(n, swapped(n, upd, a), succ(a))263    rw step264    have inInsert : succ(a) ∈ insert(succ(a), a)265      apply insert.membership.backward266      left267      rfl268    simp [functionImage.membership]269  have fresh := raised.fresh with updInjective, hb270  have one := indicator.member with inRaised271  have zero := indicator.absent with fresh272  intro equal273  have values : kuhnVertex(n, base, swapped(n, upd, a))(succ(a))(upd(succ(a))) = kuhnVertex(n, base, upd)(succ(a))(upd(succ(a)))274    rw equal275    rfl276  rw [c1, c2, one, zero] at values277  have baseValue := FunctionBetween.apply_closed with baseFunction, coordinate278  have baseNat := nat.omega.backward with baseValue279  arith280281-- Helpers: indicators separate sets; equal vertices force equal raised282-- sets and equal bases; equal vertex maps give equal simplices.283theorem indicator.separates (A B j : Set)284  requires same : indicator(A, j) = indicator(B, j)285  shows j ∈ A ↔ j ∈ B286proof287  constructor288  . intro inA289    have one := indicator.member with inA290    by_contra outB291    have zero := indicator.absent with outB292    rw [one, zero] at same293    apply zero.ne_one294    symm295    exact same296  . intro inB297    have one := indicator.member with inB298    by_contra outA299    have zero := indicator.absent with outA300    rw [one, zero] at same301    exact zero.ne_one with same302303theorem raised.of_vertex (n : Nat) (base u v k : Set)304  requires baseFunction : base : n → ℕ305  requires hk : k ∈ succ(n)306  requires same : kuhnVertex(n, base, u)(k) = kuhnVertex(n, base, v)(k)307  shows raised(n, u, k) = raised(n, v, k)308proof309  have insideU := raised.subset at n, u, k310  have insideV := raised.subset at n, v, k311  ext j312  constructor313  . intro hj314    have hjn := insideU with j, hj315    have c1 := kuhnVertex.coordinate at n, base, u, k, j with baseFunction, hk, hjn316    have c2 := kuhnVertex.coordinate at n, base, v, k, j with baseFunction, hk, hjn317    have values : kuhnVertex(n, base, u)(k)(j) = kuhnVertex(n, base, v)(k)(j)318      rw same319      rfl320    rw [c1, c2] at values321    have baseValue := FunctionBetween.apply_closed with baseFunction, hjn322    have baseNat := nat.omega.backward with baseValue323    have tagU := indicator.natural at raised(n, u, k), j324    have tagV := indicator.natural at raised(n, v, k), j325    have tags : indicator(raised(n, u, k), j) = indicator(raised(n, v, k), j) by exact add.left_cancel with values326    have equivalent := indicator.separates with tags327    exact equivalent.forward with hj328  . intro hj329    have hjn := insideV with j, hj330    have c1 := kuhnVertex.coordinate at n, base, u, k, j with baseFunction, hk, hjn331    have c2 := kuhnVertex.coordinate at n, base, v, k, j with baseFunction, hk, hjn332    have values : kuhnVertex(n, base, u)(k)(j) = kuhnVertex(n, base, v)(k)(j)333      rw same334      rfl335    rw [c1, c2] at values336    have baseValue := FunctionBetween.apply_closed with baseFunction, hjn337    have baseNat := nat.omega.backward with baseValue338    have tags : indicator(raised(n, u, k), j) = indicator(raised(n, v, k), j) by exact add.left_cancel with values339    have equivalent := indicator.separates with tags340    exact equivalent.backward with hj341342theorem kuhnSimplex.base_of_bottom (n : Nat) (b1 u1 b2 u2 : Set)343  requires f1 : b1 : n → ℕ344  requires f2 : b2 : n → ℕ345  requires same : kuhnVertex(n, b1, u1)(0) = kuhnVertex(n, b2, u2)(0)346  shows b1 = b2347proof348  apply FunctionBetween.ext with f1, f2349  intros j hj350  have z1 := kuhnVertex.zero_coordinate at n, b1, u1, j with f1, hj351  have z2 := kuhnVertex.zero_coordinate at n, b2, u2, j with f2, hj352  have values : kuhnVertex(n, b1, u1)(0)(j) = kuhnVertex(n, b2, u2)(0)(j)353    rw same354    rfl355  rwa [z1, z2] at values356357theorem kuhnSimplex.ext_of_vertices (n : Nat) (b1 u1 b2 u2 : Set)358  requires f1 : b1 : n → ℕ359  requires f2 : b2 : n → ℕ360  requires same : ∀ k ∈ succ(n), kuhnVertex(n, b1, u1)(k) = kuhnVertex(n, b2, u2)(k)361  shows kuhnSimplex(n, b1, u1) = kuhnSimplex(n, b2, u2)362proof363  ext x364  constructor365  . intro hx366    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hx367    have equal := same with hk368    rw [shape, equal]369    exact kuhnVertex.member with f2, hk370  . intro hx371    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hx372    have equal := same with hk373    rw [shape, ← equal]374    exact kuhnVertex.member with f1, hk375376-- The swapped simplex shares the face opposite the (a + 1)-st vertex.377theorem kuhnSimplex.swapped_face (n : Nat) (base upd a : Set)378  requires baseFunction : base : n → ℕ379  requires updBijective : BijectiveBetween(upd, n, n)380  requires ha : a ∈ n381  requires hb : succ(a) ∈ n382  shows kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(succ(a))} =383    kuhnSimplex(n, base, swapped(n, upd, a)) ∖ {kuhnVertex(n, base, swapped(n, upd, a))(succ(a))}384proof385  have updInjective := Bijective.injective with updBijective386  have swapInjective := Bijective.injective with (swapped.bijective with updBijective, ha, hb)387  have bIn := membership.into_successor with hb388  ext x389  constructor390  . intro hx391    have parts := difference.singleton_membership.forward with hx392    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left393    have different : k ≠ succ(a)394      intro same395      apply parts.right396      rw [shape, same]397      rfl398    have agree := kuhnVertex.swapped_same with baseFunction, updBijective, ha, hb, hk, different399    apply difference.singleton_membership.backward400    constructor401    . rw [shape, ← agree]402      exact kuhnVertex.member with baseFunction, hk403    . intro equal404      rw [shape, ← agree] at equal405      have same := kuhnVertex.injective with baseFunction, swapInjective, hk, bIn, equal406      exact different with same407  . intro hx408    have parts := difference.singleton_membership.forward with hx409    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left410    have different : k ≠ succ(a)411      intro same412      apply parts.right413      rw [shape, same]414      rfl415    have agree := kuhnVertex.swapped_same with baseFunction, updBijective, ha, hb, hk, different416    apply difference.singleton_membership.backward417    constructor418    . rw [shape, agree]419      exact kuhnVertex.member with baseFunction, hk420    . intro equal421      rw [shape, agree] at equal422      have same := kuhnVertex.injective with baseFunction, updInjective, hk, bIn, equal423      exact different with same424425theorem kuhnVertex.of_raised (n : Nat) (base u v k : Set)426  requires baseFunction : base : n → ℕ427  requires hk : k ∈ succ(n)428  requires same : raised(n, u, k) = raised(n, v, k)429  shows kuhnVertex(n, base, u)(k) = kuhnVertex(n, base, v)(k)430proof431  have f1 := kuhnVertex.function_on at n, base, u, k with baseFunction, hk432  have f2 := kuhnVertex.function_on at n, base, v, k with baseFunction, hk433  apply FunctionBetween.ext with f1, f2434  intros j hj435  have c1 := kuhnVertex.coordinate at n, base, u, k, j with baseFunction, hk, hj436  have c2 := kuhnVertex.coordinate at n, base, v, k, j with baseFunction, hk, hj437  rw [c1, c2, same]438  rfl439440theorem raised.swapped_step (n : Nat) (upd a : Set)441  requires updBijective : BijectiveBetween(upd, n, n)442  requires ha : a ∈ n443  requires hb : succ(a) ∈ n444  shows raised(n, swapped(n, upd, a), succ(a)) = insert(upd(succ(a)), raised(n, upd, a))445proof446  have updFunction := Injective.function with (Bijective.injective with updBijective)447  have bInside := Ordinal.member_subset with (Ordinal.natural at n), hb448  have step := raised.swapped with updBijective, ha, hb, bInside449  have image := transposition.image_step with ha, hb450  have inserted := functionImage.insert at upd, n, n, succ(a), a with updFunction, hb451  have same : raised(n, upd, a) = functionImage(upd, a, n)452    unfold raised453    rfl454  rw [step, image, inserted, same]455  rfl456457-- Across an interior face, the only simplices are the simplex itself and458-- its swapped neighbour.459theorem kuhnSimplex.interior_neighbours (n : Nat) (b u a b2 u2 c : Set)460  requires f1 : b : n → ℕ461  requires bij1 : BijectiveBetween(u, n, n)462  requires f2 : b2 : n → ℕ463  requires bij2 : BijectiveBetween(u2, n, n)464  requires ha : a ∈ n465  requires hb : succ(a) ∈ n466  requires hc : c ∈ kuhnSimplex(n, b2, u2)467  requires same : kuhnSimplex(n, b2, u2) ∖ {c} = kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(succ(a))}468  shows kuhnSimplex(n, b2, u2) = kuhnSimplex(n, b, u) ∨469    kuhnSimplex(n, b2, u2) = kuhnSimplex(n, b, swapped(n, u, a))470proof471  have inj1 := Bijective.injective with bij1472  have inj2 := Bijective.injective with bij2473  have fun1 := Injective.function with inj1474  have fun2 := Injective.function with inj2475  have zeroNat : Nat(0) by typecheck476  have naturals := natural.member at n477  have aNat := naturals with ha478  have iIn := membership.into_successor with hb479  have positive : 0 < succ(n) by arith480  have zeroIn := membership.of_Less with positive481  have nIn := bootstrap.succ.self at n482  have aIn := membership.into_successor with ha483  have bBelow := Less.of_membership with hb484  have ssBelow : succ(succ(a)) < succ(n) by arith485  have ssIn := membership.of_Less with ssBelow486  have inT : ∀ k ∈ succ(n), k ≠ succ(a) → kuhnVertex(n, b, u)(k) ∈ kuhnSimplex(n, b2, u2)487    intros k hk different488    have member := kuhnVertex.member at n, b, u, k with f1, hk489    have notMissing : kuhnVertex(n, b, u)(k) ≠ kuhnVertex(n, b, u)(succ(a))490      intro equal491      have sameIndex := kuhnVertex.injective with f1, inj1, hk, iIn, equal492      exact different with sameIndex493    have inFace : kuhnVertex(n, b, u)(k) ∈ kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(succ(a))}494      exact difference.singleton_membership.backward with ⟨member, notMissing⟩495    rw ← same at inFace496    have parts := difference.singleton_membership.forward with inFace497    exact parts.left498  have zeroDifferent : 0 ≠ succ(a) by arith499  have nDifferent : n ≠ succ(a)500    intro equal501    rw equal at hb502    have irreflexive := Ordinal.not_member_self at succ(a)503    exact irreflexive with hb504  have v0 := inT with 0, zeroIn, zeroDifferent505  have vn := inT with n, nIn, nDifferent506  have bounds0 := kuhnSimplex.sum_bounds with f2, inj2, v0507  have boundsN := kuhnSimplex.sum_bounds with f2, inj2, vn508  have sum0 := kuhnVertex.sum with f1, inj1, zeroIn509  have sumN := kuhnVertex.sum with f1, inj1, nIn510  have weights1 : ∀ j ∈ n, b(j) ∈ ℕ511    intros j hj512    exact FunctionBetween.apply_closed with f1, hj513  have weights2 : ∀ j ∈ n, b2(j) ∈ ℕ514    intros j hj515    exact FunctionBetween.apply_closed with f2, hj516  have total1 := natSum.natural with (Finite.natural at n), weights1517  have total2 := natSum.natural with (Finite.natural at n), weights2518  have lower := bounds0.left519  have upper := boundsN.right520  rw sum0 at lower521  rw sumN at upper522  rw add.right_unit at lower523  have upper2 := LessEqual.add_right_cancel with upper524  have equalSums := LessEqual.antisymmetric with lower, upper2525  have agree : ∀ k ∈ succ(n), k ≠ succ(a) → kuhnVertex(n, b, u)(k) = kuhnVertex(n, b2, u2)(k)526    intros k hk different527    have inside := inT with k, hk, different528    have total := kuhnVertex.sum with f1, inj1, hk529    rw ← equalSums at total530    exact kuhnSimplex.vertex_of_sum with f2, inj2, inside, hk, total531  have bases := kuhnSimplex.base_of_bottom with f1, f2, (agree with 0, zeroIn, zeroDifferent)532  have aDifferent : a ≠ succ(a) by arith533  have ssDifferent : succ(succ(a)) ≠ succ(a) by arith534  have agreeA := agree with a, aIn, aDifferent535  have agreeSS := agree with succ(succ(a)), ssIn, ssDifferent536  rw ← bases at agreeA537  rw ← bases at agreeSS538  have raisedA := raised.of_vertex with f1, aIn, agreeA539  have raisedSS := raised.of_vertex with f1, ssIn, agreeSS540  have stepU2 := raised.succ with fun2, ha541  have stepU2b := raised.succ with fun2, hb542  have stepU := raised.succ with fun1, ha543  have stepUb := raised.succ with fun1, hb544  have u2aIn : u2(a) ∈ raised(n, u, succ(succ(a)))545    rw [raisedSS, stepU2b, stepU2]546    apply insert.membership.backward547    right548    apply insert.membership.backward549    left550    rfl551  rw [stepUb, stepU] at u2aIn552  have fresh2 := raised.fresh with inj2, ha553  rw ← raisedA at fresh2554  have split := insert.membership.forward with u2aIn555  cases split with isB | rest556  . right557    have raisedStep : raised(n, u2, succ(a)) = raised(n, swapped(n, u, a), succ(a))558      rw [stepU2, ← raisedA, isB]559      have swappedStep := raised.swapped_step with bij1, ha, hb560      rw swappedStep561      rfl562    rw ← bases563    apply kuhnSimplex.ext_of_vertices with f1, f1564    intros k hk565    have split2 : k = succ(a) ∨ k ≠ succ(a) by tauto566    cases split2 with isStep | other567    . rw isStep568      exact kuhnVertex.of_raised with f1, iIn, raisedStep569    . have fromS := agree with k, hk, other570      rw ← bases at fromS571      have toSwapped := kuhnVertex.swapped_same with f1, bij1, ha, hb, hk, other572      rw [← fromS, toSwapped]573      rfl574  . have split3 := insert.membership.forward with rest575    cases split3 with isA | inA576    . left577      have raisedStep : raised(n, u2, succ(a)) = raised(n, u, succ(a))578        rw [stepU2, ← raisedA, isA, stepU]579        rfl580      rw ← bases581      apply kuhnSimplex.ext_of_vertices with f1, f1582      intros k hk583      have split2 : k = succ(a) ∨ k ≠ succ(a) by tauto584      cases split2 with isStep | other585      . rw isStep586        exact kuhnVertex.of_raised with f1, iIn, raisedStep587      . have fromS := agree with k, hk, other588        rw ← bases at fromS589        symm590        exact fromS591    . exfalso592      exact fresh2 with inA593