-- Real analysis: PartitionSplit
-- 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.Real.Analysis.Integration.PartitionSplit
import Nat.Least
import CommonRefinementComparison
import RiemannSums
import Nat.Order

-- Section: PartitionSplit
theorem riemannSum.two_cell_left (f : Set) (A C B : Real)
  requires function : f : ℝ → ℝ
  shows riemannSum(f, twoCellPoints(A, C, B), twoCellPoints(A, C, B),
      succ(succ(0))) =
    f(A) * (C - A) + f(C) * (B - C)
proof
  have points := twoCellPoints.sequence at A, C, B with *
  have first := riemannSum.succ at f, twoCellPoints(A, C, B),
    twoCellPoints(A, C, B), 0 with function, points, points
  have second := riemannSum.succ at f, twoCellPoints(A, C, B),
    twoCellPoints(A, C, B), succ(0) with function, points, points
  rw riemannSum.zero at first
  rw twoCellPoints.zero at first
  rw twoCellPoints.one at first
  rw twoCellPoints.one at second
  rw twoCellPoints.two at second
  rw first at second
  rw second
  ring

-- SumCongruence
theorem riemannSum.congr_cells (f p t q s : Set, N : Nat)
  requires function : f : ℝ → ℝ
  requires pointsP : RealSequence(p)
  requires pointsQ : RealSequence(q)
  requires tagsT : RealSequence(t)
  requires tagsS : RealSequence(s)
  requires cells : ∀ i ∈ ℕ, i < N →
    p[i] = q[i] ∧ p[succ(i)] = q[succ(i)] ∧ t[i] = s[i]
  shows riemannSum(f, p, t, N) = riemannSum(f, q, s, N)
proof
  have termsP : RealSequence(riemannTerms(f, p, t))
    unfold RealSequence
    exact riemannTerms.function with function, pointsP, tagsT
  have termsQ : RealSequence(riemannTerms(f, q, s))
    unfold RealSequence
    exact riemannTerms.function with function, pointsQ, tagsS
  have equalTerms : ∀ i ∈ ℕ, i < N →
      riemannTerms(f, p, t)[i] = riemannTerms(f, q, s)[i]
    intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    obtain ⟨atI, atNext, atTag⟩ := cells with i, naturalI, before
    have termP := riemannTerms.value at f, p, t, i with function, pointsP, tagsT
    have termQ := riemannTerms.value at f, q, s, i with function, pointsQ, tagsS
    rw [termP, termQ, atI, atNext, atTag]
    rfl
  unfold riemannSum
  exact realPartialSum.eq_prefix with termsP, termsQ, equalTerms

-- ShiftedRiemannSums
theorem riemannTerms.shifted (f p t : Set, n i : Nat)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  requires tags : RealSequence(t)
  shows riemannTerms(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n))[i] =
    shiftedRealSequence(riemannTerms(f, p, t), n)[i]
proof
  have shiftedP := shiftedRealSequence.sequence at p, n with points
  have shiftedT := shiftedRealSequence.sequence at t, n with tags
  have terms : RealSequence(riemannTerms(f, p, t))
    unfold RealSequence
    exact riemannTerms.function with function, points, tags
  have shiftedTerm := riemannTerms.value at
    f, shiftedRealSequence(p, n), shiftedRealSequence(t, n), i with
      function, shiftedP, shiftedT
  have originalTerm := riemannTerms.value at f, p, t, add(n, i) with
    function, points, tags
  have rhs := shiftedRealSequence.value at riemannTerms(f, p, t), n, i with terms
  have tag := shiftedRealSequence.value at t, n, i with tags
  have left := shiftedRealSequence.value at p, n, i with points
  have right := shiftedRealSequence.value at p, n, succ(i) with points
  rw [shiftedTerm, rhs, originalTerm, tag, left, right, add.succ_right]
  rfl

theorem riemannSum.split_at (f p t : Set, n m : Nat)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  requires tags : RealSequence(t)
  shows riemannSum(f, p, t, add(n, m)) =
    riemannSum(f, p, t, n) +
      riemannSum(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n), m)
proof
  have shiftedP := shiftedRealSequence.sequence at p, n with points
  have shiftedT := shiftedRealSequence.sequence at t, n with tags
  have terms : RealSequence(riemannTerms(f, p, t))
    unfold RealSequence
    exact riemannTerms.function with function, points, tags
  have shiftedTerms : RealSequence(shiftedRealSequence(riemannTerms(f, p, t), n))
    exact shiftedRealSequence.sequence with terms
  have suffixTerms : RealSequence(riemannTerms(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n)))
    unfold RealSequence
    exact riemannTerms.function with function, shiftedP, shiftedT
  have equal : ∀ i ∈ ℕ, i < m →
      shiftedRealSequence(riemannTerms(f, p, t), n)[i] =
        riemannTerms(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n))[i]
    intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    have value := riemannTerms.shifted at f, p, t, n, i with
      function, points, tags
    rw value
    rfl
  have equalSums := realPartialSum.eq_prefix with shiftedTerms, suffixTerms, equal
  have split := realPartialSum.split_at at riemannTerms(f, p, t), n, m with terms
  rw equalSums at split
  simp [riemannSum]

-- ShiftedPartitions
theorem IntervalPartition.suffix (p : Set) (A B : Real, n m : Nat)
  requires partition : IntervalPartition(p, A, B, add(n, m))
  shows IntervalPartition(shiftedRealSequence(p, n), p[n], B, m)
proof
  rcases partition with ⟨points, start, finish, increasing⟩
  have shifted := shiftedRealSequence.sequence at p, n with points
  have atZero := shiftedRealSequence.value at p, n, 0 with points
  have atEnd := shiftedRealSequence.value at p, n, m with points
  have plusZero := add.right_unit at n
  rw plusZero at atZero
  constructor
  . exact shifted
  . constructor
    . exact atZero
    . constructor
      . rw atEnd
        exact finish
      . intros j naturalJ before
        have typedJ := nat.omega.backward with naturalJ
        have index := add.closed at j, n with typedJ
        have reflexive := LessEqual.reflexive at n with assumption
        have shiftedBefore := LessEqual.add_Less with reflexive, before
        have step := increasing with add(n, j), nat.omega.forward at add(n, j) with index, shiftedBefore
        have left := shiftedRealSequence.value at p, n, j with points
        have right := shiftedRealSequence.value at p, n, succ(j) with points
        rwa [left, right, add.succ_right]

theorem TaggedPartition.suffix (p t : Set) (A B : Real, n m : Nat)
  requires tagged : TaggedPartition(p, t, A, B, add(n, m))
  shows TaggedPartition(shiftedRealSequence(p, n), shiftedRealSequence(t, n), p[n], B, m)
proof
  rcases tagged with ⟨partition, tags, cells⟩
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have suffix := IntervalPartition.suffix with partition
  have shiftedTags := shiftedRealSequence.sequence at t, n with tags
  constructor
  . exact suffix
  . constructor
    . exact shiftedTags
    . intros j naturalJ before
      have typedJ := nat.omega.backward with naturalJ
      have index := add.closed at j, n with typedJ
      have reflexive := LessEqual.reflexive at n with assumption
      have shiftedBefore := LessEqual.add_Less with reflexive, before
      have cell := cells with add(n, j), nat.omega.forward at add(n, j) with index, shiftedBefore
      have tag := shiftedRealSequence.value at t, n, j with tags
      have left := shiftedRealSequence.value at p, n, j with points
      have right := shiftedRealSequence.value at p, n, succ(j) with points
      rwa [tag, left, right, add.succ_right]

theorem FinePartition.suffix (p : Set) (A B D : Real, n m : Nat)
  requires fine : FinePartition(p, A, B, add(n, m), D)
  shows FinePartition(shiftedRealSequence(p, n), p[n], B, m, D)
proof
  rcases fine with ⟨partition, positive, widths⟩
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have suffix := IntervalPartition.suffix with partition
  constructor
  . exact suffix
  . constructor
    . exact positive
    . intros j naturalJ before
      have typedJ := nat.omega.backward with naturalJ
      have index := add.closed at j, n with typedJ
      have reflexive := LessEqual.reflexive at n with assumption
      have shiftedBefore := LessEqual.add_Less with reflexive, before
      have bound := widths with add(n, j), nat.omega.forward at add(n, j) with index, shiftedBefore
      have left := shiftedRealSequence.value at p, n, j with points
      have right := shiftedRealSequence.value at p, n, succ(j) with points
      rwa [left, right, add.succ_right]

theorem IntervalPartition.prefix (p : Set) (A B : Real, n m : Nat)
  requires partition : IntervalPartition(p, A, B, add(n, m))
  shows IntervalPartition(p, A, p[n], n)
proof
  rcases partition with ⟨points, start, finish, increasing⟩
  constructor
  . exact points
  . constructor
    . exact start
    . constructor
      . rfl
      . intros j naturalJ before
        have typedJ := nat.omega.backward with naturalJ
        have nLe := LessEqual.add_right at n, m with *
        have originalBefore := Less.transitive_LessEqual with before, nLe
        exact increasing with j, naturalJ, originalBefore

theorem TaggedPartition.prefix (p t : Set) (A B : Real, n m : Nat)
  requires tagged : TaggedPartition(p, t, A, B, add(n, m))
  shows TaggedPartition(p, t, A, p[n], n)
proof
  rcases tagged with ⟨partition, tags, cells⟩
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have pointN := RealSequence.value at p, n with points
  have prefix := IntervalPartition.prefix with partition
  constructor
  . exact prefix
  . constructor
    . exact tags
    . intros j naturalJ before
      have typedJ := nat.omega.backward with naturalJ
      have nLe := LessEqual.add_right at n, m with *
      have originalBefore := Less.transitive_LessEqual with before, nLe
      exact cells with j, naturalJ, originalBefore

theorem FinePartition.prefix (p : Set) (A B D : Real, n m : Nat)
  requires fine : FinePartition(p, A, B, add(n, m), D)
  shows FinePartition(p, A, p[n], n, D)
proof
  rcases fine with ⟨partition, positive, widths⟩
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have pointN := RealSequence.value at p, n with points
  have prefix := IntervalPartition.prefix with partition
  constructor
  . exact prefix
  . constructor
    . exact positive
    . intros j naturalJ before
      have typedJ := nat.omega.backward with naturalJ
      have nLe := LessEqual.add_right at n, m with *
      have originalBefore := Less.transitive_LessEqual with before, nLe
      exact widths with j, naturalJ, originalBefore

-- PartitionSplit
theorem FinePartition.split_tagged_sum (f p t : Set) (A B D : Real, n m : Nat)
  requires function : f : ℝ → ℝ
  requires fine : FinePartition(p, A, B, add(n, m), D)
  requires tagged : TaggedPartition(p, t, A, B, add(n, m))
  shows FinePartition(p, A, p[n], n, D) ∧
    FinePartition(shiftedRealSequence(p, n), p[n], B, m, D) ∧
    TaggedPartition(p, t, A, p[n], n) ∧
    TaggedPartition(shiftedRealSequence(p, n), shiftedRealSequence(t, n), p[n], B, m) ∧
    riemannSum(f, p, t, add(n, m)) =
      (riemannSum(f, p, t, n):R) +
        (riemannSum(f, shiftedRealSequence(p, n), shiftedRealSequence(t, n), m):R)
proof
  have partition : IntervalPartition(p, A, B, add(n, m))
    rcases fine with ⟨partition, positive, widths⟩
    exact partition
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have pointN := RealSequence.value at p, n with points
  have tags : RealSequence(t)
    rcases tagged with ⟨partitionT, tags, cells⟩
    exact tags
  have finePrefix := FinePartition.prefix with fine
  have fineSuffix := FinePartition.suffix with fine
  have taggedPrefix := TaggedPartition.prefix with tagged
  have taggedSuffix := TaggedPartition.suffix with tagged
  have sum := riemannSum.split_at at f, p, t, n, m with function, points, tags
  refine ⟨finePrefix, fineSuffix, taggedPrefix, taggedSuffix, sum⟩

-- Section: IndexedInsertionSplit
def firstCellTailPoint (p : Set, C : Real, n : Nat) → Set
  | p, C, zero => C
  | p, C, succ(k) => p[succ(k)]

def firstCellInsertedPoint (p : Set, C : Real, n : Nat) → Set
  | p, C, zero => p[0]
  | p, C, succ(k) => firstCellTailPoint(p, C, k)

theorem firstCellTailPoint.real (p : Set) (C : Real, n : Nat)
  requires points : RealSequence(p)
  shows Real(firstCellTailPoint(p, C, n))
proof
  induction n
  | zero =>
    rwa firstCellTailPoint
  | succ(k) using ih =>
    rw firstCellTailPoint
    exact RealSequence.value with points

theorem firstCellInsertedPoint.real (p : Set) (C : Real, n : Nat)
  requires points : RealSequence(p)
  shows Real(firstCellInsertedPoint(p, C, n))
proof
  induction n
  | zero =>
    rw firstCellInsertedPoint
    exact RealSequence.value with points
  | succ(k) using ih =>
    rw firstCellInsertedPoint
    exact firstCellTailPoint.real with points

defgraph firstCellInsertedPoints (p : Set, C : Real) (n ∈ ℕ) : ℝ :=
  firstCellInsertedPoint(p, C, n)
requires points : RealSequence(p)
proof
  have typedN := nat.omega.backward with member
  exact firstCellInsertedPoint.real with points

