-- Real analysis: SequentialCompactness
-- 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.SequentialCompactness
import Nat.Least
import Sequences
import Intervals

-- Section: Monotone
predicate Nondecreasing (u : Set) :=
  ∀ m ∈ ℕ, ∀ n ∈ ℕ, m ≤ n →
    RealLe(u(m), u(n))

predicate Nonincreasing (u : Set) :=
  ∀ m ∈ ℕ, ∀ n ∈ ℕ, m ≤ n →
    RealLe(u(n), u(m))

predicate StepwiseNondecreasing (u : Set) :=
  ∀ n ∈ ℕ, RealLe(u[n], u[succ(n)])

predicate StepwiseNonincreasing (u : Set) :=
  ∀ n ∈ ℕ, RealLe(u[succ(n)], u[n])

theorem StepwiseNondecreasing.offset (u : Set, m k : Nat)
  requires sequence : RealSequence(u)
  requires stepwise : StepwiseNondecreasing(u)
  shows RealLe(u[m], u[m + k])
proof
  induction k
  | zero =>
    have shape := add.right_unit at m with assumption
    rw shape
    have realM := RealSequence.value with sequence
    exact RealLe.reflexive with realM
  | succ(j) using ih =>
    have sumNatural := add.closed at j, m with h_j
    have sumInNaturals := nat.omega.forward with sumNatural
    have next := stepwise with m + j, sumInNaturals
    have combined := RealLe.transitive at u[m], u[m + j], u[succ(m + j)] with
      ih, next
    have shape := add.succ_right at j, m
    rw shape
    exact combined

theorem StepwiseNondecreasing.nondecreasing (u : Set)
  requires sequence : RealSequence(u)
  requires stepwise : StepwiseNondecreasing(u)
  shows Nondecreasing(u)
proof
  intros m mNatural n nNatural order
  obtain ⟨k, kNatural, shape⟩ := order
  have offset := StepwiseNondecreasing.offset at u, m, k with sequence, stepwise
  rw shape at offset
  exact offset

theorem StepwiseNonincreasing.offset (u : Set, m k : Nat)
  requires sequence : RealSequence(u)
  requires stepwise : StepwiseNonincreasing(u)
  shows RealLe(u[m + k], u[m])
proof
  induction k
  | zero =>
    have shape := add.right_unit at m with assumption
    rw shape
    have realM := RealSequence.value with sequence
    exact RealLe.reflexive with realM
  | succ(j) using ih =>
    have sumNatural := add.closed at j, m with h_j
    have sumInNaturals := nat.omega.forward with sumNatural
    have next := stepwise with m + j, sumInNaturals
    have combined := RealLe.transitive at u[succ(m + j)], u[m + j], u[m] with
      next, ih
    have shape := add.succ_right at j, m
    rw shape
    exact combined

theorem StepwiseNonincreasing.nonincreasing (u : Set)
  requires sequence : RealSequence(u)
  requires stepwise : StepwiseNonincreasing(u)
  shows Nonincreasing(u)
proof
  intros m mNatural n nNatural order
  obtain ⟨k, kNatural, shape⟩ := order
  have offset := StepwiseNonincreasing.offset at u, m, k with sequence, stepwise
  rw shape at offset
  exact offset

-- The range of a real sequence is exactly the family to which completeness
-- should be applied.  These small bridges keep the main proof mathematical.
theorem RealSequence.range_nonempty (u : Set)
  requires sequence : RealSequence(u)
  shows Nonempty(range(u))
proof
  have zeroNatural := nat.omega.forward with Naturals.constructor.zero
  have mapped := FunctionBetween.relates_apply at u, ℕ, ℝ, 0 with
    sequence, zeroNatural
  witness u₀
  unfold relates at mapped
  exact range.contains with mapped

theorem RealSequence.range_subset_reals (u : Set)
  requires sequence : RealSequence(u)
  shows range(u) ⊆ ℝ
proof
  intros A member
  obtain ⟨_, n, pairInU⟩ := range.membership.forward with member
  rcases sequence with ⟨relation, functional, total⟩
  unfold RelationBetween at relation
  have boundedPair := relation with (n, A), pairInU
  obtain ⟨_, i, iNatural, B, bReal, shape⟩ := product.membership.forward with boundedPair
  obtain ⟨_, equalA⟩ := orderedPair.injective with shape
  rwa equalA

theorem BoundedAboveBy.range_upper_bound (u : Set) (B : Real)
  requires sequence : RealSequence(u)
  requires bounded : BoundedAboveBy(u, B)
  shows RealUpperBound(range(u), B)
proof
  have typedB : Real(B) by typecheck
  constructor
  . exact typedB
  constructor
  . exact RealSequence.range_subset_reals with sequence
  . intros A member
    unfold RealSequence at sequence
    obtain ⟨_, n, pairInU⟩ := range.membership.forward with member
    obtain ⟨relation, functional, total⟩ := sequence
    unfold RelationBetween at relation
    have boundedPair := relation with (n, A), pairInU
    obtain ⟨_, i, iNatural, C, cReal, shape⟩ := product.membership.forward with boundedPair
    obtain ⟨equalN, equalA⟩ := orderedPair.injective with shape
    have nNatural : n ∈ ℕ by rwa equalN
    have mapped : relates(u, n, A) by exact pairInU
    have value := FunctionBetween.apply_value with sequence, mapped
    obtain ⟨_, _, subset⟩ := bounded with n, nNatural
    rwa ← value

-- A least upper bound is approached from below.  If no member lay above
-- U - E, then U - E itself would be a smaller upper bound.
theorem RealLeastUpperBound.approached (S : Set) (U E : Real)
  requires least : RealLeastUpperBound(S, U)
  requires positiveE : 0 < E
  shows ∃ A ∈ S, U - E < A
proof
  have realE : Real(E) by typecheck
  have upperU : RealUpperBound(S, U) by simp [RealLeastUpperBound]
  have leastU : ∀ B, RealUpperBound(S, B) → U ⊆ B by simp [RealLeastUpperBound]
  rcases upperU with ⟨realU, reals, bounds⟩
  have differenceReal := realSubValue.real with realU, realE
  have positiveView := realLess.characterization.forward with positiveE
  have reversedView := RealLess.neg_reverse with positiveView
  have negative : -E < -realZero by exact realLess.characterization.backward at -E, -realZero with reversedView
  rw realNegValue.zero at negative
  have differenceBelow := realLess.add_left at -E, realZero, U with
    realNegValue.real at E with realE, realZero.real, realU, negative
  have zeroRight := realAddValue.zero_right with realU
  rw zeroRight at differenceBelow
  have differenceBelowSub : U - E < U
    unfold realSubValue
    exact differenceBelow
  by_contra noApproach
  have candidateUpper : RealUpperBound(S, U - E)
    constructor
    . exact differenceReal
    constructor
    . exact reals
    . intros A member
      have aInReals := reals with A, member
      have realA : Real(A) by exact aInReals
      have cutA := Real.characterization.forward with realA
      have cutDifference := Real.characterization.forward with differenceReal
      have comparison := DedekindCut.comparable with cutA, cutDifference
      cases comparison with aBelow | differenceBelowA
      . exact aBelow
      . by_contra notBelow
        have unequal : U - E ≠ A
          intro equal
          apply notBelow
          rw equal
          exact Subset.reflexive
        have proper : U - E ⊂ A
          constructor
          . exact differenceBelowA
          . exact unequal
        have tooClose : U - E < A
          apply realLess.characterization.backward
          unfold RealLess
          refine ⟨differenceReal, realA, proper⟩
        apply noApproach
        witness A
        refine ⟨member, tooClose⟩
  have upperBelow := leastU with U - E, candidateUpper
  obtain ⟨_, _, properBelow⟩ := realLess.characterization.forward with differenceBelowSub
  have belowSubset := ProperSubset.subset with properBelow
  have equal := Subset.antisymmetric with belowSubset, upperBelow
  exact ProperSubset.ne with properBelow, equal

