-- The neighbour of a Kuhn simplex across an interior face: swapping two
-- consecutive steps of the order keeps every vertex but one
-- 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.FixedPoint.KuhnNeighbour
import KuhnSimplex
import Set.Transposition

-- The order with steps a and a + 1 exchanged.
def swapped (n upd a : Set) : Set := compose(upd, transposition(n, a, succ(a)), n, n, n)

theorem swapped.bijective (n upd a : Set)
  requires bijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows BijectiveBetween(swapped(n, upd, a), n, n)
proof
  have swap := transposition.bijective with ha, hb
  unfold swapped
  exact compose.bijective with swap, bijective

-- Initial segments below a, or containing both a and a + 1, are fixed by
-- the transposition.
theorem transposition.image_below (n : Nat) (a k : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hk : k ⊆ a
  shows functionImage(transposition(n, a, succ(a)), k, n) = k
proof
  have naturals := natural.member at n
  have aNat := naturals with ha
  have aInside := Ordinal.member_subset with (Ordinal.natural at n), ha
  have function := Injective.function with (Bijective.injective with (transposition.bijective at n, a, succ(a) with ha, hb))
  ext y
  constructor
  . intro hy
    simp [functionImage.membership] at hy
    obtain ⟨inN, x, hx, shape⟩ := hy
    have hxa := hk with x, hx
    have xNat := naturals with (aInside with x, hxa)
    have below := Less.of_membership with hxa
    have notFirst : x ≠ a by arith
    have notSecond : x ≠ succ(a) by arith
    have fixed := transposition.other with ha, hb, (aInside with x, hxa), notFirst, notSecond
    rwa [shape, fixed]
  . intro hy
    have hya := hk with y, hy
    have yNat := naturals with (aInside with y, hya)
    have below := Less.of_membership with hya
    have notFirst : y ≠ a by arith
    have notSecond : y ≠ succ(a) by arith
    have inN := aInside with y, hya
    have fixed := transposition.other with ha, hb, inN, notFirst, notSecond
    simp [functionImage.membership]

theorem transposition.image_above (n : Nat) (a k : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hk : k ⊆ n
  requires aIn : a ∈ k
  requires bIn : succ(a) ∈ k
  shows functionImage(transposition(n, a, succ(a)), k, n) = k
proof
  have bijective := transposition.bijective with ha, hb
  have function := Injective.function with (Bijective.injective with bijective)
  have first := transposition.first with ha, hb
  have second := transposition.second with ha, hb
  have closed : ∀ x ∈ k, transposition(n, a, succ(a))(x) ∈ k
    intros x hx
    have split : x = a ∨ x ≠ a by tauto
    cases split with isA | notA
    . rw [isA, first]
      exact bIn
    . have split2 : x = succ(a) ∨ x ≠ succ(a) by tauto
      cases split2 with isB | notB
      . rw [isB, second]
        exact aIn
      . have fixed := transposition.other with ha, hb, (hk with x, hx), notA, notB
        rwa fixed
  ext y
  constructor
  . intro hy
    simp [functionImage.membership] at hy
    obtain ⟨inN, x, hx, shape⟩ := hy
    rw shape
    exact closed with x, hx
  . intro hy
    have preimage := closed with y, hy
    have involution := transposition.involution with ha, hb
    have back : transposition(n, a, succ(a))(transposition(n, a, succ(a))(y)) = y
      exact involution.right with y, (hk with y, hy)
    simp [functionImage.membership]
    constructor
    . exact hk with y, hy
    . witness transposition(n, a, succ(a))(y)
      constructor
      . exact preimage
      . symm
        exact back

-- Raised sets under the swapped order agree except at step a + 1.
theorem raised.swapped (n : Nat) (upd a k : Set)
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hk : k ⊆ n
  shows raised(n, swapped(n, upd, a), k) = functionImage(upd, functionImage(transposition(n, a, succ(a)), k, n), n)
proof
  have updFunction := Injective.function with (Bijective.injective with updBijective)
  have swap := transposition.bijective with ha, hb
  have swapFunction := Injective.function with (Bijective.injective with swap)
  have same : raised(n, swapped(n, upd, a), k) = functionImage(compose(upd, transposition(n, a, succ(a)), n, n, n), k, n)
    unfold raised
    unfold swapped
    rfl
  rw same
  exact functionImage.compose with swapFunction, updFunction, hk

theorem raised.swapped_below (n : Nat) (upd a k : Set)
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hk : k ⊆ a
  shows raised(n, swapped(n, upd, a), k) = raised(n, upd, k)
proof
  have aInside := Ordinal.member_subset with (Ordinal.natural at n), ha
  have inside := Subset.transitive with hk, aInside
  have step := raised.swapped with updBijective, ha, hb, inside
  have image := transposition.image_below with ha, hb, hk
  rw [step, image]
  have same : raised(n, upd, k) = functionImage(upd, k, n)
    unfold raised
    rfl
  rw same
  rfl

theorem raised.swapped_above (n : Nat) (upd a k : Set)
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hk : k ⊆ n
  requires aIn : a ∈ k
  requires bIn : succ(a) ∈ k
  shows raised(n, swapped(n, upd, a), k) = raised(n, upd, k)
proof
  have step := raised.swapped with updBijective, ha, hb, hk
  have image := transposition.image_above with ha, hb, hk, aIn, bIn
  rw [step, image]
  have same : raised(n, upd, k) = functionImage(upd, k, n)
    unfold raised
    rfl
  rw same
  rfl

-- Vertices other than the (a + 1)-st agree; that one differs.
theorem kuhnVertex.swapped_same (n : Nat) (base upd a k : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hk : k ∈ succ(n)
  requires different : k ≠ succ(a)
  shows kuhnVertex(n, base, swapped(n, upd, a))(k) = kuhnVertex(n, base, upd)(k)
proof
  have naturals := natural.member at n
  have aNat := naturals with ha
  have kNat := natural.member at succ(n) with hk
  have kInside := kuhnVertex.index_subset with hk
  have sameRaised : raised(n, swapped(n, upd, a), k) = raised(n, upd, k)
    have order := Ordinal.trichotomy with (Ordinal.natural at k), succ(a), (Ordinal.natural at succ(a))
    cases order with below | rest
    . have kBelow := kuhnVertex.index_subset with below
      exact raised.swapped_below with updBijective, ha, hb, kBelow
    . cases rest with same | above
      . exfalso
        exact different with same
      . have aIn : a ∈ k
          have self := bootstrap.succ.self at a
          have inside := Ordinal.member_subset with (Ordinal.natural at k), above
          exact inside with a, self
        exact raised.swapped_above with updBijective, ha, hb, kInside, aIn, above
  have f1 := kuhnVertex.function_on at n, base, swapped(n, upd, a), k with baseFunction, hk
  have f2 := kuhnVertex.function_on at n, base, upd, k with baseFunction, hk
  apply FunctionBetween.ext with f1, f2
  intros j hj
  have c1 := kuhnVertex.coordinate at n, base, swapped(n, upd, a), k, j with baseFunction, hk, hj
  have c2 := kuhnVertex.coordinate at n, base, upd, k, j with baseFunction, hk, hj
  rw [c1, c2, sameRaised]
  rfl

theorem transposition.image_step (n : Nat) (a : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows functionImage(transposition(n, a, succ(a)), succ(a), n) = insert(succ(a), a)
proof
  have naturals := natural.member at n
  have aNat := naturals with ha
  have aInside := Ordinal.member_subset with (Ordinal.natural at n), ha
  have bijective := transposition.bijective with ha, hb
  have function := Injective.function with (Bijective.injective with bijective)
  have first := transposition.first with ha, hb
  have self := bootstrap.succ.self at a
  ext y
  constructor
  . intro hy
    simp [functionImage.membership] at hy
    obtain ⟨inN, x, hx, shape⟩ := hy
    have split := bootstrap.succ.membership.forward with hx
    apply insert.membership.backward
    cases split with below | same
    . right
      have xNat := naturals with (aInside with x, below)
      have less := Less.of_membership with below
      have notFirst : x ≠ a by arith
      have notSecond : x ≠ succ(a) by arith
      have fixed := transposition.other with ha, hb, (aInside with x, below), notFirst, notSecond
      rwa [shape, fixed]
    . left
      rw [shape, same, first]
      rfl
  . intro hy
    have split := insert.membership.forward with hy
    cases split with same | below
    . rw same
      simp [functionImage.membership]
      constructor
      . exact hb
      . witness a
        constructor
        . exact self
        . symm
          exact first
    . have xNat := naturals with (aInside with y, below)
      have less := Less.of_membership with below
      have notFirst : y ≠ a by arith
      have notSecond : y ≠ succ(a) by arith
      have inN := aInside with y, below
      have fixed := transposition.other with ha, hb, inN, notFirst, notSecond
      have inSucc := membership.into_successor with below
      simp [functionImage.membership]

theorem kuhnVertex.swapped_differs (n : Nat) (base upd a : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows kuhnVertex(n, base, swapped(n, upd, a))(succ(a)) ≠ kuhnVertex(n, base, upd)(succ(a))
proof
  have updInjective := Bijective.injective with updBijective
  have updFunction := Injective.function with updInjective
  have bIn := membership.into_successor with hb
  have coordinate := FunctionBetween.apply_closed with updFunction, hb
  have c1 := kuhnVertex.coordinate at n, base, swapped(n, upd, a), succ(a), upd(succ(a)) with baseFunction, bIn, coordinate
  have c2 := kuhnVertex.coordinate at n, base, upd, succ(a), upd(succ(a)) with baseFunction, bIn, coordinate
  have bInside := Ordinal.member_subset with (Ordinal.natural at n), hb
  have step := raised.swapped with updBijective, ha, hb, bInside
  have image := transposition.image_step with ha, hb
  rw image at step
  have inRaised : upd(succ(a)) ∈ raised(n, swapped(n, upd, a), succ(a))
    rw step
    have inInsert : succ(a) ∈ insert(succ(a), a)
      apply insert.membership.backward
      left
      rfl
    simp [functionImage.membership]
  have fresh := raised.fresh with updInjective, hb
  have one := indicator.member with inRaised
  have zero := indicator.absent with fresh
  intro equal
  have values : kuhnVertex(n, base, swapped(n, upd, a))(succ(a))(upd(succ(a))) = kuhnVertex(n, base, upd)(succ(a))(upd(succ(a)))
    rw equal
    rfl
  rw [c1, c2, one, zero] at values
  have baseValue := FunctionBetween.apply_closed with baseFunction, coordinate
  have baseNat := nat.omega.backward with baseValue
  arith

-- Helpers: indicators separate sets; equal vertices force equal raised
-- sets and equal bases; equal vertex maps give equal simplices.
theorem indicator.separates (A B j : Set)
  requires same : indicator(A, j) = indicator(B, j)
  shows j ∈ A ↔ j ∈ B
proof
  constructor
  . intro inA
    have one := indicator.member with inA
    by_contra outB
    have zero := indicator.absent with outB
    rw [one, zero] at same
    apply zero.ne_one
    symm
    exact same
  . intro inB
    have one := indicator.member with inB
    by_contra outA
    have zero := indicator.absent with outA
    rw [one, zero] at same
    exact zero.ne_one with same

theorem raised.of_vertex (n : Nat) (base u v k : Set)
  requires baseFunction : base : n → ℕ
  requires hk : k ∈ succ(n)
  requires same : kuhnVertex(n, base, u)(k) = kuhnVertex(n, base, v)(k)
  shows raised(n, u, k) = raised(n, v, k)
proof
  have insideU := raised.subset at n, u, k
  have insideV := raised.subset at n, v, k
  ext j
  constructor
  . intro hj
    have hjn := insideU with j, hj
    have c1 := kuhnVertex.coordinate at n, base, u, k, j with baseFunction, hk, hjn
    have c2 := kuhnVertex.coordinate at n, base, v, k, j with baseFunction, hk, hjn
    have values : kuhnVertex(n, base, u)(k)(j) = kuhnVertex(n, base, v)(k)(j)
      rw same
      rfl
    rw [c1, c2] at values
    have baseValue := FunctionBetween.apply_closed with baseFunction, hjn
    have baseNat := nat.omega.backward with baseValue
    have tagU := indicator.natural at raised(n, u, k), j
    have tagV := indicator.natural at raised(n, v, k), j
    have tags : indicator(raised(n, u, k), j) = indicator(raised(n, v, k), j) by exact add.left_cancel with values
    have equivalent := indicator.separates with tags
    exact equivalent.forward with hj
  . intro hj
    have hjn := insideV with j, hj
    have c1 := kuhnVertex.coordinate at n, base, u, k, j with baseFunction, hk, hjn
    have c2 := kuhnVertex.coordinate at n, base, v, k, j with baseFunction, hk, hjn
    have values : kuhnVertex(n, base, u)(k)(j) = kuhnVertex(n, base, v)(k)(j)
      rw same
      rfl
    rw [c1, c2] at values
    have baseValue := FunctionBetween.apply_closed with baseFunction, hjn
    have baseNat := nat.omega.backward with baseValue
    have tags : indicator(raised(n, u, k), j) = indicator(raised(n, v, k), j) by exact add.left_cancel with values
    have equivalent := indicator.separates with tags
    exact equivalent.backward with hj

theorem kuhnSimplex.base_of_bottom (n : Nat) (b1 u1 b2 u2 : Set)
  requires f1 : b1 : n → ℕ
  requires f2 : b2 : n → ℕ
  requires same : kuhnVertex(n, b1, u1)(0) = kuhnVertex(n, b2, u2)(0)
  shows b1 = b2
proof
  apply FunctionBetween.ext with f1, f2
  intros j hj
  have z1 := kuhnVertex.zero_coordinate at n, b1, u1, j with f1, hj
  have z2 := kuhnVertex.zero_coordinate at n, b2, u2, j with f2, hj
  have values : kuhnVertex(n, b1, u1)(0)(j) = kuhnVertex(n, b2, u2)(0)(j)
    rw same
    rfl
  rwa [z1, z2] at values

theorem kuhnSimplex.ext_of_vertices (n : Nat) (b1 u1 b2 u2 : Set)
  requires f1 : b1 : n → ℕ
  requires f2 : b2 : n → ℕ
  requires same : ∀ k ∈ succ(n), kuhnVertex(n, b1, u1)(k) = kuhnVertex(n, b2, u2)(k)
  shows kuhnSimplex(n, b1, u1) = kuhnSimplex(n, b2, u2)
proof
  ext x
  constructor
  . intro hx
    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hx
    have equal := same with hk
    rw [shape, equal]
    exact kuhnVertex.member with f2, hk
  . intro hx
    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hx
    have equal := same with hk
    rw [shape, ← equal]
    exact kuhnVertex.member with f1, hk

-- The swapped simplex shares the face opposite the (a + 1)-st vertex.
theorem kuhnSimplex.swapped_face (n : Nat) (base upd a : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(succ(a))} =
    kuhnSimplex(n, base, swapped(n, upd, a)) ∖ {kuhnVertex(n, base, swapped(n, upd, a))(succ(a))}
proof
  have updInjective := Bijective.injective with updBijective
  have swapInjective := Bijective.injective with (swapped.bijective with updBijective, ha, hb)
  have bIn := membership.into_successor with hb
  ext x
  constructor
  . intro hx
    have parts := difference.singleton_membership.forward with hx
    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left
    have different : k ≠ succ(a)
      intro same
      apply parts.right
      rw [shape, same]
      rfl
    have agree := kuhnVertex.swapped_same with baseFunction, updBijective, ha, hb, hk, different
    apply difference.singleton_membership.backward
    constructor
    . rw [shape, ← agree]
      exact kuhnVertex.member with baseFunction, hk
    . intro equal
      rw [shape, ← agree] at equal
      have same := kuhnVertex.injective with baseFunction, swapInjective, hk, bIn, equal
      exact different with same
  . intro hx
    have parts := difference.singleton_membership.forward with hx
    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left
    have different : k ≠ succ(a)
      intro same
      apply parts.right
      rw [shape, same]
      rfl
    have agree := kuhnVertex.swapped_same with baseFunction, updBijective, ha, hb, hk, different
    apply difference.singleton_membership.backward
    constructor
    . rw [shape, agree]
      exact kuhnVertex.member with baseFunction, hk
    . intro equal
      rw [shape, agree] at equal
      have same := kuhnVertex.injective with baseFunction, updInjective, hk, bIn, equal
      exact different with same

theorem kuhnVertex.of_raised (n : Nat) (base u v k : Set)
  requires baseFunction : base : n → ℕ
  requires hk : k ∈ succ(n)
  requires same : raised(n, u, k) = raised(n, v, k)
  shows kuhnVertex(n, base, u)(k) = kuhnVertex(n, base, v)(k)
proof
  have f1 := kuhnVertex.function_on at n, base, u, k with baseFunction, hk
  have f2 := kuhnVertex.function_on at n, base, v, k with baseFunction, hk
  apply FunctionBetween.ext with f1, f2
  intros j hj
  have c1 := kuhnVertex.coordinate at n, base, u, k, j with baseFunction, hk, hj
  have c2 := kuhnVertex.coordinate at n, base, v, k, j with baseFunction, hk, hj
  rw [c1, c2, same]
  rfl

theorem raised.swapped_step (n : Nat) (upd a : Set)
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows raised(n, swapped(n, upd, a), succ(a)) = insert(upd(succ(a)), raised(n, upd, a))
proof
  have updFunction := Injective.function with (Bijective.injective with updBijective)
  have bInside := Ordinal.member_subset with (Ordinal.natural at n), hb
  have step := raised.swapped with updBijective, ha, hb, bInside
  have image := transposition.image_step with ha, hb
  have inserted := functionImage.insert at upd, n, n, succ(a), a with updFunction, hb
  have same : raised(n, upd, a) = functionImage(upd, a, n)
    unfold raised
    rfl
  rw [step, image, inserted, same]
  rfl

-- Across an interior face, the only simplices are the simplex itself and
-- its swapped neighbour.
theorem kuhnSimplex.interior_neighbours (n : Nat) (b u a b2 u2 c : Set)
  requires f1 : b : n → ℕ
  requires bij1 : BijectiveBetween(u, n, n)
  requires f2 : b2 : n → ℕ
  requires bij2 : BijectiveBetween(u2, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hc : c ∈ kuhnSimplex(n, b2, u2)
  requires same : kuhnSimplex(n, b2, u2) ∖ {c} = kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(succ(a))}
  shows kuhnSimplex(n, b2, u2) = kuhnSimplex(n, b, u) ∨
    kuhnSimplex(n, b2, u2) = kuhnSimplex(n, b, swapped(n, u, a))
proof
  have inj1 := Bijective.injective with bij1
  have inj2 := Bijective.injective with bij2
  have fun1 := Injective.function with inj1
  have fun2 := Injective.function with inj2
  have zeroNat : Nat(0) by typecheck
  have naturals := natural.member at n
  have aNat := naturals with ha
  have iIn := membership.into_successor with hb
  have positive : 0 < succ(n) by arith
  have zeroIn := membership.of_Less with positive
  have nIn := bootstrap.succ.self at n
  have aIn := membership.into_successor with ha
  have bBelow := Less.of_membership with hb
  have ssBelow : succ(succ(a)) < succ(n) by arith
  have ssIn := membership.of_Less with ssBelow
  have inT : ∀ k ∈ succ(n), k ≠ succ(a) → kuhnVertex(n, b, u)(k) ∈ kuhnSimplex(n, b2, u2)
    intros k hk different
    have member := kuhnVertex.member at n, b, u, k with f1, hk
    have notMissing : kuhnVertex(n, b, u)(k) ≠ kuhnVertex(n, b, u)(succ(a))
      intro equal
      have sameIndex := kuhnVertex.injective with f1, inj1, hk, iIn, equal
      exact different with sameIndex
    have inFace : kuhnVertex(n, b, u)(k) ∈ kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(succ(a))}
      exact difference.singleton_membership.backward with ⟨member, notMissing⟩
    rw ← same at inFace
    have parts := difference.singleton_membership.forward with inFace
    exact parts.left
  have zeroDifferent : 0 ≠ succ(a) by arith
  have nDifferent : n ≠ succ(a)
    intro equal
    rw equal at hb
    have irreflexive := Ordinal.not_member_self at succ(a)
    exact irreflexive with hb
  have v0 := inT with 0, zeroIn, zeroDifferent
  have vn := inT with n, nIn, nDifferent
  have bounds0 := kuhnSimplex.sum_bounds with f2, inj2, v0
  have boundsN := kuhnSimplex.sum_bounds with f2, inj2, vn
  have sum0 := kuhnVertex.sum with f1, inj1, zeroIn
  have sumN := kuhnVertex.sum with f1, inj1, nIn
  have weights1 : ∀ j ∈ n, b(j) ∈ ℕ
    intros j hj
    exact FunctionBetween.apply_closed with f1, hj
  have weights2 : ∀ j ∈ n, b2(j) ∈ ℕ
    intros j hj
    exact FunctionBetween.apply_closed with f2, hj
  have total1 := natSum.natural with (Finite.natural at n), weights1
  have total2 := natSum.natural with (Finite.natural at n), weights2
  have lower := bounds0.left
  have upper := boundsN.right
  rw sum0 at lower
  rw sumN at upper
  rw add.right_unit at lower
  have upper2 := LessEqual.add_right_cancel with upper
  have equalSums := LessEqual.antisymmetric with lower, upper2
  have agree : ∀ k ∈ succ(n), k ≠ succ(a) → kuhnVertex(n, b, u)(k) = kuhnVertex(n, b2, u2)(k)
    intros k hk different
    have inside := inT with k, hk, different
    have total := kuhnVertex.sum with f1, inj1, hk
    rw ← equalSums at total
    exact kuhnSimplex.vertex_of_sum with f2, inj2, inside, hk, total
  have bases := kuhnSimplex.base_of_bottom with f1, f2, (agree with 0, zeroIn, zeroDifferent)
  have aDifferent : a ≠ succ(a) by arith
  have ssDifferent : succ(succ(a)) ≠ succ(a) by arith
  have agreeA := agree with a, aIn, aDifferent
  have agreeSS := agree with succ(succ(a)), ssIn, ssDifferent
  rw ← bases at agreeA
  rw ← bases at agreeSS
  have raisedA := raised.of_vertex with f1, aIn, agreeA
  have raisedSS := raised.of_vertex with f1, ssIn, agreeSS
  have stepU2 := raised.succ with fun2, ha
  have stepU2b := raised.succ with fun2, hb
  have stepU := raised.succ with fun1, ha
  have stepUb := raised.succ with fun1, hb
  have u2aIn : u2(a) ∈ raised(n, u, succ(succ(a)))
    rw [raisedSS, stepU2b, stepU2]
    apply insert.membership.backward
    right
    apply insert.membership.backward
    left
    rfl
  rw [stepUb, stepU] at u2aIn
  have fresh2 := raised.fresh with inj2, ha
  rw ← raisedA at fresh2
  have split := insert.membership.forward with u2aIn
  cases split with isB | rest
  . right
    have raisedStep : raised(n, u2, succ(a)) = raised(n, swapped(n, u, a), succ(a))
      rw [stepU2, ← raisedA, isB]
      have swappedStep := raised.swapped_step with bij1, ha, hb
      rw swappedStep
      rfl
    rw ← bases
    apply kuhnSimplex.ext_of_vertices with f1, f1
    intros k hk
    have split2 : k = succ(a) ∨ k ≠ succ(a) by tauto
    cases split2 with isStep | other
    . rw isStep
      exact kuhnVertex.of_raised with f1, iIn, raisedStep
    . have fromS := agree with k, hk, other
      rw ← bases at fromS
      have toSwapped := kuhnVertex.swapped_same with f1, bij1, ha, hb, hk, other
      rw [← fromS, toSwapped]
      rfl
  . have split3 := insert.membership.forward with rest
    cases split3 with isA | inA
    . left
      have raisedStep : raised(n, u2, succ(a)) = raised(n, u, succ(a))
        rw [stepU2, ← raisedA, isA, stepU]
        rfl
      rw ← bases
      apply kuhnSimplex.ext_of_vertices with f1, f1
      intros k hk
      have split2 : k = succ(a) ∨ k ≠ succ(a) by tauto
      cases split2 with isStep | other
      . rw isStep
        exact kuhnVertex.of_raised with f1, iIn, raisedStep
      . have fromS := agree with k, hk, other
        rw ← bases at fromS
        symm
        exact fromS
    . exfalso
      exact fresh2 with inA