theorem firstCellInsertedPoints.sequence (p : Set, C : Real)
  requires points : RealSequence(p)
  shows RealSequence(firstCellInsertedPoints(p, C))
proof
  unfold RealSequence
  exact firstCellInsertedPoints.function with points

theorem firstCellInsertedPoints.zero (p : Set, C : Real)
  requires points : RealSequence(p)
  shows firstCellInsertedPoints(p, C)[0] = p[0]
proof
  have value := firstCellInsertedPoints.value at p, C, 0 with points
  rwa firstCellInsertedPoint at value

theorem firstCellInsertedPoints.one (p : Set, C : Real)
  requires points : RealSequence(p)
  shows firstCellInsertedPoints(p, C)[succ(0)] = C
proof
  have value := firstCellInsertedPoints.value at p, C, succ(0) with points
  rwa [firstCellInsertedPoint, firstCellTailPoint] at value

theorem firstCellInsertedPoints.later (p : Set, C : Real, k : Nat)
  requires points : RealSequence(p)
  shows firstCellInsertedPoints(p, C)[succ(succ(k))] = p[succ(k)]
proof
  have value := firstCellInsertedPoints.value at p, C, succ(succ(k)) with points
  rwa [firstCellInsertedPoint, firstCellTailPoint] at value

theorem IntervalPartition.insert_first_cell (p : Set) (A B C : Real, K : Nat)
  requires partition : IntervalPartition(p, A, B, succ(K))
  requires left : A < C
  requires right : C < (p[succ(0)]:R)
  shows IntervalPartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)))
proof
  rcases partition with ⟨points, start, finish, increasing⟩
  have inserted := firstCellInsertedPoints.sequence at p, C with points
  constructor
  . exact inserted
  . constructor
    . have atZero := firstCellInsertedPoints.zero at p, C with points
      rwa atZero
    . constructor
      . have atEnd := firstCellInsertedPoints.later at p, C, K with points
        rwa atEnd
      . intros i naturalI before
        have typedI := nat.omega.backward with naturalI
        have shape := natural.zero_or_successor with typedI
        cases shape with zero | successor
        . rw [zero, firstCellInsertedPoints.zero, firstCellInsertedPoints.one, start]
          exact left
        . obtain ⟨j, naturalJ, isNext⟩ := successor
          rw isNext
          have jShape := natural.zero_or_successor with naturalJ
          cases jShape with zero | successorJ
          . rw [zero, firstCellInsertedPoints.one, firstCellInsertedPoints.later]
            exact right
          . obtain ⟨k, naturalK, jNext⟩ := successorJ
            rw jNext
            rw [isNext, jNext] at before
            have succK := Naturals.constructor.succ at K with assumption
            have shiftedBefore : Less(add(succ(k), 1), add(succ(K), 1)) by rwa [add.right_one, add.right_one]
            have oldBefore : Less(succ(k), succ(K)) by exact Less.add_right_cancel with shiftedBefore
            have old := increasing with succ(k),
              nat.omega.forward at succ(k) with Naturals.constructor.succ at k with naturalK,
              oldBefore
            rwa [firstCellInsertedPoints.later, firstCellInsertedPoints.later]

-- FirstCellFine
theorem FinePartition.insert_first_cell (p : Set) (A B C D : Real, K : Nat)
  requires fine : FinePartition(p, A, B, succ(K), D)
  requires left : A < C
  requires right : C < (p[succ(0)]:R)
  shows FinePartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)), D)
proof
  rcases fine with ⟨partition, positive, widths⟩
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have pointZero := RealSequence.value with points
  have pointOne := RealSequence.value at p, succ(0) with points
  have start : p[0] = A
    rcases partition with ⟨points, start, finish, increasing⟩
    exact start
  have beforeZero : Less(0, succ(K))
    unfold Less
    have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at K with assumption
    have shifted := LessEqual.add_monotone_right at 0, K, 1 with zeroLe
    simp [add.right_one, add] at shifted
    exact shifted
  have originalWidth := widths with 0,
    nat.omega.forward at 0 with Naturals.constructor.zero, beforeZero
  rw start at originalWidth
  have firstCompare := realSubValue.lt_left at C, p[succ(0)], A with right
  have firstWidth : C - A < D by exact realLess.transitive with firstCompare, originalWidth
  have weakLeft := realLess.implies_le with left
  have self := realLe.reflexive with pointOne
  have secondCompare := realSubValue.le with self, weakLeft
  have secondWidth : (p[succ(0)]:R) - C < D by exact realLe.transitive_less with secondCompare, originalWidth
  have inserted := IntervalPartition.insert_first_cell with partition, left, right
  constructor
  . exact inserted
  . constructor
    . exact positive
    . intros i naturalI before
      have typedI := nat.omega.backward with naturalI
      have shape := natural.zero_or_successor with typedI
      cases shape with zero | successor
      . rw [zero, firstCellInsertedPoints.zero, firstCellInsertedPoints.one, start]
        exact firstWidth
      . obtain ⟨j, naturalJ, isNext⟩ := successor
        rw isNext
        have jShape := natural.zero_or_successor with naturalJ
        cases jShape with zero | successorJ
        . rw [zero, firstCellInsertedPoints.one, firstCellInsertedPoints.later]
          exact secondWidth
        . obtain ⟨k, naturalK, jNext⟩ := successorJ
          rw jNext
          rw [isNext, jNext] at before
          have succK := Naturals.constructor.succ at K with assumption
          have succk := Naturals.constructor.succ with naturalK
          have shiftedBefore : Less(add(succ(k), 1), add(succ(K), 1)) by rwa [add.right_one, add.right_one]
          have oldBefore := Less.add_right_cancel with shiftedBefore
          have old := widths with succ(k),
            nat.omega.forward at succ(k) with succk, oldBefore
          rwa [firstCellInsertedPoints.later, firstCellInsertedPoints.later]

theorem FinePartition.insert_first_cell_tagged (p : Set) (A B C D : Real, K : Nat)
  requires fine : FinePartition(p, A, B, succ(K), D)
  requires left : A < C
  requires right : C < (p[succ(0)]:R)
  shows TaggedPartition(firstCellInsertedPoints(p, C),
      leftPartitionTags(firstCellInsertedPoints(p, C)), A, B, succ(succ(K))) ∧
    FinePartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)), D)
proof
  have inserted := FinePartition.insert_first_cell with fine, left, right
  have partition : IntervalPartition(firstCellInsertedPoints(p, C), A, B, succ(succ(K)))
    rcases inserted with ⟨partition, positive, widths⟩
    exact partition
  have tagged := IntervalPartition.left_tagged with partition
  refine ⟨tagged, inserted⟩

-- IndexedInsertion
def prependRealPoint (A : Real, u : Set, n : Nat) → Set
  | A, u, zero => A
  | A, u, succ(j) => u[j]

theorem prependRealPoint.real (A : Real, u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows Real(prependRealPoint(A, u, n))
proof
  induction n
  | zero =>
    rwa prependRealPoint
  | succ(j) using ih =>
    rw prependRealPoint
    exact RealSequence.value with sequence

defgraph prependRealSequence (A : Real, u : Set) (n ∈ ℕ) : ℝ :=
  prependRealPoint(A, u, n)
requires sequence : RealSequence(u)
proof
  exact prependRealPoint.real with sequence

theorem prependRealSequence.sequence (A : Real, u : Set)
  requires sequence : RealSequence(u)
  shows RealSequence(prependRealSequence(A, u))
proof
  unfold RealSequence
  exact prependRealSequence.function with sequence

theorem prependRealSequence.zero (A : Real, u : Set)
  requires sequence : RealSequence(u)
  shows prependRealSequence(A, u)[0] = A
proof
  have value := prependRealSequence.value at A, u, 0 with sequence
  rwa prependRealPoint at value

theorem prependRealSequence.succ (A : Real, u : Set, j : Nat)
  requires sequence : RealSequence(u)
  shows prependRealSequence(A, u)[succ(j)] = u[j]
proof
  have value := prependRealSequence.value at A, u, succ(j) with sequence
  rwa prependRealPoint at value

-- Primitive recursion on the cell index. The unchanged first point is
-- prepended to an insertion in the shifted tail.
def indexedInsertedPoints (p : Set, C : Real, k : Nat) → Set
  | p, C, zero => firstCellInsertedPoints(p, C)
  | p, C, succ(j) =>
      prependRealSequence(p[0],
        indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, j))

theorem indexedInsertedPoints.sequence_aux (k : Nat)
  shows ∀ p, ∀ C ∈ ℝ,
    RealSequence(p) → RealSequence(indexedInsertedPoints(p, C, k))
proof
  induction k
  | zero =>
    intros p C realC points
    rw indexedInsertedPoints
    exact firstCellInsertedPoints.sequence with points
  | succ(j) using ih =>
    intros p C realC points
    rw indexedInsertedPoints
    have pointZero := RealSequence.value with points
    have shifted := shiftedRealSequence.sequence at p, succ(0) with points
    have recursive := ih with shiftedRealSequence(p, succ(0)), C, realC, shifted
    exact prependRealSequence.sequence with recursive

theorem indexedInsertedPoints.sequence (p : Set) (C : Real, k : Nat)
  requires points : RealSequence(p)
  shows RealSequence(indexedInsertedPoints(p, C, k))
proof
  have realC : C ∈ ℝ
    have typedC : Real(C) by assumption
    exact typedC
  exact indexedInsertedPoints.sequence_aux at k with p, C, realC, points

theorem indexedInsertedPoints.zero (p : Set) (C : Real, k : Nat)
  requires points : RealSequence(p)
  shows indexedInsertedPoints(p, C, k)[0] = p[0]
proof
  induction k
  | zero =>
    rw indexedInsertedPoints
    exact firstCellInsertedPoints.zero with points
  | succ(j) using ih =>
    rw indexedInsertedPoints
    have pointZero := RealSequence.value with points
    have shifted := shiftedRealSequence.sequence at p, succ(0) with points
    have recursive := indexedInsertedPoints.sequence at
      shiftedRealSequence(p, succ(0)), C, j with shifted
    exact prependRealSequence.zero with recursive

theorem indexedInsertedPoints.successor (p : Set) (C : Real, k j : Nat)
  requires points : RealSequence(p)
  shows indexedInsertedPoints(p, C, succ(k))[succ(j)] =
    indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, k)[j]
proof
  rw indexedInsertedPoints
  have pointZero := RealSequence.value at p, 0 with points
  have shifted := shiftedRealSequence.sequence at p, succ(0) with points
  have recursive := indexedInsertedPoints.sequence at
    shiftedRealSequence(p, succ(0)), C, k with shifted
  exact prependRealSequence.succ with recursive

theorem indexedInsertedPoints.inserted (p : Set) (C : Real, k : Nat)
  requires points : RealSequence(p)
  shows indexedInsertedPoints(p, C, k)[succ(k)] = C
proof
  induction k generalizing p
  | zero =>
    intros p points
    rw indexedInsertedPoints
    exact firstCellInsertedPoints.one at p, C with points
  | succ(j) using ih =>
    intros p points
    have shifted := shiftedRealSequence.sequence at p, succ(0) with points
    have step := indexedInsertedPoints.successor at p, C, j, succ(j) with points
    have result := ih with shiftedRealSequence(p, succ(0)), shifted
    rwa result at step

theorem indexedInsertedPoints.after_inserted (p : Set) (C : Real, k : Nat)
  requires points : RealSequence(p)
  shows indexedInsertedPoints(p, C, k)[succ(succ(k))] = p[succ(k)]
proof
  induction k generalizing p
  | zero =>
    intros p points
    rw indexedInsertedPoints
    exact firstCellInsertedPoints.later with points
  | succ(j) using ih =>
    intros p points
    have shifted := shiftedRealSequence.sequence at p, succ(0) with points
    have step := indexedInsertedPoints.successor at p, C, j, succ(succ(j)) with points
    have result := ih with shiftedRealSequence(p, succ(0)), shifted
    rw result at step
    have value := shiftedRealSequence.value at p, succ(0), succ(j) with points
    rw value at step
    simp [add] at step
    exact step

-- PrependPartitions
theorem IntervalPartition.prepend (q : Set) (A X B : Real, N : Nat)
  requires tail : IntervalPartition(q, X, B, N)
  requires left : A < X
  shows IntervalPartition(prependRealSequence(A, q), A, B, succ(N))
proof
  rcases tail with ⟨points, start, finish, increasing⟩
  have prepended := prependRealSequence.sequence at A, q with points
  constructor
  . exact prepended
  . constructor
    . exact prependRealSequence.zero at A, q with points
    . constructor
      . have endPoint := prependRealSequence.succ at A, q, N with points
        rwa endPoint
      . intros i naturalI before
        have typedI := nat.omega.backward with naturalI
        have shape := natural.zero_or_successor with typedI
        cases shape with zero | successor
        . rw [zero, prependRealSequence.zero, prependRealSequence.succ, start]
          exact left
        . obtain ⟨j, naturalJ, isNext⟩ := successor
          rw isNext at before
          have beforeTail : Less(j, N)
            have shifted : Less(add(j, 1), add(N, 1)) by rwa [add.right_one, add.right_one]
            exact Less.add_right_cancel with shifted
          have old := increasing with j, nat.omega.forward at j with naturalJ, beforeTail
          rwa [isNext, prependRealSequence.succ, prependRealSequence.succ]