-- The bounded monotone convergence theorem, with the limit displayed as the
-- supremum of the range.
theorem Nondecreasing.converges_to_supremum (u : Set) (B : Real)
  requires sequence : RealSequence(u)
  requires increasing : Nondecreasing(u)
  requires bounded : BoundedAboveBy(u, B)
  shows ConvergesTo(u, realSup(range(u)))
proof
  have inhabited := RealSequence.range_nonempty with sequence
  have rangeUpper := BoundedAboveBy.range_upper_bound with sequence, bounded
  have least := realSup.least_upper_bound with inhabited, rangeUpper
  have supUpper : RealUpperBound(range(u), realSup(range(u))) by simp [RealLeastUpperBound]
  rcases supUpper with ⟨supReal, rangeReals, supBounds⟩
  have typedSup : Real(realSup(range(u))) by exact supReal
  constructor
  . exact sequence
  . intros E eInReals positiveE
    have typedE : Real(E) by exact eInReals
    obtain ⟨A, aInRange, closeA⟩ := RealLeastUpperBound.approached with least, positiveE
    unfold RealSequence at sequence
    obtain ⟨_, N, pairInU⟩ := range.membership.forward with aInRange
    obtain ⟨relation, functional, total⟩ := sequence
    unfold RelationBetween at relation
    have boundedPair := relation with (N, A), pairInU
    obtain ⟨_, i, iNatural, C, cReal, shape⟩ := product.membership.forward with boundedPair
    obtain ⟨equalN, equalA⟩ := orderedPair.injective with shape
    have nNatural : N ∈ ℕ by rwa equalN
    have mapped : relates(u, N, A) by exact pairInU
    have valueAtN := FunctionBetween.apply_value with sequence, mapped
    rw ← valueAtN at closeA
    have supBelowPlus := realLess.add_left with realZero.real, typedE, typedSup, positiveE
    have supZero := realAddValue.zero_right with typedSup
    rw supZero at supBelowPlus
    witness N
    constructor
    . exact nNatural
    . intros n littleNInNaturals nAfterN
      have valueNReal := FunctionBetween.apply_closed with sequence, littleNInNaturals
      have valueAtNReal := FunctionBetween.apply_closed with sequence, nNatural
      have monotoneView := increasing with
        N, nNatural, n, littleNInNaturals, nAfterN
      have monotoneLe := realLe.characterization.backward with monotoneView
      have lower := realLess.transitive_le with closeA, monotoneLe
      have mappedN := FunctionBetween.relates_apply with sequence, littleNInNaturals
      unfold relates at mappedN
      have valueInRange := range.contains with mappedN
      have valueSubsetSup := supBounds with uₙ, valueInRange
      have valueLeSup := realLe.of_subset with valueSubsetSup
      have upper := realLe.transitive_less with valueLeSup, supBelowPlus
      have interval : (realSup(range(u)) - E < uₙ ∧ uₙ < realSup(range(u)) + E)
        constructor
        . exact lower
        . exact upper
      exact openBall.order_characterization.backward with interval

theorem Nonincreasing.neg_nondecreasing (u : Set)
  requires sequence : RealSequence(u)
  requires decreasing : Nonincreasing(u)
  shows Nondecreasing(negSequence(u))
proof
  intros m mNatural n nNatural order
  have descendsView := decreasing with m, mNatural, n, nNatural, order
  have descends := realLe.characterization.backward with descendsView
  have reversed := realLe.neg_reverse with descends
  have reversedView := realLe.characterization.forward with reversed
  have realM := RealSequence.value at u, m with sequence
  have realN := RealSequence.value at u, n with sequence
  have valueM := negSequence.value with sequence, realM
  have valueN := negSequence.value with sequence, realN
  rwa [valueM, valueN]

theorem BoundedBelowBy.neg_bounded_above (u : Set) (A : Real)
  requires sequence : RealSequence(u)
  requires bounded : BoundedBelowBy(u, A)
  shows BoundedAboveBy(negSequence(u), -A)
proof
  intros n nNatural
  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
  have lowerView := bounded with n, nNatural
  have lower := realLe.characterization.backward with lowerView
  have reversed := realLe.neg_reverse with lower
  have reversedView := realLe.characterization.forward with reversed
  have realN := RealSequence.value with sequence
  have value := negSequence.value with sequence, realN
  rwa value

-- The canonical infimum of a real sequence, displayed as the negative of
-- the supremum of its negated range.
def realSequenceInfimum (u : Set) : Set :=
  realNeg(realSup(range(negSequence(u))))

theorem realSequenceInfimum.real (u : Set) (A : Real)
  requires sequence : RealSequence(u)
  requires bounded : BoundedBelowBy(u, A)
  shows Real(realSequenceInfimum(u))
proof
  have negative := negSequence.sequence with sequence
  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded
  have inhabited := RealSequence.range_nonempty with negative
  have rangeUpper := BoundedAboveBy.range_upper_bound with negative, negBounded
  have least := realSup.least_upper_bound with inhabited, rangeUpper
  have supUpper : RealUpperBound(
      range(negSequence(u)), realSup(range(negSequence(u))))
    simp [RealLeastUpperBound]
  rcases supUpper with ⟨supReal, rangeReals, bounds⟩
  have negativeReal := realNegValue.real with supReal
  unfold realSequenceInfimum
  exact negativeReal

-- The decreasing half of monotone convergence is the increasing theorem
-- applied to the negated sequence.
theorem Nonincreasing.converges_to_infimum (u : Set) (A : Real)
  requires sequence : RealSequence(u)
  requires decreasing : Nonincreasing(u)
  requires bounded : BoundedBelowBy(u, A)
  shows ConvergesTo(u, realSequenceInfimum(u))
proof
  unfold realSequenceInfimum
  have negSequenceReal := negSequence.sequence with sequence
  have negIncreasing := Nonincreasing.neg_nondecreasing with sequence, decreasing
  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded
  have negConverges := Nondecreasing.converges_to_supremum with negSequenceReal, negIncreasing, negBounded
  have inhabited := RealSequence.range_nonempty with negSequenceReal
  have rangeUpper := BoundedAboveBy.range_upper_bound with negSequenceReal, negBounded
  have least := realSup.least_upper_bound with inhabited, rangeUpper
  have supUpper : RealUpperBound(
      range(negSequence(u)), realSup(range(negSequence(u))))
    simp [RealLeastUpperBound]
  rcases supUpper with ⟨supReal, rangeReals, bounds⟩
  have typedSup : Real(realSup(range(negSequence(u)))) by exact supReal
  have limitReal := realNegValue.real with typedSup
  constructor
  . exact sequence
  . intros E eInReals positiveE
    have typedE : Real(E) by exact eInReals
    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with negConverges, positiveE
    witness N
    constructor
    . exact nNatural
    . intros n littleNatural afterN
      have typedN : Nat(n) by exact nat.omega.backward at n with littleNatural
      have realValue := RealSequence.value with sequence
      have realNegValue := RealSequence.value with negSequenceReal
      have near := close with n, littleNatural, afterN
      obtain ⟨negValueReal, within⟩ := openBall.membership.forward with near
      have valueShape := negSequence.value with sequence, realValue
      rw valueShape at within
      have distanceNeg := dist.neg with realValue, limitReal
      have involutive := realNegValue.involutive with typedSup
      rw involutive at distanceNeg
      apply openBall.membership.backward
      constructor
        exact realValue
      . rw ← distanceNeg
        exact within