theorem FinePartition.prepend (q : Set) (A X B D : Real, N : Nat)
  requires tail : FinePartition(q, X, B, N, D)
  requires left : A < X
  requires width : X - A < D
  shows FinePartition(prependRealSequence(A, q), A, B, succ(N), D)
proof
  rcases tail with ⟨partition, positive, widths⟩
  have points : RealSequence(q)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have start : q[0] = X
    rcases partition with ⟨points, start, finish, increasing⟩
    exact start
  have prepended := IntervalPartition.prepend with partition, left
  constructor
  . exact prepended
  . constructor
    . exact positive
    . intros i naturalI before
      have typedI := nat.omega.backward with naturalI
      have shape := natural.zero_or_successor with typedI
      cases shape with zero | successor
      . rw [zero, prependRealSequence.zero, prependRealSequence.succ, start]
        exact width
      . obtain ⟨j, naturalJ, isNext⟩ := successor
        rw isNext at before
        have beforeTail : Less(j, N)
          have shifted : Less(add(j, 1), add(N, 1)) by rwa [add.right_one, add.right_one]
          exact Less.add_right_cancel with shifted
        have old := widths with j, nat.omega.forward at j with naturalJ, beforeTail
        rwa [isNext, prependRealSequence.succ, prependRealSequence.succ]

-- IndexedPartition
theorem natural.zero_before_successor (K : Nat)
  shows Less(0, succ(K))
proof
  unfold Less
  have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at K with assumption
  have shifted := LessEqual.add_monotone_right at 0, K, 1 with zeroLe
  simp [add.right_one, add] at shifted
  exact shifted

theorem FinePartition.insert_indexed (p : Set) (A B C D : Real, k L : Nat)
  requires fine : FinePartition(p, A, B, succ(add(k, L)), D)
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows FinePartition(indexedInsertedPoints(p, C, k), A, B,
    succ(succ(add(k, L))), D)
proof
  induction k generalizing p A
  | zero =>
    intros p A realA fine left right
    have start : p[0] = A
      rcases fine with ⟨partition, positive, widths⟩
      rcases partition with ⟨points, start, finish, increasing⟩
      exact start
    rw start at left
    rw indexedInsertedPoints
    rw add.left_unit at fine
    rw add.left_unit
    exact FinePartition.insert_first_cell at p, A, B, C, D, L with fine, left, right
  | succ(j) using ih =>
    intros p A realA fine left right
    have points : RealSequence(p)
      rcases fine with ⟨partition, positive, widths⟩
      rcases partition with ⟨points, start, finish, increasing⟩
      exact points
    have start : p[0] = A
      rcases fine with ⟨partition, positive, widths⟩
      rcases partition with ⟨points, start, finish, increasing⟩
      exact start
    have before : Less(0, succ(add(succ(j), L)))
      apply natural.zero_before_successor
    have first : (p[0]:R) < (p[succ(0)]:R)
      rcases fine with ⟨partition, positive, widths⟩
      rcases partition with ⟨points, start, finish, increasing⟩
      exact increasing with 0, nat.omega.forward at 0 with Naturals.constructor.zero, before
    have original : FinePartition(p, A, B, add(succ(0), succ(add(j, L))), D)
      rw [add, add]
      rwa add at fine
    have suffix := FinePartition.suffix with original
    have leftValue := shiftedRealSequence.value at p, succ(0), j with points
    have rightValue := shiftedRealSequence.value at p, succ(0), succ(j) with points
    simp [add] at leftValue
    simp [add] at rightValue
    rw <- leftValue at left
    rw <- rightValue at right
    have pointOne := RealSequence.value at p, succ(0) with points
    have inserted := ih with shiftedRealSequence(p, succ(0)), p[succ(0)], pointOne, suffix, left, right
    have firstWidth : (p[succ(0)]:R) - A < D
      rcases fine with ⟨partition, positive, widths⟩
      have width := widths with 0, nat.omega.forward at 0 with Naturals.constructor.zero, before
      rwa start at width
    rw start at first
    have prepended := FinePartition.prepend with inserted, first, firstWidth
    rwa [indexedInsertedPoints, start, add]

theorem FinePartition.insert_indexed_tagged (p : Set) (A B C D : Real, k L : Nat)
  requires fine : FinePartition(p, A, B, succ(add(k, L)), D)
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows TaggedPartition(indexedInsertedPoints(p, C, k),
      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, B,
      succ(succ(add(k, L)))) ∧
    FinePartition(indexedInsertedPoints(p, C, k), A, B,
      succ(succ(add(k, L))), D)
proof
  have inserted := FinePartition.insert_indexed with fine, left, right
  have partition : IntervalPartition(indexedInsertedPoints(p, C, k), A, B,
      succ(succ(add(k, L))))
    rcases inserted with ⟨partition, positive, widths⟩
    exact partition
  have tagged := IntervalPartition.left_tagged with partition
  refine ⟨tagged, inserted⟩

-- User-facing form: an index below the number of cells, with no
-- decomposition of the remaining cell count in the statement.
theorem FinePartition.insert_at (p : Set) (A B C D : Real, N k : Nat)
  requires fine : FinePartition(p, A, B, N, D)
  requires index : Less(k, N)
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows FinePartition(indexedInsertedPoints(p, C, k), A, B, succ(N), D)
proof
  obtain ⟨L, naturalL, length⟩ := index
  rw [<- length, add] at fine
  have inserted := FinePartition.insert_indexed with fine, left, right
  rwa [<- length, add]

theorem FinePartition.insert_at_tagged (p : Set) (A B C D : Real, N k : Nat)
  requires fine : FinePartition(p, A, B, N, D)
  requires index : Less(k, N)
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows TaggedPartition(indexedInsertedPoints(p, C, k),
      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, B, succ(N)) ∧
    FinePartition(indexedInsertedPoints(p, C, k), A, B, succ(N), D)
proof
  have inserted := FinePartition.insert_at with fine, index, left, right
  have partition : IntervalPartition(indexedInsertedPoints(p, C, k), A, B, succ(N))
    rcases inserted with ⟨partition, positive, widths⟩
    exact partition
  have tagged := IntervalPartition.left_tagged with partition
  refine ⟨tagged, inserted⟩

-- IndexedInsertionSplit
theorem FinePartition.insert_indexed_split (f p : Set) (A B C D : Real, k L : Nat)
  requires function : f : ℝ → ℝ
  requires fine : FinePartition(p, A, B, succ(add(k, L)), D)
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows FinePartition(indexedInsertedPoints(p, C, k), A, C, succ(k), D) ∧
    FinePartition(shiftedRealSequence(indexedInsertedPoints(p, C, k), succ(k)),
      C, B, succ(L), D) ∧
    TaggedPartition(indexedInsertedPoints(p, C, k),
      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, C, succ(k)) ∧
    TaggedPartition(shiftedRealSequence(indexedInsertedPoints(p, C, k), succ(k)),
      shiftedRealSequence(leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(k)),
      C, B, succ(L)) ∧
    riemannSum(f, indexedInsertedPoints(p, C, k),
      leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(succ(add(k, L)))) =
      (riemannSum(f, indexedInsertedPoints(p, C, k),
        leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(k)):R) +
      (riemannSum(f,
        shiftedRealSequence(indexedInsertedPoints(p, C, k), succ(k)),
        shiftedRealSequence(leftPartitionTags(indexedInsertedPoints(p, C, k)), succ(k)),
        succ(L)):R)
proof
  obtain ⟨tagged, finer⟩ := FinePartition.insert_indexed_tagged with fine, left, right
  have points : RealSequence(p)
    rcases fine with ⟨partition, positive, widths⟩
    rcases partition with ⟨sequence, start, finish, increasing⟩
    exact sequence
  have point := indexedInsertedPoints.inserted at p, C, k with points
  have splitFine : FinePartition(indexedInsertedPoints(p, C, k), A, B,
      add(succ(k), succ(L)), D)
    rwa [add, add.succ_right]
  have splitTagged : TaggedPartition(indexedInsertedPoints(p, C, k),
      leftPartitionTags(indexedInsertedPoints(p, C, k)), A, B,
      add(succ(k), succ(L)))
    rwa [add, add.succ_right]
  have split := FinePartition.split_tagged_sum with function, splitFine, splitTagged
  rwa [point, add, add.succ_right] at split

-- Section: IndexedSharedTotal
theorem riemannSum.insert_first_cell_prefix (f p : Set) (C : Real)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  shows riemannSum(f, firstCellInsertedPoints(p, C),
      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0))) =
    f(p[0]) * (C - (p[0]:R)) +
      f(C) * ((p[succ(0)]:R) - C)
proof
  have A := RealSequence.value at p, 0 with points
  have B := RealSequence.value at p, succ(0) with points
  have inserted := firstCellInsertedPoints.sequence at p, C with points
  have leftTags : RealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)))
    unfold RealSequence
    exact leftPartitionTags.function with inserted
  have two := twoCellPoints.sequence at p[0], C, p[succ(0)] with A, assumption, B
  have cells : ∀ i ∈ ℕ, i < succ(succ(0)) → firstCellInsertedPoints(p, C)[i] = twoCellPoints(p[0], C, p[succ(0)])[i] ∧ firstCellInsertedPoints(p, C)[succ(i)] = twoCellPoints(p[0], C, p[succ(0)])[succ(i)] ∧ leftPartitionTags(firstCellInsertedPoints(p, C))[i] = twoCellPoints(p[0], C, p[succ(0)])[i]
    intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    have cases := Nat.lt_two_cases with typedI, before
    cases cases with first | second
    . rw [first, firstCellInsertedPoints.zero, firstCellInsertedPoints.one, twoCellPoints.zero, twoCellPoints.one, leftPartitionTags.value, firstCellInsertedPoints.zero]
      refine ⟨rfl, rfl, rfl⟩
    . rw [second, firstCellInsertedPoints.one, firstCellInsertedPoints.later, twoCellPoints.one, twoCellPoints.two, leftPartitionTags.value, firstCellInsertedPoints.one]
      refine ⟨rfl, rfl, rfl⟩
  have same := riemannSum.congr_cells with function, inserted, two, leftTags, two, cells
  have value := riemannSum.two_cell_left at f, p[0], C, p[succ(0)] with function
  rwa value at same

theorem riemannSum.insert_first_cell_tail (f p : Set) (C : Real, K : Nat)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  shows riemannSum(f,
      shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0))),
      shiftedRealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0))), K) =
    riemannSum(f, shiftedRealSequence(p, succ(0)),
      shiftedRealSequence(leftPartitionTags(p), succ(0)), K)
proof
  have inserted := firstCellInsertedPoints.sequence with points
  have insertedTags : RealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)))
    unfold RealSequence
    exact leftPartitionTags.function with inserted
  have originalTags : RealSequence(leftPartitionTags(p))
    unfold RealSequence
    exact leftPartitionTags.function with points
  have newPoints := shiftedRealSequence.sequence at
    firstCellInsertedPoints(p, C), succ(succ(0)) with inserted
  have oldPoints := shiftedRealSequence.sequence at p, succ(0) with points
  have newTags := shiftedRealSequence.sequence at
    leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)) with insertedTags
  have oldTags := shiftedRealSequence.sequence at leftPartitionTags(p), succ(0) with originalTags
  have atIndex : ∀ j ∈ ℕ,
      shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0)))[j] =
        shiftedRealSequence(p, succ(0))[j]
    intros j naturalJ
    have typedJ := nat.omega.backward with naturalJ
    have newValue := shiftedRealSequence.value at
      firstCellInsertedPoints(p, C), succ(succ(0)), j with inserted
    have oldValue := shiftedRealSequence.value at p, succ(0), j with points
    simp [add] at newValue
    simp [add] at oldValue
    have later := firstCellInsertedPoints.later at p, C, j with points
    rw later at newValue
    rw [newValue, oldValue]
    rfl
  have atTag : ∀ m ∈ ℕ,
      shiftedRealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)))[m] =
        shiftedRealSequence(leftPartitionTags(p), succ(0))[m]
    intros m naturalJ
    have newValue := shiftedRealSequence.value at
      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)), m with insertedTags
    have oldValue := shiftedRealSequence.value at leftPartitionTags(p), succ(0), m with originalTags
    simp [add] at newValue
    simp [add] at oldValue
    rw leftPartitionTags.value at newValue
    rw leftPartitionTags.value at oldValue
    have later := firstCellInsertedPoints.later at p, C, m with points
    rw later at newValue
    rw [newValue, oldValue]
    rfl
  have cells : ∀ i ∈ ℕ, i < K → shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0)))[i] = shiftedRealSequence(p, succ(0))[i] ∧ shiftedRealSequence(firstCellInsertedPoints(p, C), succ(succ(0)))[succ(i)] = shiftedRealSequence(p, succ(0))[succ(i)] ∧ shiftedRealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)))[i] = shiftedRealSequence(leftPartitionTags(p), succ(0))[i]
    intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    have next := Naturals.constructor.succ with typedI
    have naturalNext := nat.omega.forward with next
    have first := atIndex with i, naturalI
    have second := atIndex with succ(i), naturalNext
    have third := atTag with i, naturalI
    refine ⟨first, second, third⟩
  exact riemannSum.congr_cells with function, newPoints, oldPoints, newTags, oldTags, cells