theorem Nonincreasing.infimum_le_term (u : Set) (A : Real, n : Nat)
  requires sequence : RealSequence(u)
  requires bounded : BoundedBelowBy(u, A)
  shows (realSequenceInfimum(u) : R) ≤ (u[n] : R)
proof
  have negative := negSequence.sequence with sequence
  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded
  have inhabited := RealSequence.range_nonempty with negative
  have rangeUpper := BoundedAboveBy.range_upper_bound with negative, negBounded
  have least := realSup.least_upper_bound with inhabited, rangeUpper
  have supUpper : RealUpperBound(
      range(negSequence(u)), realSup(range(negSequence(u))))
    simp [RealLeastUpperBound]
  rcases supUpper with ⟨supReal, rangeReals, bounds⟩
  have naturalN : n ∈ ℕ by simp [Nat]
  have negativeFunction := negative
  unfold RealSequence at negativeFunction
  have mapped := FunctionBetween.relates_apply with negativeFunction, naturalN
  unfold relates at mapped
  have inRange := range.contains with mapped
  have view := bounds with negSequence(u)[n], inRange
  have realN := RealSequence.value with sequence
  have negValue := negSequence.value with sequence, realN
  rw negValue at view
  have negReal := realNegValue.real with realN
  have upper := realLe.of_subset with negReal, supReal, view
  have reversed := realLe.neg_reverse with upper
  have involutive := realNegValue.involutive with realN
  rw involutive at reversed
  unfold realSequenceInfimum
  exact reversed

-- The usual existential form follows from the displayed infimum.
theorem Nonincreasing.has_limit (u : Set) (A : Real)
  requires sequence : RealSequence(u)
  requires decreasing : Nonincreasing(u)
  requires bounded : BoundedBelowBy(u, A)
  shows ∃ L ∈ ℝ, ConvergesTo(u, L)
proof
  have converges := Nonincreasing.converges_to_infimum with sequence, decreasing, bounded
  unfold realSequenceInfimum at converges
  have negSequenceReal := negSequence.sequence with sequence
  have inhabited := RealSequence.range_nonempty with negSequenceReal
  have negBounded := BoundedBelowBy.neg_bounded_above with sequence, bounded
  have rangeUpper := BoundedAboveBy.range_upper_bound with negSequenceReal, negBounded
  have least := realSup.least_upper_bound with inhabited, rangeUpper
  have supUpper : RealUpperBound(
      range(negSequence(u)), realSup(range(negSequence(u))))
    simp [RealLeastUpperBound]
  rcases supUpper with ⟨supReal, rangeReals, bounds⟩
  have limitReal := realNegValue.real with supReal
  witness -realSup(range(negSequence(u)))
  constructor
    exact limitReal
  . exact converges

-- Section: SequentialCompactness
predicate NestedClosedIntervals (a b : Set) :=
  RealSequence(a) ∧ RealSequence(b) ∧
  Nondecreasing(a) ∧ Nonincreasing(b) ∧ PointwiseLE(a, b)

theorem NestedClosedIntervals.lower_sequence (a b : Set)
  requires nested : NestedClosedIntervals(a, b)
  shows RealSequence(a)
proof
  simp [NestedClosedIntervals]

theorem NestedClosedIntervals.upper_sequence (a b : Set)
  requires nested : NestedClosedIntervals(a, b)
  shows RealSequence(b)
proof
  simp [NestedClosedIntervals]

theorem NestedClosedIntervals.intervals_nested (a b : Set) (m n : Nat)
  requires nested : NestedClosedIntervals(a, b)
  requires order : m ≤ n
  shows closedInterval(a[n], b[n]) ⊆ closedInterval(a[m], b[m])
proof
  rcases nested with
    ⟨sequenceA, sequenceB, increasing, decreasing, ordered⟩
  have lowerView := increasing with m, n, order
  have upperView := decreasing with m, n, order
  have lower := realLe.characterization.backward with lowerView
  have upper := realLe.characterization.backward with upperView
  have realAN := RealSequence.value at a, n with sequenceA
  have realBN := RealSequence.value at b, n with sequenceB
  have realAM := RealSequence.value at a, m with sequenceA
  have realBM := RealSequence.value at b, m with sequenceB
  exact closedInterval.nested with realAN, realBN, realAM, realBM, lower, upper

-- Every left endpoint lies below every later or earlier right endpoint.
-- This is the order-theoretic heart of the nested interval theorem.
theorem NestedClosedIntervals.lower_bounded_by_upper (a b : Set) (n : Nat)
  requires nested : NestedClosedIntervals(a, b)
  shows BoundedAboveBy(a, b[n])
proof
  rcases nested with
    ⟨sequenceA, sequenceB, increasing, decreasing, ordered⟩
  intros m mNatural
  have nNatural : n ∈ ℕ by simp [Nat]
  have typedM : Nat(m) by exact nat.omega.backward at m with mNatural
  have comparison := Less.trichotomy at m, n with typedM, assumption
  cases comparison with mBefore | rest
  . have mLeN := Less.implies_LessEqual at m, n with mBefore
    have leftOrder := increasing with m, mNatural, n, mLeN
    have intervalOrder := ordered with n, nNatural
    exact RealLe.transitive with leftOrder, intervalOrder
  . cases rest with equal | nBefore
    . rw equal
      exact ordered with n, nNatural
    . have nLeM := Less.implies_LessEqual at n, m with nBefore
      have intervalOrder := ordered with m, mNatural
      have rightOrder := decreasing with n, m, mNatural, nLeM
      exact RealLe.transitive with intervalOrder, rightOrder

theorem NestedClosedIntervals.lower_bounded (a b : Set)
  requires nested : NestedClosedIntervals(a, b)
  shows BoundedAboveBy(a, b[0])
proof
  exact NestedClosedIntervals.lower_bounded_by_upper with nested

theorem NestedClosedIntervals.supremum_real (a b : Set)
  requires nested : NestedClosedIntervals(a, b)
  shows Real(realSup(range(a)))
proof
  have sequenceA := NestedClosedIntervals.lower_sequence with nested
  have sequenceB := NestedClosedIntervals.upper_sequence with nested
  have inhabited := RealSequence.range_nonempty with sequenceA
  have bounded := NestedClosedIntervals.lower_bounded with nested
  have realB0 := RealSequence.value at b, 0 with sequenceB
  have upper := BoundedAboveBy.range_upper_bound with sequenceA, bounded
  have least := realSup.least_upper_bound with inhabited, upper
  have supremumUpper : RealUpperBound(range(a), realSup(range(a))) by simp [RealLeastUpperBound]
  rcases supremumUpper with ⟨realSupremum, reals, bounds⟩
  exact realSupremum