theorem riemannSum.insert_first_cell_total (f p : Set) (C : Real, K : Nat)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  shows riemannSum(f, firstCellInsertedPoints(p, C),
      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(K))) =
    (f(p[0]) * (C - (p[0]:R)) +
      f(C) * ((p[succ(0)]:R) - C)) +
    riemannSum(f, shiftedRealSequence(p, succ(0)),
      shiftedRealSequence(leftPartitionTags(p), succ(0)), K)
proof
  have inserted := firstCellInsertedPoints.sequence with points
  have tags : RealSequence(leftPartitionTags(firstCellInsertedPoints(p, C)))
    unfold RealSequence
    exact leftPartitionTags.function with inserted
  have split := riemannSum.split_at at f, firstCellInsertedPoints(p, C),
    leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(0)), K with
      function, inserted, tags
  simp [add] at split
  have prefix := riemannSum.insert_first_cell_prefix with function, points
  have tail := riemannSum.insert_first_cell_tail with function, points
  rwa [prefix, tail] at split

-- PrependSum
theorem realPartialSum.prepend (A : Real, u : Set, N : Nat)
  requires sequence : RealSequence(u)
  shows realPartialSum(prependRealSequence(A, u), succ(N)) =
    A + realPartialSum(u, N)
proof
  induction N
  | zero =>
    rw [realPartialSum.succ, realPartialSum.zero, realPartialSum.zero, prependRealSequence.zero]
    ring
  | succ(k) using ih =>
    rw [realPartialSum.succ, prependRealSequence.succ, ih, realPartialSum.succ]
    have term := RealSequence.value with sequence
    ring

theorem realPartialSum.first_cell_inserted (f p : Set) (C : Real, K : Nat)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  shows realPartialSum(
      prependRealSequence(
        riemannSum(f, twoCellPoints(p[0], C, p[succ(0)]),
          twoCellPoints(p[0], C, p[succ(0)]), succ(succ(0))),
        shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0))),
      succ(K)) =
    riemannSum(f, firstCellInsertedPoints(p, C),
      leftPartitionTags(firstCellInsertedPoints(p, C)), succ(succ(K)))
proof
  have A := RealSequence.value at p, 0 with points
  have B := RealSequence.value at p, succ(0) with points
  have tags : RealSequence(leftPartitionTags(p))
    unfold RealSequence
    exact leftPartitionTags.function with points
  have terms : RealSequence(riemannTerms(f, p, leftPartitionTags(p)))
    unfold RealSequence
    exact riemannTerms.function with function, points, tags
  have suffixTerms := shiftedRealSequence.sequence at
    riemannTerms(f, p, leftPartitionTags(p)), succ(0) with terms
  have twoPoints := twoCellPoints.sequence at p[0], C, p[succ(0)] with A, assumption, B
  have prepended := realPartialSum.prepend at
    riemannSum(f, twoCellPoints(p[0], C, p[succ(0)]),
      twoCellPoints(p[0], C, p[succ(0)]), succ(succ(0))),
    shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0)), K with suffixTerms
  have shiftedP := shiftedRealSequence.sequence at p, succ(0) with points
  have shiftedT := shiftedRealSequence.sequence at leftPartitionTags(p), succ(0) with tags
  have shiftedRiemannTerms : RealSequence(riemannTerms(f,
      shiftedRealSequence(p, succ(0)), shiftedRealSequence(leftPartitionTags(p), succ(0))))
    unfold RealSequence
    exact riemannTerms.function with function, shiftedP, shiftedT
  have equal : ∀ j ∈ ℕ, j < K → shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0))[j] = riemannTerms(f, shiftedRealSequence(p, succ(0)), shiftedRealSequence(leftPartitionTags(p), succ(0)))[j]
    intros j naturalJ before
    have typedJ := nat.omega.backward with naturalJ
    have shifted := riemannTerms.shifted at f, p, leftPartitionTags(p), succ(0), j with
      function, points, tags
    rw shifted
    rfl
  have suffix := realPartialSum.eq_prefix with suffixTerms, shiftedRiemannTerms, equal
  rw suffix at prepended
  have suffixRiemann : realPartialSum(riemannTerms(f,
      shiftedRealSequence(p, succ(0)), shiftedRealSequence(leftPartitionTags(p), succ(0))), K) =
    riemannSum(f, shiftedRealSequence(p, succ(0)),
      shiftedRealSequence(leftPartitionTags(p), succ(0)), K)
    unfold riemannSum
    rfl
  rw suffixRiemann at prepended
  have global := riemannSum.insert_first_cell_total at f, p, C, K with function, points
  have local := riemannSum.two_cell_left at f, p[0], C, p[succ(0)] with function
  rw [local, <- global] at prepended
  rwa local

-- FirstCellSharedTotal
def firstCellSubdivisionTerms (f p : Set, C : Real) : Set :=
  prependRealSequence(
    riemannSum(f, twoCellPoints(p[0], C, p[succ(0)]),
      twoCellPoints(p[0], C, p[succ(0)]), succ(succ(0))),
    shiftedRealSequence(riemannTerms(f, p, leftPartitionTags(p)), succ(0)))

theorem CellwiseSubdivisionSums.first_cell_inserted (f p : Set) (A B C : Real, K : Nat)
  requires function : f : ℝ → ℝ
  requires partition : IntervalPartition(p, A, B, succ(K))
  requires left : (p[0]:R) < C
  requires right : C < (p[succ(0)]:R)
  shows CellwiseSubdivisionSums(f, p, firstCellSubdivisionTerms(f, p, C), succ(K))
proof
  rcases partition with ⟨points, start, finish, increasing⟩
  have pointA := RealSequence.value at p, 0 with points
  have pointB := RealSequence.value at p, succ(0) with points
  have original : IntervalPartition(p, A, B, succ(K)) by refine ⟨points, start, finish, increasing⟩
  have tags : RealSequence(leftPartitionTags(p))
    unfold RealSequence
    exact leftPartitionTags.function with points
  have terms : RealSequence(riemannTerms(f, p, leftPartitionTags(p)))
    unfold RealSequence
    exact riemannTerms.function with function, points, tags
  have tail := shiftedRealSequence.sequence at riemannTerms(f, p, leftPartitionTags(p)), succ(0) with terms
  have twoPoints := twoCellPoints.sequence at p[0], C, p[succ(0)] with pointA, assumption, pointB
  have uSequence : RealSequence(firstCellSubdivisionTerms(f, p, C))
    rw firstCellSubdivisionTerms
    exact prependRealSequence.sequence with tail
  constructor
  . exact uSequence
  . intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    have shape := natural.zero_or_successor with typedI
    cases shape with zero | successor
    . witness twoCellPoints(p[0], C, p[succ(0)])
      witness twoCellPoints(p[0], C, p[succ(0)])
      witness succ(succ(0))
      rw zero
      constructor
      . exact nat.omega.forward at succ(succ(0)) with
          Naturals.constructor.succ at succ(0) with
            Naturals.constructor.succ at 0 with Naturals.constructor.zero
      . constructor
        . exact twoCellPoints.tagged at p[0], C, p[succ(0)] with
            left, right
        . rw [firstCellSubdivisionTerms, prependRealSequence.zero]
          rfl
    . obtain ⟨j, naturalJ, isNext⟩ := successor
      have oldBefore : Less(succ(j), succ(K)) by rwa isNext at before
      have oldCell := IntervalPartition.cell with original, oldBefore
      have valueI := RealSequence.value at p, succ(j) with points
      have valueNext := RealSequence.value at p, succ(succ(j)) with points
      have le := realLess.implies_le with oldCell
      have tag := closedInterval.left_mem with valueI, valueNext, le
      witness oneCellPoints(p[succ(j)], p[succ(succ(j))])
      witness constantSequence(p[succ(j)])
      witness succ(0)
      constructor
      . exact nat.omega.forward at succ(0) with
          Naturals.constructor.succ at 0 with Naturals.constructor.zero
      . constructor
        . rw isNext
          exact oneCellPoints.tagged_at with oldCell, tag
        . rw [isNext, firstCellSubdivisionTerms, prependRealSequence.succ]
          have shifted := shiftedRealSequence.value at
            riemannTerms(f, p, leftPartitionTags(p)), succ(0), j with terms
          simp [add] at shifted
          rw shifted
          have term := riemannTerms.value at f, p, leftPartitionTags(p), succ(j) with
            function, points, tags
          rw [term, leftPartitionTags.value]
          have single := riemannSum.one_cell_tag at f,
            p[succ(j)], p[succ(succ(j))], p[succ(j)] with function
          rw single
          unfold realMulValue
          unfold call2
          rfl

theorem SharedSubdivisionTotal.first_cell_inserted (f p : Set) (A B C : Real, K : Nat)
  requires function : f : ℝ → ℝ
  requires partition : IntervalPartition(p, A, B, succ(K))
  requires left : (p[0]:R) < C
  requires right : C < (p[succ(0)]:R)
  shows SharedSubdivisionTotal(f, p, firstCellInsertedPoints(p, C),
    firstCellSubdivisionTerms(f, p, C),
    riemannTerms(f, firstCellInsertedPoints(p, C),
      leftPartitionTags(firstCellInsertedPoints(p, C))),
    succ(K), succ(succ(K)))
proof
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have start : p[0] = A
    rcases partition with ⟨points, start, finish, increasing⟩
    exact start
  have leftA : A < C by rwa start at left
  have inserted := IntervalPartition.insert_first_cell with partition, leftA, right
  have tagged := IntervalPartition.left_tagged with inserted
  have coarse := CellwiseSubdivisionSums.first_cell_inserted with function, partition, left, right
  have fine := TaggedPartition.trivial_subdivision with function, tagged
  have total := realPartialSum.first_cell_inserted at f, p, C, K with function, points
  constructor
  . exact coarse
  . constructor
    . exact fine
    . unfold firstCellSubdivisionTerms
      rw total
      unfold riemannSum
      rfl

-- SubdivisionTransport
theorem CellwiseSubdivisionSums.congr_points (f p q u : Set) (N : Nat)
  requires subdivided : CellwiseSubdivisionSums(f, p, u, N)
  requires cells : ∀ i ∈ ℕ, i < N → p[i] = q[i] ∧ p[succ(i)] = q[succ(i)]
  shows CellwiseSubdivisionSums(f, q, u, N)
proof
  rcases subdivided with ⟨sequenceU, data⟩
  constructor
  . exact sequenceU
  . intros i naturalI before
    obtain ⟨left, right⟩ := cells with i, naturalI, before
    obtain ⟨r, s, M, naturalM, tagged, value⟩ := data with i, naturalI, before
    witness r
    witness s
    witness M
    constructor
    . exact naturalM
    . constructor
      . rw [<- left, <- right]
        exact tagged
      . exact value

theorem SharedSubdivisionTotal.congr_right (f p q r u v : Set) (N M : Nat)
  requires shared : SharedSubdivisionTotal(f, p, q, u, v, N, M)
  requires cells : ∀ i ∈ ℕ, i < M → q[i] = r[i] ∧ q[succ(i)] = r[succ(i)]
  shows SharedSubdivisionTotal(f, p, r, u, v, N, M)
proof
  rcases shared with ⟨coarse, fine, total⟩
  have moved := CellwiseSubdivisionSums.congr_points with fine, cells
  refine ⟨coarse, moved, total⟩

-- PrependSubdivision
def initialCellSum (f p : Set) : Set :=
  riemannSum(f, oneCellPoints(p[0], p[succ(0)]),
    constantSequence(p[0]), succ(0))

theorem CellwiseSubdivisionSums.prepend_initial (f p u : Set) (N : Nat)
  requires function : f : ℝ → ℝ
  requires points : RealSequence(p)
  requires first : (p[0]:R) < (p[succ(0)]:R)
  requires tail : CellwiseSubdivisionSums(f, shiftedRealSequence(p, succ(0)), u, N)
  shows CellwiseSubdivisionSums(f, p,
    prependRealSequence(initialCellSum(f, p), u), succ(N))
proof
  rcases tail with ⟨sequenceU, data⟩
  have A := RealSequence.value at p, 0 with points
  have B := RealSequence.value at p, succ(0) with points
  have le := realLess.implies_le with first
  have tag := closedInterval.left_mem with A, B, le
  have single := oneCellPoints.tagged_at with first, tag
  have value : Real(initialCellSum(f, p))
    unfold initialCellSum
    have onePoints := oneCellPoints.sequence with A, B
    have oneTags := constantSequence.sequence with A
    exact riemannSum.real with function, onePoints, oneTags
  have prepended := prependRealSequence.sequence at initialCellSum(f, p), u with sequenceU
  constructor
  . exact prepended
  . intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    have shape := natural.zero_or_successor with typedI
    cases shape with zero | successor
    . witness oneCellPoints(p[0], p[succ(0)])
      witness constantSequence(p[0])
      witness succ(0)
      rw zero
      constructor
      . exact nat.omega.forward at succ(0) with
          Naturals.constructor.succ at 0 with Naturals.constructor.zero
      . constructor
        . exact single
        . rw [prependRealSequence.zero, initialCellSum]
          rfl
    . obtain ⟨j, naturalJ, isNext⟩ := successor
      have beforeTail : Less(j, N)
        have shifted : Less(add(j, 1), add(N, 1))
          rw [add.right_one, add.right_one]
          rwa isNext at before
        exact Less.add_right_cancel with shifted
      obtain ⟨r, s, M, naturalM, tagged, equal⟩ := data with
        j, nat.omega.forward at j with naturalJ, beforeTail
      witness r
      witness s
      witness M
      constructor
      . exact naturalM
      . constructor
        . rw isNext
          have shiftedLeft := shiftedRealSequence.value at p, succ(0), j with points
          have shiftedRight := shiftedRealSequence.value at p, succ(0), succ(j) with points
          simp [add] at shiftedLeft
          simp [add] at shiftedRight
          rwa [shiftedLeft, shiftedRight] at tagged
        . rw [isNext, prependRealSequence.succ]
          exact equal