-- The left endpoints approach the canonical point in the intersection.
theorem NestedClosedIntervals.lower_converges (a b : Set)
  requires nested : NestedClosedIntervals(a, b)
  shows ConvergesTo(a, realSup(range(a)))
proof
  have system := nested
  rcases nested with
    ⟨sequenceA, sequenceB, increasing, decreasing, ordered⟩
  have bounded := NestedClosedIntervals.lower_bounded with system
  exact Nondecreasing.converges_to_supremum with sequenceA, increasing, bounded

theorem NestedClosedIntervals.lower_le_supremum (a b : Set) (n : Nat)
  requires nested : NestedClosedIntervals(a, b)
  shows RealLe(a[n], realSup(range(a)))
proof
  have sequenceA := NestedClosedIntervals.lower_sequence with nested
  have sequenceB := NestedClosedIntervals.upper_sequence with nested
  have inhabited := RealSequence.range_nonempty with sequenceA
  have bounded := NestedClosedIntervals.lower_bounded with nested
  have realB0 := RealSequence.value with sequenceB
  have upper := BoundedAboveBy.range_upper_bound with sequenceA, bounded
  have least := realSup.least_upper_bound with inhabited, upper
  have supremumUpper : RealUpperBound(range(a), realSup(range(a))) by simp [RealLeastUpperBound]
  rcases supremumUpper with ⟨realSupremum, reals, bounds⟩
  have nNatural : n ∈ ℕ by simp [Nat]
  have functionA := sequenceA
  unfold RealSequence at functionA
  have mapped := FunctionBetween.relates_apply with functionA, nNatural
  unfold relates at mapped
  have member := range.contains with mapped
  have subset := bounds with a[n], member
  have realAN := RealSequence.value with sequenceA
  constructor
  . exact realAN
  . constructor
    . exact realSupremum
    . exact subset

theorem NestedClosedIntervals.supremum_le_upper (a b : Set) (n : Nat)
  requires nested : NestedClosedIntervals(a, b)
  shows RealLe(realSup(range(a)), b[n])
proof
  have sequenceA := NestedClosedIntervals.lower_sequence with nested
  have sequenceB := NestedClosedIntervals.upper_sequence with nested
  have boundedN := NestedClosedIntervals.lower_bounded_by_upper with nested
  have realBN := RealSequence.value with sequenceB
  have upperN := BoundedAboveBy.range_upper_bound with sequenceA, boundedN
  have subset := realSup.subset_upper with upperN
  have realSupremum := NestedClosedIntervals.supremum_real with nested
  constructor
  . exact realSupremum
  . constructor
    . exact realBN
    . exact subset

-- Cantor's nested interval theorem, with the common point displayed
-- canonically as the supremum of the left endpoints.
theorem NestedClosedIntervals.contains_supremum (a b : Set) (n : Nat)
  requires nested : NestedClosedIntervals(a, b)
  shows realSup(range(a)) ∈ closedInterval(a[n], b[n])
proof
  have realSupremum := NestedClosedIntervals.supremum_real with nested
  have lowerView := NestedClosedIntervals.lower_le_supremum with nested
  have upperView := NestedClosedIntervals.supremum_le_upper with nested
  have lower := realLe.characterization.backward with lowerView
  have upper := realLe.characterization.backward with upperView
  have realMember : realSup(range(a)) ∈ ℝ by exact realSupremum
  have data : realSup(range(a)) ∈ ℝ ∧ a[n] ≤ realSup(range(a)) ∧ realSup(range(a)) ≤ b[n]
    constructor
    . exact realMember
    . constructor
      . exact lower
      . exact upper
  have sequenceA := NestedClosedIntervals.lower_sequence with nested
  have sequenceB := NestedClosedIntervals.upper_sequence with nested
  have realAN := RealSequence.value with sequenceA
  have realBN := RealSequence.value with sequenceB
  exact closedInterval.membership.backward with data

theorem NestedClosedIntervals.nonempty_intersection (a b : Set)
  requires nested : NestedClosedIntervals(a, b)
  shows ∃ L ∈ ℝ, ∀ n ∈ ℕ, L ∈ closedInterval(a[n], b[n])
proof
  witness realSup(range(a))
  constructor
  . exact NestedClosedIntervals.supremum_real with nested
  . intros n nNatural
    exact NestedClosedIntervals.contains_supremum with nested

-- SequentialCompactness
predicate StrictlyIncreasingNat (k : Set) :=
  FunctionBetween(k, ℕ, ℕ) ∧
  (∀ m ∈ ℕ, ∀ n ∈ ℕ, m < n → Less(kₘ, kₙ))

def subsequence (u k : Set) : Set :=
  compose(u, k, ℕ, ℕ, ℝ)

predicate TermsIn (u S : Set) :=
  ∀ n ∈ ℕ, uₙ ∈ S

predicate SequentiallyCompact (S : Set) :=
  S ⊆ ℝ ∧
  (∀ u, RealSequence(u) → TermsIn(u, S) →
    ∃ k, StrictlyIncreasingNat(k) ∧
      ∃ L ∈ ℝ, L ∈ S ∧ ConvergesTo(subsequence(u, k), L))

theorem StrictlyIncreasingNat.function (k : Set)
  requires increasing : StrictlyIncreasingNat(k)
  shows k : ℕ → ℕ
proof
  simp [StrictlyIncreasingNat]

theorem identity.strictly_increasing_nat
  shows StrictlyIncreasingNat(identity(ℕ))
proof
  constructor
  . exact identity.function at ℕ
  . intros m mNatural n nNatural less
    have valueM := identity.apply with mNatural
    have valueN := identity.apply with nNatural
    rwa [valueM, valueN]

-- A strictly increasing selector has passed its own index by stage n.
theorem StrictlyIncreasingNat.index_le_value (k : Set, n : Nat)
  requires increasing : StrictlyIncreasingNat(k)
  shows n ≤ kₙ
proof
  induction n
  | zero =>
    have function := StrictlyIncreasingNat.function with increasing
    have zeroNatural : 0 ∈ ℕ by exact nat.omega.forward at 0 with Naturals.constructor.zero
    have valueNatural := FunctionBetween.apply_closed with function, zeroNatural
    have typedValue : Nat(k₀) by exact nat.omega.backward at k₀ with valueNatural
    exact Grace.Core.Nat.Order.LessEqual.zero at k₀ with typedValue
  | succ(j) using ih =>
    have function := StrictlyIncreasingNat.function with increasing
    obtain ⟨functionAgain, strict⟩ := increasing
    have jNatural : j ∈ ℕ by simp [Nat]
    have nextNatural : succ(j) ∈ ℕ
      have typedNext := Naturals.constructor.succ at j
      exact nat.omega.forward with typedNext
    have jBeforeNext : j < succ(j)
      unfold Less
      exact LessEqual.reflexive with assumption
    have valuesStrict := strict with
      j, jNatural, succ(j), nextNatural, jBeforeNext
    have typedJValue : Nat(kⱼ)
      have valueNatural := FunctionBetween.apply_closed with function, jNatural
      exact nat.omega.backward with valueNatural
    have typedNextValue : Nat(k[succ(j)])
      have valueNatural := FunctionBetween.apply_closed with function, nextNatural
      exact nat.omega.backward with valueNatural
    have jBeforeValue := LessEqual.transitive_Less at
      j, kⱼ, k[succ(j)] with
        assumption, typedJValue, typedNextValue, ih, valuesStrict
    exact jBeforeValue