-- PrependSharedTotal
theorem SharedSubdivisionTotal.prepend_initial (f p q u v : Set) (N M : Nat)
  requires function : f : ℝ → ℝ
  requires pointsP : RealSequence(p)
  requires pointsQ : RealSequence(q)
  requires first : (p[0]:R) < (p[succ(0)]:R)
  requires sameStart : p[0] = q[0]
  requires sameNext : p[succ(0)] = q[succ(0)]
  requires shared : SharedSubdivisionTotal(f,
    shiftedRealSequence(p, succ(0)), shiftedRealSequence(q, succ(0)),
    u, v, N, M)
  shows SharedSubdivisionTotal(f, p, q,
    prependRealSequence(initialCellSum(f, p), u),
    prependRealSequence(initialCellSum(f, q), v), succ(N), succ(M))
proof
  rcases shared with ⟨coarseTail, fineTail, equalTail⟩
  have coarse := CellwiseSubdivisionSums.prepend_initial with function, pointsP, first, coarseTail
  have firstQ : (q[0]:R) < (q[succ(0)]:R) by rwa [<- sameStart, <- sameNext]
  have fine := CellwiseSubdivisionSums.prepend_initial with function, pointsQ, firstQ, fineTail
  have sameInitial : initialCellSum(f, p) = initialCellSum(f, q)
    simp [initialCellSum]
  have sequenceU : RealSequence(u)
    rcases coarseTail with ⟨sequence, data⟩
    exact sequence
  have sequenceV : RealSequence(v)
    rcases fineTail with ⟨sequence, data⟩
    exact sequence
  have pointP := RealSequence.value at p, 0 with pointsP
  have pointNext := RealSequence.value at p, succ(0) with pointsP
  have onePoints := oneCellPoints.sequence with pointP, pointNext
  have oneTags := constantSequence.sequence with pointP
  have firstReal : Real(initialCellSum(f, p))
    unfold initialCellSum
    exact riemannSum.real with function, onePoints, oneTags
  have pointQ := RealSequence.value at q, 0 with pointsQ
  have pointQNext := RealSequence.value at q, succ(0) with pointsQ
  have qPoints := oneCellPoints.sequence with pointQ, pointQNext
  have qTags := constantSequence.sequence with pointQ
  have secondReal : Real(initialCellSum(f, q))
    unfold initialCellSum
    exact riemannSum.real with function, qPoints, qTags
  have sumP := realPartialSum.prepend at initialCellSum(f, p), u, N with sequenceU
  have sumQ := realPartialSum.prepend at initialCellSum(f, q), v, M with sequenceV
  have totals : realPartialSum(prependRealSequence(initialCellSum(f, p), u), succ(N)) =
      realPartialSum(prependRealSequence(initialCellSum(f, q), v), succ(M))
    rw [sumP, sumQ, sameInitial, equalTail]
    rfl
  refine ⟨coarse, fine, totals⟩

-- IndexedSharedTotal
theorem SharedSubdivisionTotal.exists_insert_indexed (f p : Set) (A B C : Real, k L : Nat)
  requires function : f : ℝ → ℝ
  requires partition : IntervalPartition(p, A, B, succ(add(k, L)))
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows ∃ u, ∃ v, SharedSubdivisionTotal(f, p,
    indexedInsertedPoints(p, C, k), u, v,
    succ(add(k, L)), succ(succ(add(k, L))))
proof
  induction k generalizing p A
  | zero =>
    intros p A realA partition left right
    have basePartition : IntervalPartition(p, A, B, succ(L)) by rwa add.left_unit at partition
    have base := SharedSubdivisionTotal.first_cell_inserted at f, p, A, B, C, L with
      function, basePartition, left, right
    witness firstCellSubdivisionTerms(f, p, C)
    witness riemannTerms(f, firstCellInsertedPoints(p, C),
      leftPartitionTags(firstCellInsertedPoints(p, C)))
    rwa [indexedInsertedPoints, add.left_unit]
  | succ(j) using ih =>
    intros p A realA partition left right
    have points : RealSequence(p)
      rcases partition with ⟨points, start, finish, increasing⟩
      exact points
    have totalNat : Nat(add(succ(j), L)) by apply add.closed at L, succ(j)
    have firstBefore := natural.zero_before_successor with totalNat
    have first := IntervalPartition.cell with partition, firstBefore
    have tailPartition : IntervalPartition(shiftedRealSequence(p, succ(0)),
        p[succ(0)], B, succ(add(j, L)))
      have original : IntervalPartition(p, A, B,
          add(succ(0), succ(add(j, L))))
        rw [add, add]
        rwa add at partition
      exact IntervalPartition.suffix with original
    have shifted := shiftedRealSequence.sequence at p, succ(0) with points
    have leftValue := shiftedRealSequence.value at p, succ(0), j with points
    have rightValue := shiftedRealSequence.value at p, succ(0), succ(j) with points
    simp [add] at leftValue
    simp [add] at rightValue
    rw <- leftValue at left
    rw <- rightValue at right
    have pointOne := RealSequence.value at p, succ(0) with points
    obtain ⟨u, v, tailShared⟩ := ih with
      shiftedRealSequence(p, succ(0)), p[succ(0)],
      pointOne,
      tailPartition, left, right
    have inserted := indexedInsertedPoints.sequence at p, C, succ(j) with points
    have insertedTail := indexedInsertedPoints.sequence at
      shiftedRealSequence(p, succ(0)), C, j with shifted
    have newShift := shiftedRealSequence.sequence at
      indexedInsertedPoints(p, C, succ(j)), succ(0) with inserted
    have tailCells : ∀ i ∈ ℕ, i < succ(succ(add(j, L))) → indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, j)[i] = shiftedRealSequence(indexedInsertedPoints(p, C, succ(j)), succ(0))[i] ∧ indexedInsertedPoints(shiftedRealSequence(p, succ(0)), C, j)[succ(i)] = shiftedRealSequence(indexedInsertedPoints(p, C, succ(j)), succ(0))[succ(i)]
      intros i naturalI before
      have typedI := nat.omega.backward with naturalI
      have next := Naturals.constructor.succ with typedI
      have naturalNext := nat.omega.forward with next
      have atI := indexedInsertedPoints.successor at p, C, j, i with points
      have shiftI := shiftedRealSequence.value at
        indexedInsertedPoints(p, C, succ(j)), succ(0), i with inserted
      simp [add] at shiftI
      rw shiftI
      have atNext := indexedInsertedPoints.successor at p, C, j, succ(i) with points
      have shiftNext := shiftedRealSequence.value at
        indexedInsertedPoints(p, C, succ(j)), succ(0), succ(i) with inserted
      simp [add] at shiftNext
      rw shiftNext
      refine ⟨rfl, rfl⟩
    have moved := SharedSubdivisionTotal.congr_right with tailShared, tailCells
    have sameStart := indexedInsertedPoints.zero at p, C, succ(j) with points
    have sameStartP : p[0] = indexedInsertedPoints(p, C, succ(j))[0]
      rw sameStart
      rfl
    have sameNext : p[succ(0)] = indexedInsertedPoints(p, C, succ(j))[succ(0)]
      have step := indexedInsertedPoints.successor at p, C, j, 0 with points
      have tailZero := indexedInsertedPoints.zero at
        shiftedRealSequence(p, succ(0)), C, j with shifted
      have shiftedZero := shiftedRealSequence.value at p, succ(0), 0 with points
      simp [add] at shiftedZero
      rw [tailZero, shiftedZero] at step
      rw step
      rfl
    have lifted := SharedSubdivisionTotal.prepend_initial with
      function, points, inserted, first, sameStartP, sameNext, moved
    witness prependRealSequence(initialCellSum(f, p), u)
    witness prependRealSequence(initialCellSum(f,
      indexedInsertedPoints(p, C, succ(j))), v)
    rwa add

theorem SharedSubdivisionTotal.exists_insert_at (f p : Set) (A B C : Real, N k : Nat)
  requires function : f : ℝ → ℝ
  requires partition : IntervalPartition(p, A, B, N)
  requires index : Less(k, N)
  requires left : (p[k]:R) < C
  requires right : C < (p[succ(k)]:R)
  shows ∃ u, ∃ v, SharedSubdivisionTotal(f, p,
    indexedInsertedPoints(p, C, k), u, v, N, succ(N))
proof
  obtain ⟨L, naturalL, length⟩ := index
  rw [<- length, add] at partition
  obtain ⟨u, v, shared⟩ := SharedSubdivisionTotal.exists_insert_indexed with function, partition, left, right
  witness u
  witness v
  rwa [<- length, add]

-- Section: CommonVertices
theorem IntervalPartition.locate_interior (p : Set) (A B C : Real, N : Nat)
  requires partition : IntervalPartition(p, A, B, N)
  requires above : A < C
  requires below : C < B
  shows (∃ i ∈ ℕ, i ≤ N ∧ p[i] = C) ∨
    (∃ k ∈ ℕ, k < N ∧ (p[k]:R) < C ∧ C < (p[succ(k)]:R))
proof
  induction N generalizing p A
  | zero =>
    intros p A realA partition above
    have start : p[0] = A
      rcases partition with ⟨points, start, finish, increasing⟩
      exact start
    have finish : p[0] = B
      rcases partition with ⟨points, start, finish, increasing⟩
      exact finish
    rw [<- finish, start] at below
    have impossible := realLess.transitive with above, below
    have contradiction := realLess.characterization.forward with impossible
    have irreflexive := RealLess.irreflexive with contradiction
    exfalso
    exact irreflexive
  | succ(K) using ih =>
    intros p A realA partition above
    have points : RealSequence(p)
      rcases partition with ⟨points, start, finish, increasing⟩
      exact points
    have start : p[0] = A
      rcases partition with ⟨points, start, finish, increasing⟩
      exact start
    have pointOne := RealSequence.value at p, succ(0) with points
    have alternatives : C = p[succ(0)] ∨ C ≠ p[succ(0)] by tauto
    cases alternatives with equal | distinct
    . left
      witness succ(0)
      constructor
      . exact nat.omega.forward at succ(0) with
          Naturals.constructor.succ at 0 with Naturals.constructor.zero
      . constructor
        . have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at K
          have shifted := LessEqual.add_monotone_right at 0, K, 1 with zeroLe
          rwa [add.right_one, add.right_one] at shifted
        . rw equal
          rfl
    have comparison := realLess.connected_on with C, p[succ(0)], distinct
    cases comparison with beforeFirst | afterFirst
    . right
      witness 0
      constructor
      . exact nat.omega.forward at 0 with Naturals.constructor.zero
      . constructor
        . exact natural.zero_before_successor at K
        . constructor
          . rw start
            exact above
          . exact beforeFirst
    . have tail : IntervalPartition(shiftedRealSequence(p, succ(0)),
          p[succ(0)], B, K)
        have length : IntervalPartition(p, A, B, add(succ(0), K)) by rwa [add, add.left_unit]
        exact IntervalPartition.suffix with length
    have tailPoint := ih with shiftedRealSequence(p, succ(0)),
      p[succ(0)], pointOne, tail, afterFirst
    cases tailPoint with atVertex | inCell
    . obtain ⟨i, naturalI, bound, value⟩ := atVertex
      left
      witness succ(i)
      constructor
      . exact nat.omega.forward at succ(i) with
          Naturals.constructor.succ at i with nat.omega.backward at i with naturalI
      . constructor
        . have lifted := LessEqual.add_monotone_right at i, K, 1 with bound
          rwa [add.right_one, add.right_one] at lifted
          . have shifted := shiftedRealSequence.value at p, succ(0), i with points
            simp [add] at shifted
            rw <- shifted
            rfl
    . obtain ⟨m, naturalI, bound, left, right⟩ := inCell
      right
      witness succ(m)
      constructor
      . exact nat.omega.forward at succ(m) with
          Naturals.constructor.succ at m with nat.omega.backward at m with naturalI
      . constructor
        . have lifted := Less.add_LessEqual at m, K, 1, 1 with
            bound, LessEqual.reflexive at 1 with
              Naturals.constructor.succ at 0 with Naturals.constructor.zero
          rwa [add.right_one, add.right_one] at lifted
        . have shiftedLeft := shiftedRealSequence.value at p, succ(0), m with points
          have shiftedRight := shiftedRealSequence.value at p, succ(0), succ(m) with points
          simp [add] at shiftedLeft
          simp [add] at shiftedRight
          rw shiftedLeft at left
          rw shiftedRight at right
          refine ⟨left, right⟩

-- IndexedInsertionVertices
theorem indexedInsertedPoints.before (p : Set) (C : Real, k i : Nat)
  requires points : RealSequence(p)
  requires bounded : i ≤ k
  shows indexedInsertedPoints(p, C, k)[i] = p[i]