theorem subsequence.function (u k : Set)
  requires sequence : RealSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows subsequence(u, k) : ℕ → ℝ
proof
  unfold RealSequence at sequence
  have selector := StrictlyIncreasingNat.function with increasing
  unfold subsequence
  exact compose.function with selector, sequence

theorem subsequence.sequence (u k : Set)
  requires sequence : RealSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows RealSequence(subsequence(u, k))
proof
  unfold RealSequence
  exact subsequence.function with sequence, increasing

theorem subsequence.value (u k : Set, n : Nat)
  requires sequence : RealSequence(u)
  requires increasing : StrictlyIncreasingNat(k)
  shows subsequence(u, k)(n) = u(kₙ)
proof
  have selector := StrictlyIncreasingNat.function with increasing
  have nNatural : n ∈ ℕ by simp [Nat]
  unfold RealSequence at sequence
  have value := compose.apply with selector, sequence, nNatural
  simp [subsequence]

theorem subsequence.identity (u : Set)
  requires sequence : RealSequence(u)
  shows subsequence(u, identity(ℕ)) = u
proof
  unfold RealSequence at sequence
  unfold subsequence
  exact compose.identity_right with sequence

theorem TermsIn.subsequence (u k S : Set)
  requires sequence : RealSequence(u)
  requires terms : TermsIn(u, S)
  requires increasing : StrictlyIncreasingNat(k)
  shows TermsIn(subsequence(u, k), S)
proof
  intros n nNatural
  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
  have selector := StrictlyIncreasingNat.function with increasing
  have selectedNatural := FunctionBetween.apply_closed with selector, nNatural
  have member := terms with kₙ, selectedNatural
  have value := subsequence.value with sequence, increasing
  rwa value