proof
  induction k generalizing p i
  | zero =>
    intros p i naturalI points bounded
    have zeroLe := Grace.Core.Nat.Order.LessEqual.zero at i
    have iZero := LessEqual.antisymmetric with bounded, zeroLe
    rw [iZero, indexedInsertedPoints]
    exact firstCellInsertedPoints.zero at p, C with points
  | succ(j) using ih =>
    intros p i naturalI points bounded
    have shape := natural.zero_or_successor at i
    cases shape with zero | successor
    . rw zero
      exact indexedInsertedPoints.zero with points
    . obtain ⟨m, naturalM, isNext⟩ := successor
      have before : m ≤ j
        have shifted : add(m, 1) ≤ add(j, 1)
          rw [add.right_one, add.right_one]
          rwa isNext at bounded
        exact LessEqual.add_right_cancel with shifted
      have tail := shiftedRealSequence.sequence at p, succ(0) with points
      have result := ih with shiftedRealSequence(p, succ(0)), m, naturalM, tail, before
      have step := indexedInsertedPoints.successor at p, C, j, m with points
      have value := shiftedRealSequence.value at p, succ(0), m with points
      simp [add] at value
      rw [result, value] at step
      rwa isNext

theorem indexedInsertedPoints.after (p : Set) (C : Real, k j : Nat)
  requires points : RealSequence(p)
  shows indexedInsertedPoints(p, C, k)[succ(succ(add(k, j)))] =
    p[succ(add(k, j))]
proof
  induction k generalizing p
  | zero =>
    intros p points
    rw [add.left_unit, indexedInsertedPoints]
    exact firstCellInsertedPoints.later with points
  | succ(m) using ih =>
    intros p points
    have shifted := shiftedRealSequence.sequence at p, succ(0) with points
    have step := indexedInsertedPoints.successor at p, C, m,
      succ(succ(add(m, j))) with points
    have result := ih with shiftedRealSequence(p, succ(0)), shifted
    rw result at step
    have value := shiftedRealSequence.value at p, succ(0), succ(add(m, j)) with points
    simp [add] at value
    rw value at step
    rwa add

theorem indexedInsertedPoints.preserves_vertex (p : Set) (C : Real, N k i : Nat)
  requires points : RealSequence(p)
  requires index : k < N
  requires vertex : i ≤ N
  shows ∃ j ∈ ℕ, j ≤ succ(N) ∧ indexedInsertedPoints(p, C, k)[j] = p[i]
proof
  have cases := Less.trichotomy at i, k with *
  cases cases with before | rest
  . have bounded := Less.implies_LessEqual at i, k with before
    have value := indexedInsertedPoints.before with points, bounded
    have kLeN := Less.implies_LessEqual at k, N with *
    have iLeN := LessEqual.transitive with bounded, kLeN
    have iLeNext := LessEqual.transitive at i, N, succ(N) with
      *{2}, Naturals.constructor.succ at N with assumption,
      iLeN, LessEqual.successor at N with assumption
    witness i
    refine ⟨nat.omega.forward at i with assumption, iLeNext, value⟩
  cases rest with equal | after
  . have bounded : i ≤ k
      rw equal
      exact LessEqual.reflexive with assumption
  have value := indexedInsertedPoints.before with points, bounded
  have kLeN := Less.implies_LessEqual at k, N with *
  have iLeN := LessEqual.transitive with bounded, kLeN
  have iLeNext := LessEqual.transitive at i, N, succ(N) with
    *{2}, Naturals.constructor.succ at N with assumption,
    iLeN, LessEqual.successor at N with assumption
  witness i
  refine ⟨nat.omega.forward at i with assumption, iLeNext, value⟩
    obtain ⟨L, naturalL, length⟩ := after
    have original : i = succ(add(k, L))
      rw [<- length, add]
      rfl
    have shifted := indexedInsertedPoints.after at p, C, k, L with points
    rw <- original at shifted
    have nextI := Naturals.constructor.succ at i
    have lifted := LessEqual.add_monotone_right at i, N, 1 with vertex
    rw [add.right_one, add.right_one] at lifted
    witness succ(i)
    refine ⟨nat.omega.forward at succ(i) with nextI, lifted, shifted⟩

-- PartitionVertices
theorem IntervalPartition.strict_indices (p : Set) (A B : Real, N i j : Nat)
  requires partition : IntervalPartition(p, A, B, N)
  requires before : i < j
  requires bounded : j ≤ N
  shows (p[i]:R) < (p[j]:R)
proof
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, steps⟩
    exact points
  have iBefore : i < N by exact Less.transitive_LessEqual at i, j, N with before, bounded
  have step := IntervalPartition.cell with partition, iBefore
  have prefix : ∀ k ∈ ℕ, k < j → (p[k]:R) < (p[succ(k)]:R)
    intros k naturalK below
    have typedK := nat.omega.backward with naturalK
    have valid := Less.transitive_LessEqual with below, bounded
    exact IntervalPartition.cell with partition, valid
  have monotone := IntervalPartition.prefix_mono with points, prefix
  have successorLe : succ(i) ≤ j by exact before
  have nextNatural := Naturals.constructor.succ at i
  have weak := monotone with succ(i), nat.omega.forward at succ(i) with nextNatural, successorLe
  have first := RealSequence.value at p, i with points
  have second := RealSequence.value at p, succ(i) with points
  have last := RealSequence.value at p, j with points
  exact realLess.transitive_le with first, second, last, step, weak

theorem IntervalPartition.vertex_index_unique (p : Set) (A B : Real, N i j : Nat)
  requires partition : IntervalPartition(p, A, B, N)
  requires boundedI : i ≤ N
  requires boundedJ : j ≤ N
  requires same : p[i] = p[j]
  shows i = j
proof
  have alternatives := Less.trichotomy at i, j with *
  cases alternatives with before | rest
  . have strict := IntervalPartition.strict_indices at p, A, B, N, i, j with
      partition, before, boundedJ
    rw same at strict
    have contradiction := realLess.characterization.forward with strict
    exfalso
    exact RealLess.irreflexive with contradiction
  cases rest with equal | after
  . exact equal
  . have strict := IntervalPartition.strict_indices at p, A, B, N, j, i with
      partition, after, boundedI
    rw <- same at strict
    have contradiction := realLess.characterization.forward with strict
    exfalso
    exact RealLess.irreflexive with contradiction

-- VertexContainment
predicate VerticesContained (p q : Set) (N M : Nat) :=
  ∀ i ∈ ℕ, i ≤ N → ∃ j ∈ ℕ, j ≤ M ∧ q[j] = p[i]

theorem VerticesContained.reflexive (p : Set) (N : Nat)
  shows VerticesContained(p, p, N, N)
proof
  intros i naturalI bounded
  witness i
  refine ⟨naturalI, bounded, rfl⟩

theorem VerticesContained.transitive (p q r : Set) (N M L : Nat)
  requires first : VerticesContained(p, q, N, M)
  requires second : VerticesContained(q, r, M, L)
  shows VerticesContained(p, r, N, L)
proof
  intros i naturalI bounded
  obtain ⟨j, naturalJ, jBound, equalP⟩ := first with i, naturalI, bounded
  obtain ⟨k, naturalK, kBound, equalQ⟩ := second with j, naturalJ, jBound
  witness k
  constructor
  . exact naturalK
  . constructor
    . exact kBound
    . rw equalQ
      exact equalP

theorem VerticesContained.insert_at (p : Set) (C : Real, N k : Nat)
  requires points : RealSequence(p)
  requires before : k < N
  shows VerticesContained(p, indexedInsertedPoints(p, C, k), N, succ(N))
proof
  intros i naturalI bounded
  have typedI := nat.omega.backward with naturalI
  exact indexedInsertedPoints.preserves_vertex with points, before, bounded

-- InsertOrHit
theorem FinePartition.insert_or_hit (f p : Set) (A B C D : Real, N : Nat)
  requires function : f : ℝ → ℝ
  requires fine : FinePartition(p, A, B, N, D)
  requires above : A < C
  requires below : C < B
  shows ∃ q, ∃ M ∈ ℕ, ∃ u, ∃ v,
    FinePartition(q, A, B, M, D) ∧
    TaggedPartition(q, leftPartitionTags(q), A, B, M) ∧
    SharedSubdivisionTotal(f, p, q, u, v, N, M) ∧
    VerticesContained(p, q, N, M) ∧
    (∃ i ∈ ℕ, i ≤ M ∧ q[i] = C)
proof
  have partition : IntervalPartition(p, A, B, N)
    rcases fine with ⟨partition, positive, widths⟩
    exact partition
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, increasing⟩
    exact points
  have location := IntervalPartition.locate_interior with partition, above, below
  cases location with existing | inside
  . obtain ⟨i, naturalI, bounded, value⟩ := existing
    have tagged := IntervalPartition.left_tagged with partition
    have subdivided := TaggedPartition.trivial_subdivision with function, tagged
    have shared : SharedSubdivisionTotal(f, p, p,
        riemannTerms(f, p, leftPartitionTags(p)),
        riemannTerms(f, p, leftPartitionTags(p)), N, N)
      refine ⟨subdivided, subdivided, rfl⟩
    witness p
    witness N
    constructor
    . exact nat.omega.forward at N with assumption
    . witness riemannTerms(f, p, leftPartitionTags(p))
      witness riemannTerms(f, p, leftPartitionTags(p))
      have preserved := VerticesContained.reflexive at p, N
      refine ⟨fine, tagged, shared, preserved, i, naturalI, bounded, value⟩
  . obtain ⟨k, naturalK, before, left, right⟩ := inside
    obtain ⟨tagged, finer⟩ := FinePartition.insert_at_tagged with fine, before, left, right
    obtain ⟨u, v, shared⟩ := SharedSubdivisionTotal.exists_insert_at with
      function, partition, before, left, right
    have point := indexedInsertedPoints.inserted at p, C, k with points
    have preserved := VerticesContained.insert_at at p, C, N, k with points, before
    have nextK := Naturals.constructor.succ at k
    have nextN := Naturals.constructor.succ at N
    have boundK : succ(k) ≤ N by exact before
    have boundInserted := LessEqual.transitive at succ(k), N, succ(N) with
      nextK, assumption, nextN, boundK, LessEqual.successor at N with assumption
    witness indexedInsertedPoints(p, C, k)
    witness succ(N)
    constructor
    . exact nat.omega.forward at succ(N) with nextN
    . witness u
      witness v
      refine ⟨finer, tagged, shared, preserved, succ(k),
        nat.omega.forward at succ(k) with nextK, boundInserted, point⟩

-- CommonVertices
predicate PrefixVerticesContained (q r : Set) (m L : Nat) :=
  ∀ i ∈ ℕ, i ≤ m → ∃ j ∈ ℕ, j ≤ L ∧ r[j] = q[i]

theorem PrefixVerticesContained.transitive (q r s : Set) (m L H : Nat)
  requires prefix : PrefixVerticesContained(q, r, m, L)
  requires preserved : VerticesContained(r, s, L, H)
  shows PrefixVerticesContained(q, s, m, H)
proof
  intros i naturalI bounded
  obtain ⟨j, naturalJ, boundJ, equalQ⟩ := prefix with i, naturalI, bounded
  obtain ⟨h, naturalH, boundH, equalR⟩ := preserved with j, naturalJ, boundJ
  witness h
  constructor
  . exact naturalH
  . constructor
    . exact boundH
    . rw equalR
      exact equalQ

theorem FinePartition.collect_vertices (f p q : Set) (A B D : Real, N M m : Nat)
  requires function : f : ℝ → ℝ
  requires fine : FinePartition(p, A, B, N, D)
  requires source : IntervalPartition(q, A, B, M)
  shows m ≤ M → ∃ r, ∃ L ∈ ℕ,
    FinePartition(r, A, B, L, D) ∧
    VerticesContained(p, r, N, L) ∧
    PrefixVerticesContained(q, r, m, L)
proof
  induction m
  | zero =>
    intro prefix
    have partitionP : IntervalPartition(p, A, B, N)
      rcases fine with ⟨partition, positive, widths⟩
      exact partition
    have startP : p[0] = A
      rcases partitionP with ⟨points, start, finish, increasing⟩
      exact start
    have startQ : q[0] = A
      rcases source with ⟨points, start, finish, increasing⟩
      exact start
    have prefixZero : PrefixVerticesContained(q, p, 0, N)
      intros i naturalI bounded
      have typedI := nat.omega.backward with naturalI
      have zeroLe := Grace.Core.Nat.Order.LessEqual.zero with typedI
      have equal := LessEqual.antisymmetric with bounded, zeroLe
      witness 0
      rw equal
      constructor
      . exact nat.omega.forward at 0 with Naturals.constructor.zero
      . constructor
        . exact Grace.Core.Nat.Order.LessEqual.zero at N
        . rw [startP, startQ]
          rfl
    witness p
    witness N
    constructor
    . exact nat.omega.forward at N with assumption
    . have preserved := VerticesContained.reflexive at p, N
      refine ⟨fine, preserved, prefixZero⟩
  | succ(k) using ih =>
    intro prefix
    have kBound := LessEqual.transitive at k, succ(k), M with
      LessEqual.successor at k with assumption, prefix
    obtain ⟨r, L, naturalL, fineR, original, processed⟩ := ih with kBound
    have partitionR : IntervalPartition(r, A, B, L)
      rcases fineR with ⟨partition, positive, widths⟩
      exact partition
    have alternatives := Less.trichotomy at succ(k), M with
      Naturals.constructor.succ at k with *{2}
    cases alternatives with interior | rest
    . have zeroBefore := natural.zero_before_successor at k
      have sourceStart := IntervalPartition.strict_indices with source, zeroBefore, prefix
      have sourceEnd := IntervalPartition.strict_indices at q, A, B, M,
        succ(k), M with source, interior, LessEqual.reflexive at M with assumption
      have startQ : q[0] = A
        rcases source with ⟨points, start, finish, increasing⟩
        exact start
      have endQ : q[M] = B
        rcases source with ⟨points, start, finish, increasing⟩
        exact finish
      rw startQ at sourceStart
      rw endQ at sourceEnd
      have sourcePoints : RealSequence(q)
        rcases source with ⟨points, start, finish, increasing⟩
        exact points
      have sourceValue := RealSequence.value at q, succ(k) with sourcePoints
      obtain ⟨s, H, naturalH, u, v, fineS, taggedS, shared, preserved, newPoint⟩ :=
        FinePartition.insert_or_hit at f, r, A, B, q[succ(k)], D, L with
          sourceValue, function, fineR, sourceStart, sourceEnd
      have oldVertices := VerticesContained.transitive with original, preserved
      have oldPrefix := PrefixVerticesContained.transitive with processed, preserved
      have nextPrefix : PrefixVerticesContained(q, s, succ(k), H)
        intros i naturalI bounded
        have typedI := nat.omega.backward with naturalI
        have cases := nat.le_succ_cases with bounded
        cases cases with earlier | last
          exact oldPrefix with i, naturalI, earlier
        . obtain ⟨j, naturalJ, boundedJ, valueJ⟩ := newPoint
          witness j
          constructor
          . exact naturalJ
          . constructor
            . exact boundedJ
            . rw last
              exact valueJ
      witness s
      witness H
      refine ⟨naturalH, fineS, oldVertices, nextPrefix⟩
    . cases rest with endpoint | impossible
      . have endQ : q[M] = B
          rcases source with ⟨points, start, finish, increasing⟩
          exact finish
      have endR : r[L] = B
        rcases partitionR with ⟨points, start, finish, increasing⟩
        exact finish
      have nextPrefix : PrefixVerticesContained(q, r, succ(k), L)
        intros i naturalI bounded
        have typedI := nat.omega.backward with naturalI
        have cases := nat.le_succ_cases with bounded
        cases cases with earlier | last
          exact processed with i, naturalI, earlier
        . witness L
          rw last
          constructor
          . exact naturalL
          . constructor
            . exact LessEqual.reflexive at L
            . rw [endpoint, endQ]
              exact endR
      witness r
      witness L
      refine ⟨naturalL, fineR, original, nextPrefix⟩
      . have weak := Less.implies_LessEqual at M, succ(k) with impossible
        have equal := LessEqual.antisymmetric with prefix, weak
        exfalso
        have contradiction := Less.irreflexive at M
        apply contradiction
        rwa equal at impossible

theorem FinePartition.common_vertices (f p q : Set) (A B D : Real, N M : Nat)
  requires function : f : ℝ → ℝ
  requires fineP : FinePartition(p, A, B, N, D)
  requires fineQ : FinePartition(q, A, B, M, D)
  shows ∃ r, ∃ L ∈ ℕ,
    FinePartition(r, A, B, L, D) ∧
    VerticesContained(p, r, N, L) ∧
    VerticesContained(q, r, M, L)
proof
  have partitionQ : IntervalPartition(q, A, B, M)
    rcases fineQ with ⟨partition, positive, widths⟩
    exact partition
  obtain ⟨r, L, naturalL, fineR, old, new⟩ :=
    FinePartition.collect_vertices at f, p, q, A, B, D, N, M, M with
      function, fineP, partitionQ, LessEqual.reflexive at M with assumption
  witness r
  witness L
  have contained : VerticesContained(q, r, M, L)
    unfold VerticesContained
    exact new
  refine ⟨naturalL, fineR, old, contained⟩

-- Section: ArbitrarySharedTotal
def refinementIndex.candidates (p r : Set, N M i : Nat) : Set :=
  {j ∈ ℕ | (i ≤ N → j ≤ M ∧ r[j] = p[i]) ∧ (¬(i ≤ N) → j = 0)}

def refinementIndex (p r : Set, N M i : Nat) : Set :=
  leastNatural(refinementIndex.candidates(p, r, N, M, i))

theorem refinementIndex.exists (p r : Set, N M i : Nat)
requires contained : VerticesContained(p, r, N, M)
shows ∃ j ∈ ℕ, (i ≤ N → j ≤ M ∧ r[j] = p[i]) ∧ (¬(i ≤ N) → j = 0)
proof
  have alternatives : i ≤ N ∨ ¬(i ≤ N) by tauto
  cases alternatives with bounded | beyond
    obtain ⟨j, naturalJ, jBound, value⟩ := contained with i,
      nat.omega.forward at i with assumption, bounded
    witness j
    constructor
    . exact naturalJ
    . constructor
      . intro again
        refine ⟨jBound, value⟩
      . intro impossible
        exfalso
        exact impossible with bounded
  . witness 0
    constructor
    . exact nat.omega.forward at 0 with Naturals.constructor.zero
    . constructor
      . intro bounded
        exfalso
        exact beyond with bounded
      . intro ignored
        rfl

-- Repeated vertices may give several valid indices. Selecting the least one
-- makes the existing interface deterministic without strengthening its guards.
theorem refinementIndex.selected (p r : Set, N M i : Nat)
  requires contained : VerticesContained(p, r, N, M)
  shows refinementIndex(p, r, N, M, i) ∈ ℕ ∧
    (i ≤ N → refinementIndex(p, r, N, M, i) ≤ M ∧
      r[refinementIndex(p, r, N, M, i)] = p[i]) ∧
    (¬(i ≤ N) → refinementIndex(p, r, N, M, i) = 0)
proof
  have exists := refinementIndex.exists at p, r, N, M, i with contained
  have inhabited : Nonempty(refinementIndex.candidates(p, r, N, M, i)) by simp [refinementIndex.candidates, Nonempty]
  have naturals : refinementIndex.candidates(p, r, N, M, i) ⊆ ℕ by simp [refinementIndex.candidates, Subset]
  have member := leastNatural.member at refinementIndex.candidates(p, r, N, M, i) with *
  have data := refinementIndex.candidates.membership.forward at
    p, r, N, M, i, leastNatural(refinementIndex.candidates(p, r, N, M, i)) with *
  simpa [refinementIndex] using data

defgraph refinementIndices (p r : Set, N M : Nat) (i ∈ ℕ) : ℕ :=
  refinementIndex(p, r, N, M, i)
requires contained : VerticesContained(p, r, N, M)
proof
  obtain ⟨natural, bounded, outside⟩ := refinementIndex.selected at p, r, N, M, i with contained
  exact natural

theorem refinementIndices.vertex (p r : Set) (N M i : Nat)
  requires contained : VerticesContained(p, r, N, M)
  requires bounded : i ≤ N
  shows refinementIndices(p, r, N, M)[i] ≤ M ∧
    r[refinementIndices(p, r, N, M)[i]] = p[i]
proof
  obtain ⟨natural, valid, outside⟩ := refinementIndex.selected at p, r, N, M, i with contained
  have data := valid with bounded
  have value := refinementIndices.value at p, r, N, M, i with contained
  rwa value

theorem refinementIndices.strict_cell (p r : Set) (A B : Real, N M i : Nat)
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  requires before : i < N
  shows Less(refinementIndices(p, r, N, M)[i],
    refinementIndices(p, r, N, M)[succ(i)])
proof
  have hFunction : refinementIndices(p, r, N, M) : ℕ → ℕ
    exact refinementIndices.function with contained
  have naturalI := nat.omega.forward at i with assumption
  have nextI := Naturals.constructor.succ at i
  have naturalNext := nat.omega.forward with nextI
  have firstNatural := FunctionBetween.apply_closed with hFunction, naturalI
  have secondNatural := FunctionBetween.apply_closed with hFunction, naturalNext
  have firstTyped := nat.omega.backward with firstNatural
  have secondTyped := nat.omega.backward with secondNatural
  have boundedI := Less.implies_LessEqual with before
  have boundedNext : succ(i) ≤ N by exact before
  have firstData := refinementIndices.vertex with contained, boundedI
  have nextData := refinementIndices.vertex with contained, boundedNext
  rcases firstData with ⟨firstBound, firstValue⟩
  rcases nextData with ⟨nextBound, nextValue⟩
  have coarsePoints : RealSequence(p)
    rcases coarse with ⟨points, start, finish, increasing⟩
    exact points
  have pointI := RealSequence.value at p, i with coarsePoints
  have pointNext := RealSequence.value at p, succ(i) with coarsePoints
  have step := IntervalPartition.cell with coarse, before
  have cases := Less.trichotomy with firstTyped, secondTyped
  cases cases with increasing | rest
  . exact increasing
  cases rest with equal | decreasing
  . rw equal at firstValue
    rw [<- firstValue, <- nextValue] at step
    have contradiction := realLess.characterization.forward with step
    exfalso
    exact RealLess.irreflexive with contradiction
  . have reverse := IntervalPartition.strict_indices at r, A, B, M,
      refinementIndices(p, r, N, M)[succ(i)],
      refinementIndices(p, r, N, M)[i] with fine, decreasing, firstBound
    rw [nextValue, firstValue] at reverse
    have cycle := realLess.transitive with pointI, pointNext, pointI, step, reverse
    have contradiction := realLess.characterization.forward with cycle
    exfalso
    exact RealLess.irreflexive with contradiction

theorem refinementIndices.zero (p r : Set) (A B : Real, N M : Nat)
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  shows refinementIndices(p, r, N, M)[0] = 0
proof
  have zeroBound := Grace.Core.Nat.Order.LessEqual.zero at N
  obtain ⟨bounded, value⟩ := refinementIndices.vertex with contained, zeroBound
  have startP : p[0] = A
    rcases coarse with ⟨points, start, finish, steps⟩
    exact start
  have startR : r[0] = A
    rcases fine with ⟨points, start, finish, steps⟩
    exact start
  rw [startP, <- startR] at value
  have indexFunction := refinementIndices.function with contained
  have member := FunctionBetween.apply_closed at refinementIndices(p, r, N, M),
    ℕ, ℕ, 0 with indexFunction,
      nat.omega.forward at 0 with Naturals.constructor.zero
  have typed := nat.omega.backward with member
  exact IntervalPartition.vertex_index_unique at r, A, B, M,
    refinementIndices(p, r, N, M)[0], 0 with fine, bounded,
      Grace.Core.Nat.Order.LessEqual.zero at M with assumption, value

theorem refinementIndices.last (p r : Set) (A B : Real, N M : Nat)
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  shows refinementIndices(p, r, N, M)[N] = M
proof
  have data := refinementIndices.vertex at p, r, N, M, N with
    contained, LessEqual.reflexive at N with assumption
  rcases data with ⟨bounded, value⟩
  have endP : p[N] = B
    rcases coarse with ⟨points, start, finish, steps⟩
    exact finish
  have endR : r[M] = B
    rcases fine with ⟨points, start, finish, steps⟩
    exact finish
  rw [endP, <- endR] at value
  have indexFunction := refinementIndices.function with contained
  have member := FunctionBetween.apply_closed at refinementIndices(p, r, N, M),
    ℕ, ℕ, N with indexFunction, nat.omega.forward at N with assumption
  have typed := nat.omega.backward with member
  exact IntervalPartition.vertex_index_unique at r, A, B, M,
    refinementIndices(p, r, N, M)[N], M with fine, bounded,
      LessEqual.reflexive at M with assumption, value

-- RefinementSegments
defunique refinementSegmentCount (p r : Set, A B : Real, N M i : Nat) (d ∈ ℕ) :=
  (i < N → add(refinementIndices(p, r, N, M)[i], d) =
    refinementIndices(p, r, N, M)[succ(i)]) ∧
  (¬(i < N) → d = 0)
requires coarse : IntervalPartition(p, A, B, N)
requires fine : IntervalPartition(r, A, B, M)
requires contained : VerticesContained(p, r, N, M)
proof
  have alternatives : i < N ∨ ¬(i < N) by tauto
  cases alternatives with before | beyond
  . have strict := refinementIndices.strict_cell at p, r, A, B, N, M, i with
      coarse, fine, contained, before
    obtain ⟨L, naturalL, length⟩ := strict
    have hFunction := refinementIndices.function with contained
    have naturalI := nat.omega.forward at i with assumption
    have hMember := FunctionBetween.apply_closed with hFunction, naturalI
    have hNat := nat.omega.backward with hMember
    have shape := add.succ_right at L, refinementIndices(p, r, N, M)[i] with hNat
    witness succ(L)
    constructor
    . exact nat.omega.forward at succ(L) with
        Naturals.constructor.succ at L with naturalL
    . constructor
      . intro again
        rw add at length
        rwa shape
      . intro impossible
        exfalso
        exact impossible with before
  . witness 0
    constructor
    . exact nat.omega.forward at 0 with Naturals.constructor.zero
    . constructor
      . intro before
        exfalso
        exact beyond with before
      . intro ignored
        rfl