-- Every subsequence of a convergent sequence has the same limit.
theorem ConvergesTo.subsequence (u k : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  requires increasing : StrictlyIncreasingNat(k)
  shows ConvergesTo(subsequence(u, k), L)
proof
  have sequence := ConvergesTo.sequence with converges
  constructor
  . exact subsequence.sequence with sequence, increasing
  . intros E realE positive
    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, positive
    witness N
    constructor
    . exact nNatural
    . intros n littleNatural nAfterN
      have nBeforeValue := StrictlyIncreasingNat.index_le_value at
        k, n with increasing
      have valueNatural := FunctionBetween.apply_closed at
        k, ℕ, ℕ, n with
          StrictlyIncreasingNat.function at k with increasing,
          littleNatural
      have indexAfterN := LessEqual.transitive with nAfterN, nBeforeValue
      have near := close with kₙ, valueNatural, indexAfterN
      have value := subsequence.value at u, k, n with sequence, increasing
      rwa value

theorem ConvergesTo.has_convergent_subsequence (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  shows ∃ k, StrictlyIncreasingNat(k) ∧
    ConvergesTo(subsequence(u, k), L)
proof
  witness identity(ℕ)
  constructor
  . exact identity.strictly_increasing_nat
  . exact ConvergesTo.subsequence at u, identity(ℕ), L with
      converges, identity.strictly_increasing_nat

-- Closed intervals contain limits of sequences whose terms stay inside them.
theorem closedInterval.contains_limit (u : Set) (L A B : Real)
  requires converges : ConvergesTo(u, L)
  requires terms : TermsIn(u, closedInterval(A, B))
  shows L ∈ closedInterval(A, B)
proof
  have sequence := ConvergesTo.sequence with converges
  have lowerBound : BoundedBelowBy(u, A)
    intros n nNatural
    have member := terms with n, nNatural
    obtain ⟨realValue, lower, upper⟩ := closedInterval.membership.forward with member
    exact realLe.characterization.forward with lower
  have upperBound : BoundedAboveBy(u, B)
    intros n nNatural
    have member := terms with n, nNatural
    obtain ⟨realValue, lower, upper⟩ := closedInterval.membership.forward with member
    exact realLe.characterization.forward with upper
  have lower := ConvergesTo.ge_constant with converges, lowerBound
  have upper := ConvergesTo.le_constant with converges, upperBound
  have realL : L ∈ ℝ by simp [Real]
  have data : L ∈ ℝ ∧ A ≤ L ∧ L ≤ B
    constructor
    . exact realL
    . constructor
      . exact lower
      . exact upper
  exact closedInterval.membership.backward with data

theorem closedInterval.contains_subsequence_limit (u k : Set) (L A B : Real)
  requires sequence : RealSequence(u)
  requires terms : TermsIn(u, closedInterval(A, B))
  requires increasing : StrictlyIncreasingNat(k)
  requires converges : ConvergesTo(subsequence(u, k), L)
  shows L ∈ closedInterval(A, B)
proof
  have selectedTerms := TermsIn.subsequence with sequence, terms, increasing
  exact closedInterval.contains_limit with converges, selectedTerms

-- Section: CompactContinuity
predicate SequencePeak (u : Set, n : Nat) :=
  ∀ m ∈ ℕ, n < m → RealLe(u[m], u[n])

predicate UnboundedSequencePeaks (u : Set) :=
  ∀ N ∈ ℕ, ∃ n ∈ ℕ, N ≤ n ∧ SequencePeak(u, n)

predicate EventuallyNoSequencePeaks (u : Set, N : Nat) :=
  ∀ n ∈ ℕ, N ≤ n → ¬SequencePeak(u, n)

-- At stage zero we choose either a peak, or a point beyond which no peaks
-- remain.  Subsequent stages choose a later peak in the first case and a
-- later, strictly larger value in the second.
def monotoneStartCandidates (u : Set) : Set :=
  { n ∈ ℕ |
    (UnboundedSequencePeaks(u) ∧ SequencePeak(u, n)) ∨
    (¬UnboundedSequencePeaks(u) ∧ EventuallyNoSequencePeaks(u, n)) }

def monotoneNextCandidates (u k : Set) : Set :=
  { n ∈ ℕ | Less(k, n) ∧
    ((UnboundedSequencePeaks(u) ∧ SequencePeak(u, n)) ∨
     (¬UnboundedSequencePeaks(u) ∧ RealLess(u[k], u[n]))) }

theorem monotoneStartCandidates.naturals (u : Set)
  shows monotoneStartCandidates(u) ⊆ ℕ
proof
  simp

theorem monotoneNextCandidates.naturals (u k : Set)
  shows monotoneNextCandidates(u, k) ⊆ ℕ
proof
  simp

def monotoneIndex (u : Set, n : Nat) → Set
  | u, 0 => leastNatural(monotoneStartCandidates(u))
  | u, succ(n) => leastNatural(monotoneNextCandidates(u, monotoneIndex(u, n)))

def monotoneSelector (u : Set) : Set :=
  { p ∈ ℕ × ℕ | ∃ n ∈ ℕ, p = (n, monotoneIndex(u, n)) }

theorem not_unbounded_sequence_peaks.eventually_none (u : Set)
  requires bounded : ¬UnboundedSequencePeaks(u)
  shows ∃ N ∈ ℕ, EventuallyNoSequencePeaks(u, N)
proof
  by_contra noThreshold
  apply bounded
  intros N nNatural
  by_contra noLaterPeak
  apply noThreshold
  witness N
  constructor
  . exact nNatural
    intros n littleNatural afterN peak
    apply noLaterPeak
    witness n
    refine ⟨littleNatural, afterN, peak⟩

theorem UnboundedSequencePeaks.or_not (u : Set)
  shows UnboundedSequencePeaks(u) ∨ ¬UnboundedSequencePeaks(u)
proof
  tauto

theorem monotoneStartCandidates.nonempty (u : Set)
  shows Nonempty(monotoneStartCandidates(u))
proof
  have alternatives : UnboundedSequencePeaks(u) ∨ ¬UnboundedSequencePeaks(u) by tauto
  cases alternatives with unbounded | bounded
  . have unboundedPeaks := unbounded
    have zeroNatural : 0 ∈ ℕ by exact nat.omega.forward at 0 with Naturals.constructor.zero
    obtain ⟨n, nNatural, afterZero, peak⟩ :=
      unbounded with 0, zeroNatural
    witness n
    apply monotoneStartCandidates.membership.backward
    refine ⟨nNatural, _⟩
    left
    refine ⟨unboundedPeaks, peak⟩
  . obtain ⟨N, nNatural, noPeaks⟩ :=
      not_unbounded_sequence_peaks.eventually_none at u with bounded
    witness N
    apply monotoneStartCandidates.membership.backward
    refine ⟨nNatural, _⟩
    right
    refine ⟨bounded, noPeaks⟩

theorem EventuallyNoSequencePeaks.tail (u : Set, k m : Nat)
  requires none : EventuallyNoSequencePeaks(u, k)
  requires later : k ≤ m
  shows EventuallyNoSequencePeaks(u, m)
proof
  intros n nNatural afterM
  have afterK := LessEqual.transitive with later, afterM
  exact none with n, nNatural, afterK

theorem monotoneNextCandidates.nonempty (u : Set, k : Nat)
  requires sequence : RealSequence(u)
  requires position :
    (UnboundedSequencePeaks(u) ∧ SequencePeak(u, k)) ∨
    (¬UnboundedSequencePeaks(u) ∧ EventuallyNoSequencePeaks(u, k))
  shows Nonempty(monotoneNextCandidates(u, k))
proof
  cases position with peakCase | risingCase
  . rcases peakCase with ⟨unbounded, peak⟩
    have unboundedPeaks := unbounded
    have nextNatural := Naturals.constructor.succ at k
    have nextInNaturals := nat.omega.forward with nextNatural
    obtain ⟨n, nNatural, afterNext, laterPeak⟩ :=
      unbounded with succ(k), nextInNaturals
    have later : k < n by exact afterNext
    witness n
    apply monotoneNextCandidates.membership.backward
    refine ⟨nNatural, later, _⟩
    left
    refine ⟨unboundedPeaks, laterPeak⟩
  . rcases risingCase with ⟨bounded, noPeaks⟩
    have reflexive := LessEqual.reflexive at k
    have notPeak := noPeaks with k, reflexive
    have laterViolation : ∃ n ∈ ℕ, k < n ∧ ¬RealLe(u[n], u[k])
      by_contra noViolation
      apply notPeak
      intros m mNatural later
      by_contra notLe
      apply noViolation
      witness m
      refine ⟨mNatural, later, notLe⟩
    obtain ⟨next, nextNatural, later, notLe⟩ := laterViolation
    have realK := RealSequence.value with sequence
    have realNext := RealSequence.value with sequence
    have notOrdered : ¬(u[next] ≤ u[k])
      intro ordered
      apply notLe
      exact realLe.characterization.forward with ordered
    have rises := realLess.of_not_le with notOrdered
    have risesView := realLess.characterization.forward with rises
    witness next
    apply monotoneNextCandidates.membership.backward
    refine ⟨nextNatural, later, _⟩
    right
    refine ⟨bounded, risesView⟩

-- Every recursively chosen index is natural and remains in the branch chosen
-- at stage zero.  In the no-peaks branch it also remains beyond the threshold.
theorem monotoneIndex.position (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows Nat(monotoneIndex(u, n)) ∧
    ((UnboundedSequencePeaks(u) ∧
        SequencePeak(u, monotoneIndex(u, n))) ∨
     (¬UnboundedSequencePeaks(u) ∧
        EventuallyNoSequencePeaks(u, monotoneIndex(u, n))))
proof
  induction n
  | zero =>
    have inhabited := monotoneStartCandidates.nonempty at u
    have chosen := leastNatural.member with inhabited, monotoneStartCandidates.naturals at u
    have data := monotoneStartCandidates.membership.forward with chosen
    rw monotoneIndex
    rcases data with ⟨natural, position⟩
    have typed : Nat(leastNatural(monotoneStartCandidates(u))) by exact nat.omega.backward with natural
    constructor
    . exact typed
    . exact position
  | succ(j) using ih =>
    rcases ih with ⟨oldNatural, oldPosition⟩
    have inhabited := monotoneNextCandidates.nonempty with sequence, oldPosition
    have naturals := monotoneNextCandidates.naturals at u, monotoneIndex(u, j)
    have chosen := leastNatural.member with inhabited, naturals
    obtain ⟨natural, later, branch⟩ := monotoneNextCandidates.membership.forward with chosen
    have typed : Nat(leastNatural(monotoneNextCandidates(u, monotoneIndex(u, j))))
      exact nat.omega.backward with natural
    rw monotoneIndex
    constructor
    . exact typed
    . cases branch with peakBranch | risingBranch
      . left
        exact peakBranch
      . rcases risingBranch with ⟨bounded, rises⟩
        right
        constructor
        . exact bounded
        . cases oldPosition with oldPeak | oldRising
          . rcases oldPeak with ⟨unbounded, oldPeak⟩
            contradiction
          . rcases oldRising with ⟨boundedAgain, oldTail⟩
            have weak := Less.implies_LessEqual with oldNatural, later
            exact EventuallyNoSequencePeaks.tail with oldTail, weak

theorem monotoneIndex.natural (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows Nat(monotoneIndex(u, n))
proof
  have data := monotoneIndex.position with sequence
  simp

theorem monotoneIndex.step (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows Less(monotoneIndex(u, n), monotoneIndex(u, succ(n)))
proof
  obtain ⟨oldNatural, position⟩ := monotoneIndex.position with sequence
  have inhabited := monotoneNextCandidates.nonempty with sequence, position
  have naturals := monotoneNextCandidates.naturals at u, monotoneIndex(u, n)
  have chosen := leastNatural.member with inhabited, naturals
  obtain ⟨natural, later, branch⟩ := monotoneNextCandidates.membership.forward with chosen
  rwa monotoneIndex

theorem monotoneIndex.offset (u : Set, m k : Nat)
  requires sequence : RealSequence(u)
  shows LessEqual(monotoneIndex(u, m), monotoneIndex(u, m + k))
proof
  induction k
  | zero =>
    have shape := add.right_unit at m
    rw shape
    have indexNatural := monotoneIndex.natural with sequence
    exact LessEqual.reflexive with indexNatural
  | succ(j) using ih =>
    have step := monotoneIndex.step at u, m + j with sequence
    have weak := Less.implies_LessEqual with step
    have combined := LessEqual.transitive with ih, weak
    have shape := add.succ_right at j, m
    rwa shape

theorem monotoneIndex.monotone (u : Set, m n : Nat)
  requires sequence : RealSequence(u)
  requires order : m ≤ n
  shows LessEqual(monotoneIndex(u, m), monotoneIndex(u, n))
proof
  obtain ⟨k, kNatural, shape⟩ := order
  have offset := monotoneIndex.offset at u, m, k with sequence
  rwa shape at offset

theorem monotoneIndex.strict (u : Set, m n : Nat)
  requires sequence : RealSequence(u)
  requires order : m < n
  shows Less(monotoneIndex(u, m), monotoneIndex(u, n))
proof
  unfold Less at order
  have tail := monotoneIndex.monotone with sequence, order
  have first := monotoneIndex.step at u, m with sequence
  exact Less.transitive_LessEqual with first, tail

theorem monotoneSelector.relates (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows relates(monotoneSelector(u), n, monotoneIndex(u, n))
proof
  unfold relates
  have nInNaturals := nat.omega.forward at n with assumption
  have indexNatural := monotoneIndex.natural with sequence
  have indexInNaturals := nat.omega.forward with indexNatural
  apply monotoneSelector.membership.backward
  constructor
  . exact product.pair at n, monotoneIndex(u, n), ℕ, ℕ with
      nInNaturals, indexInNaturals
  . witness n
    refine ⟨nInNaturals, rfl⟩

theorem monotoneSelector.function (u : Set)
  requires sequence : RealSequence(u)
  shows monotoneSelector(u) : ℕ → ℕ
proof
  constructor
    intros p member
    have data := monotoneSelector.membership.forward with member
    simp
  . constructor
      intros n first mappedFirst second mappedSecond
      unfold relates at mappedFirst
      unfold relates at mappedSecond
      have firstData := monotoneSelector.membership.forward with mappedFirst
      have secondData := monotoneSelector.membership.forward with mappedSecond
      rcases firstData with ⟨_, i, iNatural, firstShape⟩
      rcases secondData with ⟨_, j, jNatural, secondShape⟩
      have firstCoordinates := orderedPair.injective with firstShape
      have secondCoordinates := orderedPair.injective with secondShape
      rcases firstCoordinates with ⟨nEqualsI, firstValue⟩
      rcases secondCoordinates with ⟨nEqualsJ, secondValue⟩
      rw ← nEqualsI at firstValue
      rw ← nEqualsJ at secondValue
      rw [firstValue, secondValue]
      rfl
    . intros n nNatural
      have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
      have indexNatural := monotoneIndex.natural with sequence
      have indexInNaturals := nat.omega.forward with indexNatural
      witness monotoneIndex(u, n)
      constructor
      . exact indexInNaturals
      . exact monotoneSelector.relates at u, n with sequence

theorem monotoneSelector.value (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows monotoneSelector(u)[n] = monotoneIndex(u, n)
proof
  have function := monotoneSelector.function with sequence
  have nNatural := nat.omega.forward at n with assumption
  have mapped := monotoneSelector.relates with sequence
  exact FunctionBetween.apply_value with function, nNatural, mapped

theorem monotoneSelector.strictly_increasing (u : Set)
  requires sequence : RealSequence(u)
  shows StrictlyIncreasingNat(monotoneSelector(u))
proof
  constructor
  . exact monotoneSelector.function with sequence
  . intros m mNatural n nNatural order
    have strict := monotoneIndex.strict with sequence, order
    have valueM := monotoneSelector.value at u, m with sequence
    have valueN := monotoneSelector.value at u, n with sequence
    rwa [valueM, valueN]

theorem monotoneIndex.rises_without_peaks (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  requires noUnbounded : ¬UnboundedSequencePeaks(u)
  shows RealLess(u[monotoneIndex(u, n)], u[monotoneIndex(u, succ(n))])
proof
  obtain ⟨oldNatural, oldPosition⟩ := monotoneIndex.position with sequence
  have inhabited := monotoneNextCandidates.nonempty with sequence, oldPosition
  have naturals := monotoneNextCandidates.naturals at u, monotoneIndex(u, n)
  have chosen := leastNatural.member with inhabited, naturals
  obtain ⟨nextNatural, later, branch⟩ := monotoneNextCandidates.membership.forward with chosen
  cases branch with peakBranch | risingBranch
  . rcases peakBranch with ⟨unbounded, peak⟩
    contradiction
  . rcases risingBranch with ⟨bounded, rises⟩
    rwa monotoneIndex

-- The selected values are monotone.  Arbitrarily late peaks give a
-- nonincreasing subsequence; once peaks cease, every chosen value rises.
theorem RealSequence.has_monotone_subsequence (u : Set)
  requires sequence : RealSequence(u)
  shows ∃ k, StrictlyIncreasingNat(k) ∧
    (Nondecreasing(subsequence(u, k)) ∨
     Nonincreasing(subsequence(u, k)))
proof
  witness monotoneSelector(u)
  constructor
  . exact monotoneSelector.strictly_increasing at u with sequence
  . have alternatives := UnboundedSequencePeaks.or_not at u
    cases alternatives with unbounded | noUnbounded
    . right
      have selectedSequence := subsequence.sequence at
        u, monotoneSelector(u) with
          sequence, monotoneSelector.strictly_increasing at u with sequence
      apply StepwiseNonincreasing.nonincreasing
      . exact selectedSequence
        intros n nNatural
        have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
        obtain ⟨currentNatural, position⟩ := monotoneIndex.position with sequence
        have peak : SequencePeak(u, monotoneIndex(u, n))
          cases position with peakBranch | risingBranch
          . settle
          . rcases risingBranch with ⟨bounded, tail⟩
            contradiction
        have nextIndexNatural := monotoneIndex.natural at u, succ(n) with sequence
        have nextIndexInNaturals := nat.omega.forward with nextIndexNatural
        have later := monotoneIndex.step at u, n with sequence
        have decreases := peak with
          monotoneIndex(u, succ(n)), nextIndexInNaturals, later
        have valueNow := subsequence.value at
          u, monotoneSelector(u), n with
            sequence, monotoneSelector.strictly_increasing at u with sequence
        have valueNext := subsequence.value at
          u, monotoneSelector(u), succ(n) with
            sequence, monotoneSelector.strictly_increasing at u with sequence
        have selectorNow := monotoneSelector.value at u, n with sequence
        have selectorNext := monotoneSelector.value at u, succ(n) with sequence
        rwa [valueNow, valueNext, selectorNow, selectorNext]
    . left
      have selectedSequence := subsequence.sequence at
        u, monotoneSelector(u) with
          sequence, monotoneSelector.strictly_increasing at u with sequence
      apply StepwiseNondecreasing.nondecreasing
      . exact selectedSequence
        intros n nNatural
        have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
        have risesView := monotoneIndex.rises_without_peaks with sequence, noUnbounded
        have rises := realLess.characterization.backward with risesView
        have weak := realLess.implies_le with rises
        have weakView := realLe.characterization.forward with weak
        have valueNow := subsequence.value at
          u, monotoneSelector(u), n with
            sequence, monotoneSelector.strictly_increasing at u with sequence
        have valueNext := subsequence.value at
          u, monotoneSelector(u), succ(n) with
            sequence, monotoneSelector.strictly_increasing at u with sequence
        have selectorNow := monotoneSelector.value with sequence
        have selectorNext := monotoneSelector.value at u, succ(n) with sequence
        rwa [valueNow, valueNext, selectorNow, selectorNext]

theorem TermsIn.closedInterval_bounded_above (u : Set) (A B : Real)
  requires terms : TermsIn(u, closedInterval(A, B))
  shows BoundedAboveBy(u, B)
proof
  intros n nNatural
  have member := terms with n, nNatural
  have data := closedInterval.membership.forward with member
  simp [RealLe, realLe.characterization]

theorem TermsIn.closedInterval_bounded_below (u : Set) (A B : Real)
  requires terms : TermsIn(u, closedInterval(A, B))
  shows BoundedBelowBy(u, A)
proof
  intros n nNatural
  have member := terms with n, nNatural
  have data := closedInterval.membership.forward with member
  simp [RealLe, realLe.characterization]

-- Bolzano-Weierstrass for a sequence in a closed interval.  The proof first
-- extracts a monotone subsequence, then invokes the appropriate half of the
-- monotone convergence theorem.
theorem closedInterval.bolzano_weierstrass (u : Set) (A B : Real)
  requires sequence : RealSequence(u)
  requires terms : TermsIn(u, closedInterval(A, B))
  shows ∃ k, StrictlyIncreasingNat(k) ∧
    ∃ L ∈ ℝ, L ∈ closedInterval(A, B) ∧
      ConvergesTo(subsequence(u, k), L)
proof
  obtain ⟨k, increasing, monotone⟩ := RealSequence.has_monotone_subsequence with sequence
  have selectedSequence := subsequence.sequence with sequence, increasing
  have selectedTerms := TermsIn.subsequence with sequence, terms, increasing
  witness k
  constructor
  . exact increasing
  . cases monotone with nondecreasing | nonincreasing
    . have boundedAbove := TermsIn.closedInterval_bounded_above at
        subsequence(u, k), A, B with selectedTerms
      have converges := Nondecreasing.converges_to_supremum with selectedSequence, nondecreasing, boundedAbove
      have inhabited := RealSequence.range_nonempty with selectedSequence
      have rangeUpper := BoundedAboveBy.range_upper_bound with selectedSequence, boundedAbove
      have least := realSup.least_upper_bound with inhabited, rangeUpper
      have supUpper : RealUpperBound(
          range(subsequence(u, k)), realSup(range(subsequence(u, k))))
        simp [RealLeastUpperBound]
      rcases supUpper with ⟨limitReal, rangeReals, bounds⟩
      witness realSup(range(subsequence(u, k)))
      constructor
        exact limitReal
      . constructor
        . exact closedInterval.contains_subsequence_limit at
            u, k, realSup(range(subsequence(u, k))), A, B with
              sequence, terms, increasing, converges
        . exact converges
    . have boundedBelow := TermsIn.closedInterval_bounded_below at
        subsequence(u, k), A, B with selectedTerms
      obtain ⟨L, realL, converges⟩ := Nonincreasing.has_limit with
        selectedSequence, nonincreasing, boundedBelow
      witness L
      constructor
      . exact realL
      . constructor
        . exact closedInterval.contains_subsequence_limit at
            u, k, L, A, B with
              sequence, terms, increasing, converges
        . exact converges

theorem closedInterval.sequentially_compact (A B : Real)
  shows SequentiallyCompact(closedInterval(A, B))
proof
  constructor
  . exact closedInterval.subset_reals with *{2}
  . intros u sequence terms
    exact closedInterval.bolzano_weierstrass with sequence, terms

-- CompactContinuity
theorem ContinuousWithinAt.converges_in (f u S : Set) (L : Real)
  requires continuous : ContinuousWithinAt(f, S, L)
  requires converges : ConvergesTo(u, L)
  requires terms : TermsIn(u, S)
  shows ConvergesTo(compose(f, u, ℕ, ℝ, ℝ), f(L))
proof
  rcases continuous with ⟨function, subset, control⟩
  have sequence := ConvergesTo.sequence with converges
  unfold RealSequence at sequence
  have realL : L ∈ ℝ by simp [Real]
  have fLReal := FunctionBetween.apply_closed with function
  constructor
  . unfold RealSequence
    exact compose.function with sequence, function
  . intros E realE positive
    obtain ⟨D, realD, positiveD, maps⟩ :=
      control with E, realE, positive
    obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, positiveD
    witness N
    constructor
    . exact naturalN
    . intros n indexNatural nAfterN
      have unReal := FunctionBetween.apply_closed with sequence, indexNatural
      have member := terms
      have inS := member with n, indexNatural
      have near := close with n, indexNatural, nAfterN
      have mapped := maps with u(n), unReal, inS, near
      have value := compose.apply with sequence, function, indexNatural
      rwa value

theorem ContinuousOn.converges_in (f u S : Set) (L : Real)
  requires continuous : ContinuousOn(f, S)
  requires limitMember : L ∈ S
  requires converges : ConvergesTo(u, L)
  requires terms : TermsIn(u, S)
  shows ConvergesTo(compose(f, u, ℕ, ℝ, ℝ), f(L))
proof
  rcases continuous with ⟨function, subset, atEveryPoint⟩
  have atLimit := atEveryPoint with L, limitMember
  exact ContinuousWithinAt.converges_in with atLimit, converges, terms

-- Compactness supplies the convergent input subsequence; relative continuity
-- transfers its limit through f, including when the limit is an endpoint.
theorem ContinuousOn.compact_subsequence (f u S : Set)
  requires continuous : ContinuousOn(f, S)
  requires compact : SequentiallyCompact(S)
  requires sequence : RealSequence(u)
  requires terms : TermsIn(u, S)
  shows ∃ k, StrictlyIncreasingNat(k) ∧
    ∃ L ∈ ℝ, L ∈ S ∧
      ConvergesTo(compose(f, subsequence(u, k), ℕ, ℝ, ℝ), f(L))
proof
  rcases compact with ⟨subset, extract⟩
  obtain ⟨k, increasing, L, realL, member, converges⟩ :=
    extract with u, sequence, terms
  have selected := TermsIn.subsequence with sequence, terms, increasing
  have mapped := ContinuousOn.converges_in with continuous, member, converges, selected
  witness k
  constructor
  . exact increasing
  . witness L
    refine ⟨realL, member, mapped⟩

theorem closedInterval.continuous_subsequence (f u : Set) (A B : Real)
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires sequence : RealSequence(u)
  requires terms : TermsIn(u, closedInterval(A, B))
  shows ∃ k, StrictlyIncreasingNat(k) ∧
    ∃ L ∈ ℝ, L ∈ closedInterval(A, B) ∧
      ConvergesTo(compose(f, subsequence(u, k), ℕ, ℝ, ℝ), f(L))
proof
  have compact := closedInterval.sequentially_compact at A, B with
    *{2}
  exact ContinuousOn.compact_subsequence with continuous, compact, sequence, terms