uniqueness
  intros d memberD first e memberE second
  have naturalD := nat.omega.backward with memberD
  have naturalE := nat.omega.backward with memberE
  have alternatives : i < N ∨ ¬(i < N) by tauto
  cases alternatives with before | beyond
  . have firstValue : add(refinementIndices(p, r, N, M)[i], d) =
        refinementIndices(p, r, N, M)[succ(i)]
      tauto
    have secondValue : add(refinementIndices(p, r, N, M)[i], e) =
        refinementIndices(p, r, N, M)[succ(i)]
      tauto
    have hFunction := refinementIndices.function with contained
    have hMember := FunctionBetween.apply_closed at refinementIndices(p, r, N, M),
      ℕ, ℕ, i with hFunction, nat.omega.forward at i with assumption
    have hNat := nat.omega.backward with hMember
    have same : add(refinementIndices(p, r, N, M)[i], d) =
        add(refinementIndices(p, r, N, M)[i], e)
      cc
    exact add.left_cancel with hNat, same
  . have firstZero : d = 0
      tauto
    have secondZero : e = 0 by tauto
    cc

defgraph refinementSegmentCounts (p r : Set, A B : Real, N M : Nat) (i ∈ ℕ) : ℕ :=
  refinementSegmentCount(p, r, A, B, N, M, i)
requires coarse : IntervalPartition(p, A, B, N)
requires fine : IntervalPartition(r, A, B, M)
requires contained : VerticesContained(p, r, N, M)
proof
  have selected := refinementSegmentCount.selected at p, r, A, B, N, M, i with
    coarse, fine, contained
  rcases selected with ⟨natural, valid, outside⟩
  exact natural

theorem refinementSegmentCounts.endpoint (p r : Set) (A B : Real, N M i : Nat)
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  requires before : i < N
  shows add(refinementIndices(p, r, N, M)[i],
    refinementSegmentCounts(p, r, A, B, N, M)[i]) =
      refinementIndices(p, r, N, M)[succ(i)]
proof
  have selected := refinementSegmentCount.selected at p, r, A, B, N, M, i with
    coarse, fine, contained
  rcases selected with ⟨natural, valid, outside⟩
  have data := valid with before
  have value := refinementSegmentCounts.value at p, r, A, B, N, M, i with
    coarse, fine, contained
  rwa value

-- RefinementSlices
theorem TaggedPartition.refinement_cell (p r : Set) (A B : Real, N M i : Nat)
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  requires before : i < N
  shows TaggedPartition(
    shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),
    shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),
    p[i], p[succ(i)], refinementSegmentCounts(p, r, A, B, N, M)[i])
proof
  have boundedI := Less.implies_LessEqual with before
  have boundedNext : succ(i) ≤ N by exact before
  have first := refinementIndices.vertex with contained, boundedI
  have next := refinementIndices.vertex with contained, boundedNext
  rcases first with ⟨firstBound, firstValue⟩
  rcases next with ⟨nextBound, nextValue⟩
  have naturalI := nat.omega.forward at i with assumption
  have nextI := Naturals.constructor.succ at i
  have naturalNext := nat.omega.forward with nextI
  have indexFunction := refinementIndices.function with contained
  have firstMember := FunctionBetween.apply_closed with indexFunction, naturalI
  have nextMember := FunctionBetween.apply_closed with indexFunction, naturalNext
  have firstNat := nat.omega.backward with firstMember
  have nextNat := nat.omega.backward with nextMember
  have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained
  have segmentMember := FunctionBetween.apply_closed with segmentFunction, naturalI
  have segmentNat := nat.omega.backward with segmentMember
  have pointsR : RealSequence(r)
    rcases fine with ⟨points, start, finish, increasing⟩
    exact points
  have endpointReal := RealSequence.value at r,
    refinementIndices(p, r, N, M)[succ(i)] with pointsR
  have length := refinementSegmentCounts.endpoint with coarse, fine, contained, before
  obtain ⟨R, naturalR, finish⟩ := nextBound
  have partitionPrefix : IntervalPartition(r, A, r[refinementIndices(p, r, N, M)[succ(i)]],
      refinementIndices(p, r, N, M)[succ(i)])
    rw <- finish at fine
    exact IntervalPartition.prefix with fine
  have taggedFull := IntervalPartition.left_tagged with fine
  have taggedPrefix : TaggedPartition(r, leftPartitionTags(r), A,
      r[refinementIndices(p, r, N, M)[succ(i)]],
      refinementIndices(p, r, N, M)[succ(i)])
    rw <- finish at taggedFull
    exact TaggedPartition.prefix with taggedFull
  have taggedSlice : TaggedPartition(
      shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),
      shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),
      r[refinementIndices(p, r, N, M)[i]],
      r[refinementIndices(p, r, N, M)[succ(i)]],
      refinementSegmentCounts(p, r, A, B, N, M)[i])
    have taggedLength : TaggedPartition(r, leftPartitionTags(r), A,
        r[refinementIndices(p, r, N, M)[succ(i)]],
        add(refinementIndices(p, r, N, M)[i],
          refinementSegmentCounts(p, r, A, B, N, M)[i]))
      rwa length
    exact TaggedPartition.suffix at r, leftPartitionTags(r), A,
      r[refinementIndices(p, r, N, M)[succ(i)]],
      refinementIndices(p, r, N, M)[i],
      refinementSegmentCounts(p, r, A, B, N, M)[i] with endpointReal, taggedLength
  rwa [firstValue, nextValue] at taggedSlice

-- RefinementCellSums
defgraph refinementCellSums (f p r : Set, A B : Real, N M : Nat) (i ∈ ℕ) : ℝ :=
  riemannSum(f,
    shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),
    shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),
    refinementSegmentCounts(p, r, A, B, N, M)[i])
requires function : f : ℝ → ℝ
requires coarse : IntervalPartition(p, A, B, N)
requires fine : IntervalPartition(r, A, B, M)
requires contained : VerticesContained(p, r, N, M)
proof
  have points : RealSequence(r)
    rcases fine with ⟨points, start, finish, increasing⟩
    exact points
  have tags : RealSequence(leftPartitionTags(r))
    unfold RealSequence
    exact leftPartitionTags.function with points
  have indexFunction := refinementIndices.function with contained
  have indexMember := FunctionBetween.apply_closed with indexFunction, member
  have indexNat := nat.omega.backward with indexMember
  have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained
  have segmentMember := FunctionBetween.apply_closed with segmentFunction, member
  have segmentNat := nat.omega.backward with segmentMember
  have shiftedPoints := shiftedRealSequence.sequence at r,
    refinementIndices(p, r, N, M)[i] with points
  have shiftedTags := shiftedRealSequence.sequence at leftPartitionTags(r),
    refinementIndices(p, r, N, M)[i] with tags
  have sum := riemannSum.real at f,
    shiftedRealSequence(r, refinementIndices(p, r, N, M)[i]),
    shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i]),
    refinementSegmentCounts(p, r, A, B, N, M)[i] with function, shiftedPoints, shiftedTags
  exact sum

theorem CellwiseSubdivisionSums.refinement (f p r : Set) (A B : Real, N M : Nat)
  requires function : f : ℝ → ℝ
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  shows CellwiseSubdivisionSums(f, p,
    refinementCellSums(f, p, r, A, B, N, M), N)
proof
  have sequence : RealSequence(refinementCellSums(f, p, r, A, B, N, M))
    unfold RealSequence
    exact refinementCellSums.function with function, coarse, fine, contained
  constructor
  . exact sequence
  . intros i naturalI before
    have typedI := nat.omega.backward with naturalI
    have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained
    have segmentMember := FunctionBetween.apply_closed with segmentFunction, naturalI
    witness shiftedRealSequence(r, refinementIndices(p, r, N, M)[i])
    witness shiftedRealSequence(leftPartitionTags(r), refinementIndices(p, r, N, M)[i])
    witness refinementSegmentCounts(p, r, A, B, N, M)[i]
    constructor
    . exact segmentMember
    . constructor
      . exact TaggedPartition.refinement_cell at p, r, A, B, N, M, i with
          coarse, fine, contained, before
      . exact refinementCellSums.value at f, p, r, A, B, N, M, i with
          function, coarse, fine, contained

-- RefinementTotal
theorem refinementCellSums.prefix_total (f p r : Set) (A B : Real, N M n : Nat)
  requires function : f : ℝ → ℝ
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  shows n ≤ N → realPartialSum(refinementCellSums(f, p, r, A, B, N, M), n) =
    riemannSum(f, r, leftPartitionTags(r), refinementIndices(p, r, N, M)[n])
proof
  induction n
  | zero =>
    intro bounded
    have start := refinementIndices.zero with coarse, fine, contained
    rw [start, realPartialSum.zero, riemannSum.zero]
    rfl
  | succ(k) using ih =>
    intro bounded
    have before : k < N by exact bounded
    have kBound := Less.implies_LessEqual with before
    have previous := ih with kBound
    have endpoint := refinementSegmentCounts.endpoint with coarse, fine, contained, before
    have indexFunction := refinementIndices.function with contained
    have naturalK := nat.omega.forward at k with assumption
    have indexMember := FunctionBetween.apply_closed with indexFunction, naturalK
    have indexNat := nat.omega.backward with indexMember
    have segmentFunction := refinementSegmentCounts.function with coarse, fine, contained
    have segmentMember := FunctionBetween.apply_closed with segmentFunction, naturalK
    have segmentNat := nat.omega.backward with segmentMember
    have points : RealSequence(r)
      rcases fine with ⟨points, start, finish, increasing⟩
      exact points
    have tags : RealSequence(leftPartitionTags(r))
      unfold RealSequence
      exact leftPartitionTags.function with points
    have split := riemannSum.split_at at f, r, leftPartitionTags(r),
      refinementIndices(p, r, N, M)(k),
      refinementSegmentCounts(p, r, A, B, N, M)(k) with function, points, tags
    rw endpoint at split
    have value := refinementCellSums.value at f, p, r, A, B, N, M, k with
      function, coarse, fine, contained
    rw [realPartialSum.succ, value, previous]
    simp [realAddValue, call2]

theorem refinementCellSums.total (f p r : Set) (A B : Real, N M : Nat)
  requires function : f : ℝ → ℝ
  requires coarse : IntervalPartition(p, A, B, N)
  requires fine : IntervalPartition(r, A, B, M)
  requires contained : VerticesContained(p, r, N, M)
  shows realPartialSum(refinementCellSums(f, p, r, A, B, N, M), N) =
    riemannSum(f, r, leftPartitionTags(r), M)
proof
  have prefix := refinementCellSums.prefix_total at f, p, r, A, B, N, M, N with
    function, coarse, fine, contained
  have bound := LessEqual.reflexive at N
  have total := prefix with bound
  have last := refinementIndices.last with coarse, fine, contained
  rwa last at total

-- ArbitrarySharedTotal
theorem FinePartition.shared_subdivision (f p q : Set) (A B D : Real, N M : Nat)
  requires function : f : ℝ → ℝ
  requires fineP : FinePartition(p, A, B, N, D)
  requires fineQ : FinePartition(q, A, B, M, D)
  shows ∃ u, ∃ v, SharedSubdivisionTotal(f, p, q, u, v, N, M)
proof
  obtain ⟨r, L, naturalL, fineR, containedP, containedQ⟩ := FinePartition.common_vertices with
    function, fineP, fineQ
  have partitionP : IntervalPartition(p, A, B, N)
    rcases fineP with ⟨partition, positive, widths⟩
    exact partition
  have partitionQ : IntervalPartition(q, A, B, M)
    rcases fineQ with ⟨partition, positive, widths⟩
    exact partition
  have partitionR : IntervalPartition(r, A, B, L)
    rcases fineR with ⟨partition, positive, widths⟩
    exact partition
  have cellsP := CellwiseSubdivisionSums.refinement with function, partitionP, partitionR, containedP
  have cellsQ := CellwiseSubdivisionSums.refinement with function, partitionQ, partitionR, containedQ
  have totalP := refinementCellSums.total with function, partitionP, partitionR, containedP
  have totalQ := refinementCellSums.total with function, partitionQ, partitionR, containedQ
  witness refinementCellSums(f, p, r, A, B, N, L)
  witness refinementCellSums(f, q, r, A, B, M, L)
  constructor
  . exact cellsP
  . constructor
    . exact cellsQ
    . rw [totalP, totalQ]
      rfl

theorem FineCellOscillation.compare_fine_partitions (f p t q s : Set) (A B D E : Real, N M : Nat)
  requires function : f : ℝ → ℝ
  requires oscillation : FineCellOscillation(f, A, B, D, E)
  requires fineP : FinePartition(p, A, B, N, D)
  requires fineQ : FinePartition(q, A, B, M, D)
  requires taggedP : TaggedPartition(p, t, A, B, N)
  requires taggedQ : TaggedPartition(q, s, A, B, M)
  shows (riemannSum(f, p, t, N):R) ≤ (riemannSum(f, q, s, M):R) + (E + E) * (B - A) ∧
    (riemannSum(f, q, s, M):R) ≤ (riemannSum(f, p, t, N):R) + (E + E) * (B - A)
proof
  obtain ⟨u, v, shared⟩ := FinePartition.shared_subdivision at f, p, q, A, B, D, N, M
    with function, fineP, fineQ
  exact FineCellOscillation.compare_shared_subdivision with
    function, oscillation, fineP, fineQ, taggedP, taggedQ, shared