-- Real analysis: MeanValueIntegration
-- 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.MeanValueIntegration
import Differentiation
import Intervals
import ExtremeValue
import Continuity
import Integration.CommonRefinementComparison
import Integration.IntegralOrderBound

-- Section: MeanValueCorrectionDerivative
def meanValueCorrection (F : Set) (A B : Real) : Set :=
  pointwiseSub(
    pointwiseMul(constantRealFunction(realSubValue(B, A)), F),
    pointwiseMul(constantRealFunction(realSubValue(F(B), F(A))), identity(ℝ)))

theorem meanValueCorrection.continuous_on (F : Set) (A B : Real)
  requires continuous : ContinuousOn(F, closedInterval(A, B))
  shows ContinuousOn(meanValueCorrection(F, A, B), closedInterval(A, B))
proof
  have function : F : ℝ → ℝ
    rcases continuous with ⟨graph, subset, everywhere⟩
    exact graph
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have valueA := FunctionBetween.apply_closed with function, realA
  have valueB := FunctionBetween.apply_closed with function, realB
  have typedFA : Real(F(A)) by exact valueA
  have typedFB : Real(F(B)) by exact valueB
  have widthReal : Real(B - A)
    exact realSubValue.real with *
  have deltaReal : Real(F(B) - F(A)) by exact realSubValue.real at F(B), F(A) with typedFB, typedFA
  have subset := closedInterval.subset_reals at A, B with *
  have constantWidth := Continuous.continuous_on at
    constantRealFunction(B - A), closedInterval(A, B) with
      constantRealFunction.continuous at B - A with widthReal, subset
  have first := ContinuousOn.mul with constantWidth, continuous
  have linear := Continuous.mul at
    constantRealFunction(F(B) - F(A)), identity(ℝ) with
      constantRealFunction.continuous at
        F(B) - F(A) with deltaReal,
      identity.continuous
  have negLinear := Continuous.neg with linear
  have second := Continuous.continuous_on at
    pointwiseNeg(pointwiseMul(
      constantRealFunction(F(B) - F(A)), identity(ℝ))),
    closedInterval(A, B) with negLinear, subset
  unfold meanValueCorrection
  unfold pointwiseSub
  exact ContinuousOn.add at
    pointwiseMul(constantRealFunction(B - A), F),
    pointwiseNeg(pointwiseMul(
      constantRealFunction(F(B) - F(A)), identity(ℝ))),
    closedInterval(A, B) with first, second

-- MeanValueCorrectionValues
theorem meanValueCorrection.value (F : Set) (A B X : Real)
  requires function : F : ℝ → ℝ
  shows meanValueCorrection(F, A, B)(X) =
    (B - A) * F(X) - (F(B) - F(A)) * X
proof
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have realX : X ∈ ℝ by simp [Real]
  have fA := FunctionBetween.apply_closed with function, realA
  have fB := FunctionBetween.apply_closed with function, realB
  have fX := FunctionBetween.apply_closed with function, realX
  have typedFA : Real(F(A)) by exact fA
  have typedFB : Real(F(B)) by exact fB
  have typedFX : Real(F(X)) by exact fX
  have typedWidth := realSubValue.real at B, A with *
  have typedDelta := realSubValue.real with typedFB, typedFA
  have widthFunction := constantRealFunction.function with typedWidth
  have deltaFunction := constantRealFunction.function with typedDelta
  have identityFunction := identity.function at ℝ
  have leftFunction := pointwiseMul.function with widthFunction, function
  have rightFunction := pointwiseMul.function with deltaFunction, identityFunction
  have widthX := FunctionBetween.apply_closed with widthFunction, realX
  have deltaX := FunctionBetween.apply_closed with deltaFunction, realX
  have identityX := FunctionBetween.apply_closed with identityFunction, realX
  have typedWidthX : Real(constantRealFunction(B - A)(X)) by exact widthX
  have typedDeltaX : Real(constantRealFunction(F(B) - F(A))(X)) by exact deltaX
  have typedIdentityX : Real(identity(ℝ)(X)) by exact identityX
  have leftValue := pointwiseMul.value at
    constantRealFunction(B - A), F, X with
      assumption, widthFunction, function, typedWidthX, typedFX
  have rightValue := pointwiseMul.value at
    constantRealFunction(F(B) - F(A)), identity(ℝ), X with
      assumption, deltaFunction, identityFunction, typedDeltaX, typedIdentityX
  have leftReal := FunctionBetween.apply_closed with leftFunction, realX
  have rightReal := FunctionBetween.apply_closed with rightFunction, realX
  have typedLeft : Real(pointwiseMul(constantRealFunction(B - A), F)(X)) by exact leftReal
  have typedRight : Real(pointwiseMul(constantRealFunction(F(B) - F(A)), identity(ℝ))(X)) by exact rightReal
  have subtraction := pointwiseSub.value at
    pointwiseMul(constantRealFunction(B - A), F),
    pointwiseMul(constantRealFunction(F(B) - F(A)), identity(ℝ)),
    X with assumption, leftFunction, rightFunction, typedLeft, typedRight
  have widthValue := constantRealFunction.value at B - A, X with typedWidth, assumption
  have deltaValue := constantRealFunction.value at
    F(B) - F(A), X with typedDelta, assumption
  have identityValue := identity.apply with realX
  have equality : meanValueCorrection(F, A, B)(X) =
      pointwiseMul(constantRealFunction(B - A), F)(X) -
        pointwiseMul(constantRealFunction(F(B) - F(A)), identity(ℝ))(X)
    simp [meanValueCorrection]
  rwa [leftValue, rightValue, widthValue, deltaValue, identityValue] at equality

theorem meanValueCorrection.endpoints (F : Set) (A B : Real)
  requires function : F : ℝ → ℝ
  shows meanValueCorrection(F, A, B)(A) =
    meanValueCorrection(F, A, B)(B)
proof
  have atA := meanValueCorrection.value at F, A, B, A with function
  have atB := meanValueCorrection.value at F, A, B, B with function
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have fA := FunctionBetween.apply_closed with function, realA
  have fB := FunctionBetween.apply_closed with function, realB
  rw [atA, atB]
  ring

-- MeanValueCorrectionDerivative
theorem meanValueCorrection.derivative (F : Set) (A B C D : Real)
  requires derivative : HasDerivativeAt(F, D, C)
  shows HasDerivativeAt(meanValueCorrection(F, A, B), (B - A) * D - ((F(B):R) - (F(A):R)), C)
proof
  have function := HasDerivativeAt.function with derivative
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have valueA := FunctionBetween.apply_closed with function, realA
  have valueB := FunctionBetween.apply_closed with function, realB
  have typedFA : Real(F(A)) by exact valueA
  have typedFB : Real(F(B)) by exact valueB
  have widthReal := realSubValue.real at B, A with *
  have deltaReal := realSubValue.real with typedFB, typedFA
  have constantWidth := constantRealFunction.has_derivative_at at B - A, C with
    widthReal, assumption
  have constantDelta := constantRealFunction.has_derivative_at at
    F(B) - F(A), C with deltaReal, assumption
  have identityDerivative := identity.has_derivative_at at C
  have first := HasDerivativeAt.mul with realZero.real, constantWidth, derivative
  have second := HasDerivativeAt.mul with realZero.real, realOne.real, constantDelta, identityDerivative
  have realC : C ∈ ℝ by simp [Real]
  have fC := FunctionBetween.apply_closed with function, realC
  have typedFC : Real(F(C)) by exact fC
  have widthC := FunctionBetween.apply_closed at
    constantRealFunction(B - A), ℝ, ℝ, C with
      constantRealFunction.function at B - A with widthReal, realC
  have deltaC := FunctionBetween.apply_closed at
    constantRealFunction(F(B) - F(A)), ℝ, ℝ, C with
      constantRealFunction.function at F(B) - F(A) with deltaReal, realC
  have idC := FunctionBetween.apply_closed at identity(ℝ), ℝ, ℝ, C with
    identity.function at ℝ, realC
  have typedWidthC : Real(constantRealFunction(B - A)(C)) by exact widthC
  have typedDeltaC : Real(constantRealFunction(F(B) - F(A))(C)) by exact deltaC
  have typedIdC : Real(identity(ℝ)(C)) by exact idC
  have productZeroF := realMulValue.real with realZero.real, typedFC
  have productWidth := realMulValue.real at constantRealFunction(B - A)(C), D with typedWidthC, assumption
  have productZeroId := realMulValue.real with realZero.real, typedIdC
  have productDelta := realMulValue.real with typedDeltaC, realOne.real
  have raw := HasDerivativeAt.sub with first, second
  have widthValue := constantRealFunction.value at B - A, C with widthReal, assumption
  have deltaValue := constantRealFunction.value at
    F(B) - F(A), C with deltaReal, assumption
  have result : (realZero * F(C) + constantRealFunction(B - A)(C) * D) -
    (realZero * identity(ℝ)(C) +
      constantRealFunction(F(B) - F(A))(C) * realOne) =
      (B - A) * D - (F(B) - F(A))
    rw [widthValue, deltaValue]
    ring
  have view : realSubValue(
      realAddValue(realMulValue(realZero, F(C)),
        realMulValue(constantRealFunction(B - A)(C), D)),
      realAddValue(realMulValue(realZero, identity(ℝ)(C)),
        realMulValue(constantRealFunction(F(B) - F(A))(C), realOne))) =
      (realZero * F(C) + constantRealFunction(B - A)(C) * D) -
      (realZero * identity(ℝ)(C) +
        constantRealFunction(F(B) - F(A))(C) * realOne)
    unfold realSubValue
    unfold realAddValue
    unfold realMulValue
    unfold call2
    rfl
  unfold meanValueCorrection
  rwa [view, result] at raw

-- Section: InteriorSteps
theorem differenceQuotient.positive_increment (f : Set) (C H : Real)
  requires function : f : ℝ → ℝ
  requires positiveH : 0 < H
  requires positiveQ : 0 < (differenceQuotient(f, C)(H):R)
  shows 0 < f(C + H) - f(C)
proof
  have realCPlusH := realAddValue.real at C, H with *
  have memberCPlusH : C + H ∈ ℝ by exact realCPlusH
  have memberC : C ∈ ℝ by simp [Real]
  have valueCPlusH := FunctionBetween.apply_closed with function, memberCPlusH
  have valueC := FunctionBetween.apply_closed with function, memberC
  have realValueCPlusH : Real(f(C + H)) by exact valueCPlusH
  have realValueC : Real(f(C)) by exact valueC
  have realIncrement := realSubValue.real with realValueCPlusH, realValueC
  have realQ := differenceQuotient.function at f, C with function
  have memberH : H ∈ ℝ by simp [Real]
  have valueQ := FunctionBetween.apply_closed with realQ, memberH
  have nonzero : H ≠ 0
    intro equal
    rw equal at positiveH
    have impossible := realLess.characterization.forward with positiveH
    exact RealLess.irreflexive with impossible
  have quotient := differenceQuotient.value at f, C, H with function
  have cancels := realDiv.mul_right with realIncrement, assumption, nonzero
  rw ← quotient at cancels
  have product := realMulValue.positive with positiveQ, positiveH
  rwa cancels at product

theorem differenceQuotient.negative_step_positive_increment (f : Set) (C H : Real)
  requires function : f : ℝ → ℝ
  requires negativeH : H < 0
  requires negativeQ : (differenceQuotient(f, C)(H):R) < 0
  shows 0 < f(C + H) - f(C)
proof
  have realCPlusH := realAddValue.real at C, H with *
  have memberCPlusH : C + H ∈ ℝ by exact realCPlusH
  have memberC : C ∈ ℝ by simp [Real]
  have valueCPlusH := FunctionBetween.apply_closed with function, memberCPlusH
  have valueC := FunctionBetween.apply_closed with function, memberC
  have realValueCPlusH : Real(f(C + H)) by exact valueCPlusH
  have realValueC : Real(f(C)) by exact valueC
  have realIncrement := realSubValue.real with realValueCPlusH, realValueC
  have realQ := differenceQuotient.function at f, C with function
  have memberH : H ∈ ℝ by simp [Real]
  have valueQ := FunctionBetween.apply_closed with realQ, memberH
  have typedQ : Real(differenceQuotient(f, C)(H)) by exact valueQ
  have nonzero : H ≠ 0
    intro equal
    rw equal at negativeH
    have impossible := realLess.characterization.forward with negativeH
    exact RealLess.irreflexive with impossible
  have quotient := differenceQuotient.value at f, C, H with function
  have cancels := realDiv.mul_right with realIncrement, assumption, nonzero
  rw ← quotient at cancels
  have negativeQView := realLess.characterization.forward with negativeQ
  have negativeHView := realLess.characterization.forward with negativeH
  have positiveNegQView := RealLess.neg_reverse with negativeQView
  have positiveNegHView := RealLess.neg_reverse with negativeHView
  have positiveNegQ := realLess.characterization.backward with positiveNegQView
  have positiveNegH := realLess.characterization.backward with positiveNegHView
  rw realNegValue.zero at positiveNegQ
  rw realNegValue.zero at positiveNegH
  have positiveProduct := realMulValue.positive at
    -differenceQuotient(f, C)(H), -H with
      realNegValue.real at differenceQuotient(f, C)(H) with typedQ,
      realNegValue.real at H with assumption,
      positiveNegQ, positiveNegH
  have sameProduct : (-differenceQuotient(f, C)(H)) * (-H) =
      differenceQuotient(f, C)(H) * H
    ring
  rwa [sameProduct, cancels] at positiveProduct

-- InteriorSteps
theorem closedInterval.right_step (A C B H : Real)
  requires left : A < C
  requires positive : 0 < H
  requires small : H < B - C
  shows C + H ∈ closedInterval(A, B)
proof
  have pointReal := realAddValue.real at C, H with *
  have pointMember : C + H ∈ ℝ by exact pointReal
  have aboveC := realLess.add_left at realZero, H, C with
    realZero.real, *{2}, positive
  have zero := realAddValue.zero_right at C
  rw zero at aboveC
  have lowerStrict : A < C + H
    exact realLess.transitive at A, C, C + H with
      *{2}, pointReal, left, aboveC
  have widthReal := realSubValue.real at B, C with *
  have shifted := realLess.add_right at H, B - C, C with
    assumption, widthReal, assumption, small
  have cancel := realSubValue.add_right_cancel at B, C with
    *{2}
  rw cancel at shifted
  have commute := realAddValue.commutative at H, C with *
  rw commute at shifted
  have upperStrict : C + H < B by exact shifted
  have lower := realLess.implies_le with lowerStrict
  have upper := realLess.implies_le with upperStrict
  apply closedInterval.membership.backward
  refine ⟨pointMember, lower, upper⟩

theorem closedInterval.left_step (A C B H : Real)
  requires right : C < B
  requires positive : 0 < H
  requires small : H < C - A
  shows C - H ∈ closedInterval(A, B)
proof
  have pointReal := realSubValue.real at C, H with *
  have pointMember : C - H ∈ ℝ by exact pointReal
  have widthReal := realSubValue.real at C, A with *
  have shifted := realLess.add_right at H, C - A, A with
    assumption, widthReal, assumption, small
  have cancel := realSubValue.add_right_cancel at C, A with
    *{2}
  rw cancel at shifted
  have shiftBack := realLess.add_right_iff.forward at
    A, C - H, H with
      assumption, pointReal, assumption
  have lowerStrict : A < C - H
    have same : A + H = H + A by ring
    have cancelH : (C - H) + H = C by ring
    rw [← same, ← cancelH] at shifted
    exact shiftBack with shifted
  have negativeView := realLess.characterization.forward with positive
  have reversed := RealLess.neg_reverse with negativeView
  have negative := realLess.characterization.backward with reversed
  rw realNegValue.zero at negative
  have belowC := realLess.add_left at -H, realZero, C with
    realNegValue.real at H with assumption, realZero.real, assumption,
    negative
  have zero := realAddValue.zero_right at C
  rw zero at belowC
  have belowCSub : C - H < C
    unfold realSubValue
    exact belowC
  have upperStrict : C - H < B by exact realLess.transitive with belowCSub, right
  have lower := realLess.implies_le with lowerStrict
  have upper := realLess.implies_le with upperStrict
  apply closedInterval.membership.backward
  refine ⟨pointMember, lower, upper⟩

-- Section: IntervalInterior
theorem Real.exists_small_positive (E W : Real)
  requires positiveE : 0 < E
  requires positiveW : 0 < W
  shows ∃ H ∈ ℝ, 0 < H ∧ H < E ∧ H < W
proof
  obtain ⟨N, naturalN, near⟩ := ConvergesTo.common_eventually with
    dyadicRadii.converges_zero, dyadicRadii.converges_zero, positiveE, positiveW
  have typedN := nat.omega.backward with naturalN
  have close := near with N, naturalN,
    LessEqual.reflexive with typedN
  rcases close with ⟨nearE, nearW⟩
  have value := dyadicRadii.value with typedN
  rw value at nearE
  rw value at nearW
  have first := openBall.order_characterization.forward with nearE
  have second := openBall.order_characterization.forward with nearW
  rcases first with ⟨lowerE, upperE⟩
  rcases second with ⟨lowerW, upperW⟩
  have zeroE := realAddValue.zero_left at E
  have zeroW := realAddValue.zero_left at W
  rw zeroE at upperE
  rw zeroW at upperW
  have realH := dyadicRadius.real with typedN
  witness dyadicRadius(N)
  constructor
    exact realH
  . refine ⟨dyadicRadius.positive at N with typedN, upperE, upperW⟩

theorem Real.small_positive_in_ball (H E : Real)
  requires positive : 0 < H
  requires below : H < E
  shows H ∈ openBall(realZero, E)
proof
  have positiveE := realLess.transitive with realZero.real, positive, below
  have negativeE := realLess.characterization.forward with positiveE
  have reversed := RealLess.neg_reverse with negativeE
  have negative := realLess.characterization.backward with reversed
  rw realNegValue.zero at negative
  have lower := realLess.transitive at -E, realZero, H with
    realNegValue.real at E with assumption, realZero.real, assumption,
    negative, positive
  have zeroMinus := realSubValue.zero_left at E
  have zeroPlus := realAddValue.zero_left at E
  rw ← zeroMinus at lower
  rw ← zeroPlus at below
  apply openBall.order_characterization.backward with realZero.real
  refine ⟨lower, below⟩

theorem Real.small_negative_in_ball (H E : Real)
  requires positive : 0 < H
  requires below : H < E
  shows -H ∈ openBall(realZero, E)
proof
  have negativeHView := realLess.characterization.forward with positive
  have reversedH := RealLess.neg_reverse with negativeHView
  have negativeH := realLess.characterization.backward with reversedH
  rw realNegValue.zero at negativeH
  have positiveE := realLess.transitive with realZero.real, positive, below
  have upper := realLess.transitive at -H, realZero, E with
    realNegValue.real at H with assumption, realZero.real, assumption,
    negativeH, positiveE
  have belowView := realLess.characterization.forward with below
  have reversed := RealLess.neg_reverse with belowView
  have lower := realLess.characterization.backward with reversed
  have zeroMinus := realSubValue.zero_left at E
  have zeroPlus := realAddValue.zero_left at E
  rw ← zeroMinus at lower
  rw ← zeroPlus at upper
  apply openBall.order_characterization.backward at -H, realZero, E with
    realNegValue.real at H with assumption, realZero.real, assumption
  refine ⟨lower, upper⟩

-- PuncturedSign
theorem TendsToAt.eventually_positive (f : Set) (D A : Real)
  requires limit : TendsToAt(f, D, A)
  requires positive : 0 < D
  shows ∃ E ∈ ℝ, 0 < E ∧
    (∀ H ∈ ℝ, H ≠ A → H ∈ openBall(A, E) → (0:R) < (f(H):R))
proof
  obtain ⟨E, realE, positiveE, near⟩ := TendsToAt.eventually with limit, positive
  witness E
  constructor
  . exact realE
  . constructor
    . exact positiveE
    . intros H realH nonzero close
      have image := near with H, realH, nonzero, close
      have function := TendsToAt.function with limit
      have imageReal := FunctionBetween.apply_closed with function, realH
      obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with image
      have self := realSubValue.self at D
      rwa self at lower

theorem TendsToAt.eventually_negative (f : Set) (D A : Real)
  requires limit : TendsToAt(f, D, A)
  requires negative : D < 0
  shows ∃ E ∈ ℝ, 0 < E ∧
    (∀ H ∈ ℝ, H ≠ A → H ∈ openBall(A, E) → (f(H):R) < (0:R))
proof
  have negativeView := realLess.characterization.forward with negative
  have reversed := RealLess.neg_reverse with negativeView
  have positiveNeg := realLess.characterization.backward with reversed
  rw realNegValue.zero at positiveNeg
  obtain ⟨E, realE, positiveE, near⟩ := TendsToAt.eventually with limit, positiveNeg
  witness E
  constructor
  . exact realE
  . constructor
    . exact positiveE
    . intros H realH nonzero close
      have image := near with H, realH, nonzero, close
      have function := TendsToAt.function with limit
      have imageReal := FunctionBetween.apply_closed with function, realH
      obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with image
      have cancel := realAddValue.neg_right at D
      rwa cancel at upper

-- Fermat
theorem HasDerivativeAt.not_positive_at_interval_max (f : Set) (A C B D : Real)
  requires left : A < C
  requires right : C < B
  requires derivative : HasDerivativeAt(f, D, C)
  requires maximal : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(C):R)
  shows ¬(0 < D)
proof
  intro positiveD
  have function := HasDerivativeAt.function with derivative
  have limit := HasDerivativeAt.limit with derivative
  obtain ⟨E, realE, positiveE, sign⟩ := TendsToAt.eventually_positive with limit, positiveD
  have width := realLess.iff_pos_sub.forward with right
  obtain ⟨H, realH, positiveH, belowE, belowWidth⟩ := Real.exists_small_positive with positiveE, width
  have typedH : Real(H) by exact realH
  have near := Real.small_positive_in_ball with positiveH, belowE
  have nonzero : H ≠ realZero
    intro equal
    rw equal at positiveH
    have impossible := realLess.characterization.forward with positiveH
    exact RealLess.irreflexive with impossible
  have positiveQ := sign with H, realH, nonzero, near
  have member := closedInterval.right_step with left, positiveH, belowWidth
  have increment := differenceQuotient.positive_increment with function, positiveH, positiveQ
  have realC : C ∈ ℝ by simp [Real]
  have realNext : C + H ∈ ℝ by exact realAddValue.real at C, H with assumption, typedH
  have valueC := FunctionBetween.apply_closed with function, realC
  have valueNext := FunctionBetween.apply_closed with function, realNext
  have strict := realLess.iff_pos_sub.backward with increment
  have bound := maximal with C + H, member
  have cycle := realLess.transitive_le with strict, bound
  have impossible := realLess.characterization.forward with cycle
  exact RealLess.irreflexive with impossible

theorem HasDerivativeAt.not_negative_at_interval_max (f : Set) (A C B D : Real)
  requires left : A < C
  requires right : C < B
  requires derivative : HasDerivativeAt(f, D, C)
  requires maximal : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(C):R)
  shows ¬(D < 0)
proof
  intro negativeD
  have function := HasDerivativeAt.function with derivative
  have limit := HasDerivativeAt.limit with derivative
  obtain ⟨E, realE, positiveE, sign⟩ := TendsToAt.eventually_negative with limit, negativeD
  have width := realLess.iff_pos_sub.forward with left
  obtain ⟨H, realH, positiveH, belowE, belowWidth⟩ := Real.exists_small_positive with positiveE, width
  have typedH : Real(H) by exact realH
  have near := Real.small_negative_in_ball with positiveH, belowE
  have negativeHView := realLess.characterization.forward with positiveH
  have reversed := RealLess.neg_reverse with negativeHView
  have negativeH := realLess.characterization.backward with reversed
  rw realNegValue.zero at negativeH
  have nonzero : -H ≠ realZero
    intro equal
    rw equal at negativeH
    have impossible := realLess.characterization.forward with negativeH
    exact RealLess.irreflexive with impossible
  have negativeQ := sign with -H, nonzero, near
  have member := closedInterval.left_step with right, positiveH, belowWidth
  have increment := differenceQuotient.negative_step_positive_increment with function, negativeH, negativeQ
  have shape : C + (-H) = C - H by ring
  rw shape at increment
  have realC : C ∈ ℝ by simp [Real]
  have realPrevious : C - H ∈ ℝ by exact realSubValue.real at C, H with assumption, typedH
  have valueC := FunctionBetween.apply_closed with function, realC
  have valuePrevious := FunctionBetween.apply_closed with function, realPrevious
  have strict := realLess.iff_pos_sub.backward with increment
  have bound := maximal with C - H, member
  have cycle := realLess.transitive_le with strict, bound
  have impossible := realLess.characterization.forward with cycle
  exact RealLess.irreflexive with impossible

theorem HasDerivativeAt.zero_at_interval_max (f : Set) (A C B D : Real)
  requires left : A < C
  requires right : C < B
  requires derivative : HasDerivativeAt(f, D, C)
  requires maximal : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(C):R)
  shows D = 0
proof
  have notPositive := HasDerivativeAt.not_positive_at_interval_max with left, right, derivative, maximal
  have notNegative := HasDerivativeAt.not_negative_at_interval_max with left, right, derivative, maximal
  have upper : D ≤ realZero
    by_contra notUpper
    have positive := realLess.of_not_le with notUpper
    exact notPositive with positive
  have lower : realZero ≤ D
    by_contra notLower
    have negative := realLess.of_not_le with notLower
    exact notNegative with negative
  have upperView := realLe.characterization.forward with upper
  have lowerView := realLe.characterization.forward with lower
  exact RealLe.antisymmetric with upperView, lowerView

theorem HasDerivativeAt.zero_at_interval_min (f : Set) (A C B D : Real)
  requires left : A < C
  requires right : C < B
  requires derivative : HasDerivativeAt(f, D, C)
  requires minimal : ∀ X ∈ closedInterval(A, B),
    (f(C):R) ≤ (f(X):R)
  shows D = 0
proof
  have function := HasDerivativeAt.function with derivative
  have negDerivative := HasDerivativeAt.neg with derivative
  have negMax : ∀ X ∈ closedInterval(A, B),
      (pointwiseNeg(f)(X):R) ≤ (pointwiseNeg(f)(C):R)
    intros X member
    have inReals := closedInterval.subset_reals at A, B with
      *{2}
    have realXMember := inReals with X, member
    have typedX : Real(X) by exact realXMember
    have valueX := FunctionBetween.apply_closed with function, realXMember
    have realCMember : C ∈ ℝ by simp [Real]
    have valueC := FunctionBetween.apply_closed with function, realCMember
    have typedValueX : Real(f(X)) by exact valueX
    have typedValueC : Real(f(C)) by exact valueC
    have lower := minimal with X, member
    have reversed := realLe.neg_reverse with lower
    have negX := pointwiseNeg.value with typedX, function, typedValueX
    have negC := pointwiseNeg.value at f, C with
      assumption, function, typedValueC
    rwa [negX, negC]
  have zeroNeg := HasDerivativeAt.zero_at_interval_max at
    pointwiseNeg(f), A, C, B, -D with
      realNegValue.real at D with assumption,
      left, right, negDerivative, negMax
  have involutive := realNegValue.involutive at D
  rw [← involutive, zeroNeg]
  exact realNegValue.zero

-- IntervalInterior
theorem closedInterval.left_lt_of_ne (A B T : Real)
  requires member : T ∈ closedInterval(A, B)
  requires distinct : T ≠ A
  shows A < T
proof
  obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with member
  have notReverse : ¬(T ≤ A)
    intro reverse
    have first := realLe.characterization.forward with lower
    have second := realLe.characterization.forward with reverse
    have equal := RealLe.antisymmetric with first, second
    apply distinct
    rw equal
    rfl
  exact realLess.of_not_le with notReverse

theorem closedInterval.right_lt_of_ne (A B T : Real)
  requires member : T ∈ closedInterval(A, B)
  requires distinct : T ≠ B
  shows T < B
proof
  obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with member
  have notReverse : ¬(B ≤ T)
    intro reverse
    have first := realLe.characterization.forward with upper
    have second := realLe.characterization.forward with reverse
    have equal := RealLe.antisymmetric with first, second
    exact distinct with equal
  exact realLess.of_not_le with notReverse

theorem closedInterval.endpoint_or_interior (A B T : Real)
  requires member : T ∈ closedInterval(A, B)
  shows T = A ∨ T = B ∨ (A < T ∧ T < B)
proof
  obtain ⟨realT, lower, upper⟩ := closedInterval.membership.forward with member
  have alternativeA : T = A ∨ T ≠ A by tauto
  have alternativeB : T = B ∨ T ≠ B by tauto
  cases alternativeA with atA | awayA
  . tauto
  . cases alternativeB with atB | awayB
    . tauto
    . have strictA := closedInterval.left_lt_of_ne at A, B, T with
        member, awayA
      have strictB := closedInterval.right_lt_of_ne with member, awayB
      tauto

-- Section: Rolle
theorem Rolle.midpoint_of_endpoint_extrema (f : Set) (A B T D : Real)
  requires ordered : A < B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires endpoints : f(A) = f(B)
  requires maximumA : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(A):R)
  requires minimumT : ∀ X ∈ closedInterval(A, B),
    (f(T):R) ≤ (f(X):R)
  requires endpointT : T = A ∨ T = B
  requires derivative : HasDerivativeAt(f, D, intervalMidpoint(A, B))
  shows D = 0
proof
  obtain ⟨left, right⟩ := intervalMidpoint.between with ordered
  have middleReal := intervalMidpoint.real at A, B with *
  have middleMember : intervalMidpoint(A, B) ∈ closedInterval(A, B)
    have lower := realLess.implies_le with left
    have upper := realLess.implies_le with right
    have inReals : intervalMidpoint(A, B) ∈ ℝ by exact middleReal
    apply closedInterval.membership.backward
    refine ⟨inReals, lower, upper⟩
  have minimumAtMiddle := minimumT with intervalMidpoint(A, B), middleMember
  have minimumA : (f(A):R) ≤ (f(intervalMidpoint(A, B)):R)
    cases endpointT with atA | atB
    . rw atA at minimumAtMiddle
      exact minimumAtMiddle
    . rw [atB, ← endpoints] at minimumAtMiddle
      exact minimumAtMiddle
  have maximumAtMiddle := maximumA with intervalMidpoint(A, B), middleMember
  have function : f : ℝ → ℝ
    rcases continuous with ⟨graph, subset, atPoints⟩
    exact graph
  have realA : A ∈ ℝ by simp [Real]
  have realMiddle : intervalMidpoint(A, B) ∈ ℝ by exact middleReal
  have valueA := FunctionBetween.apply_closed with function, realA
  have valueMiddle := FunctionBetween.apply_closed with function, realMiddle
  have lowerView := realLe.characterization.forward with minimumA
  have upperView := realLe.characterization.forward with maximumAtMiddle
  have equal := RealLe.antisymmetric with lowerView, upperView
  have maximalMiddle : ∀ X ∈ closedInterval(A, B),
      (f(X):R) ≤ (f(intervalMidpoint(A, B)):R)
    intros X member
    have bound := maximumA with X, member
    rwa equal at bound
  exact HasDerivativeAt.zero_at_interval_max with left, right, derivative, maximalMiddle

theorem Rolle.of_endpoint_maximum (f : Set) (A B : Real)
  requires ordered : A < B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires endpoints : f(A) = f(B)
  requires maximumA : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(A):R)
  requires differentiable : ∀ C ∈ ℝ, A < C → C < B →
    ∃ D ∈ ℝ, HasDerivativeAt(f, D, C)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ HasDerivativeAt(f, realZero, C)
proof
  have orderedWeak := realLess.implies_le with ordered
  obtain ⟨T, member, minimum⟩ := ContinuousOn.closed_interval_minimum with orderedWeak, continuous
  obtain ⟨realT, lowerT, upperT⟩ := closedInterval.membership.forward with member
  have typedT : Real(T) by exact realT
  have status := closedInterval.endpoint_or_interior at A, B, T with
    typedT, member
  cases status with atA | other
  . have midpointReal := intervalMidpoint.real at A, B with *{2}
    obtain ⟨left, right⟩ := intervalMidpoint.between with ordered
    have midpointMember : intervalMidpoint(A, B) ∈ ℝ by exact midpointReal
    obtain ⟨D, realD, derivative⟩ := differentiable with
      intervalMidpoint(A, B), midpointMember, left, right
    have endpointT : T = A ∨ T = B by tauto
    have zero := Rolle.midpoint_of_endpoint_extrema with
      ordered, continuous, endpoints, maximumA, minimum, endpointT, derivative
    witness intervalMidpoint(A, B)
    refine ⟨midpointMember, left, right, _⟩
    rwa ← zero
  . cases other with atB | interior
    . have midpointReal := intervalMidpoint.real at A, B with *{2}
      obtain ⟨left, right⟩ := intervalMidpoint.between with ordered
      have midpointMember : intervalMidpoint(A, B) ∈ ℝ by exact midpointReal
      obtain ⟨E0, realE0, derivativeE0⟩ := differentiable with
        intervalMidpoint(A, B), midpointMember, left, right
      have endpointT : T = A ∨ T = B by tauto
      have zero := Rolle.midpoint_of_endpoint_extrema with
        ordered, continuous, endpoints, maximumA, minimum, endpointT, derivativeE0
      witness intervalMidpoint(A, B)
      refine ⟨midpointMember, left, right, _⟩
      rwa ← zero
    . rcases interior with ⟨left, right⟩
      obtain ⟨E1, realE1, derivativeE1⟩ := differentiable with
        T, realT, left, right
      have zero := HasDerivativeAt.zero_at_interval_min with left, right, derivativeE1, minimum
      witness T
      refine ⟨realT, left, right, _⟩
      rwa ← zero

theorem Rolle.endpoint_maximum_value (f : Set) (A B T : Real)
  requires endpoints : f(A) = f(B)
  requires maximum : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(T):R)
  requires endpointT : T = A ∨ T = B
  shows ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(A):R)
proof
  intros X member
  have bound := maximum with X, member
  cases endpointT with atA | atB
  . rw atA at bound
    exact bound
  . rw [atB, ← endpoints] at bound
    exact bound

theorem Rolle.endpoint_maximum_left (f : Set) (A B T : Real)
  requires endpoints : f(A) = f(B)
  requires maximum : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(T):R)
  requires atA : T = A
  shows ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(A):R)
proof
  intros X member
  have bound := maximum with X, member
  rwa atA at bound

theorem Rolle.endpoint_maximum_right (f : Set) (A B T : Real)
  requires endpoints : f(A) = f(B)
  requires maximum : ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(T):R)
  requires atB : T = B
  shows ∀ X ∈ closedInterval(A, B),
    (f(X):R) ≤ (f(A):R)
proof
  intros X member
  have bound := maximum with X, member
  rwa [atB, ← endpoints] at bound

-- The textbook hypotheses: continuity on the closed interval, differentiability
-- at every interior point, and equal endpoint values.
theorem Rolle.theorem (f : Set) (A B : Real)
  requires ordered : A < B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires endpoints : f(A) = f(B)
  requires differentiable : ∀ C ∈ ℝ, A < C → C < B →
    ∃ D ∈ ℝ, HasDerivativeAt(f, D, C)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ HasDerivativeAt(f, realZero, C)
proof
  have orderedWeak := realLess.implies_le with ordered
  obtain ⟨T, member, maximum⟩ := ContinuousOn.closed_interval_maximum with orderedWeak, continuous
  obtain ⟨realT, lowerT, upperT⟩ := closedInterval.membership.forward with member
  have typedT : Real(T) by exact realT
  have status := closedInterval.endpoint_or_interior at A, B, T with
    typedT, member
  cases status with atA | other
  . have maxA := Rolle.endpoint_maximum_left at f, A, B, T with
      endpoints, maximum, atA
    exact Rolle.of_endpoint_maximum with ordered, continuous, endpoints, maxA, differentiable
  . cases other with atB | interior
    . have maxA := Rolle.endpoint_maximum_right at f, A, B, T with
        endpoints, maximum, atB
      exact Rolle.of_endpoint_maximum with ordered, continuous, endpoints, maxA, differentiable
    . rcases interior with ⟨left, right⟩
      obtain ⟨D, realD, derivative⟩ := differentiable with
        T, realT, left, right
      have zero := HasDerivativeAt.zero_at_interval_max with left, right, derivative, maximum
      witness T
      refine ⟨realT, left, right, _⟩
      rwa ← zero

-- Section: MeanValueIntegration
theorem MeanValue.theorem (F : Set) (A B : Real)
  requires ordered : A < B
  requires continuous : ContinuousOn(F, closedInterval(A, B))
  requires differentiable : ∀ C ∈ ℝ, A < C → C < B → ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ ∃ D ∈ ℝ, HasDerivativeAt(F, D, C) ∧ D * (B - A) = F(B) - F(A)
proof
  have function : F : ℝ → ℝ
    rcases continuous with ⟨graph, subset, everywhere⟩
    exact graph
  have correctionContinuous := meanValueCorrection.continuous_on with continuous
  have endpoints := meanValueCorrection.endpoints at F, A, B with function
  have correctionDifferentiable : ∀ C ∈ ℝ, A < C → C < B →
      ∃ E ∈ ℝ, HasDerivativeAt(meanValueCorrection(F, A, B), E, C)
    intros C realC left right
    obtain ⟨D, realD, derivative⟩ := differentiable with C, realC, left, right
    have typedD : Real(D) by exact realD
    have atC := meanValueCorrection.derivative at F, A, B, C, D with derivative
    have realA : A ∈ ℝ by simp [Real]
    have realB : B ∈ ℝ by simp [Real]
    have valueA := FunctionBetween.apply_closed with function, realA
    have valueB := FunctionBetween.apply_closed with function, realB
    have typedFA : Real(F(A)) by exact valueA
    have typedFB : Real(F(B)) by exact valueB
    have widthReal := realSubValue.real at B, A with *
    have deltaReal := realSubValue.real with typedFB, typedFA
    have productReal := realMulValue.real with widthReal, typedD
    have slopeReal := realSubValue.real with productReal, deltaReal
    witness (B - A) * D - (F(B) - F(A))
    constructor
      exact slopeReal
    . exact atC
  obtain ⟨T, realT, left, right, zeroDerivative⟩ := Rolle.theorem with
    ordered, correctionContinuous, endpoints, correctionDifferentiable
  obtain ⟨E, realE, derivative⟩ := differentiable with T, realT, left, right
  have slopeDerivative := meanValueCorrection.derivative at F, A, B, T, E with derivative
  have unique := HasDerivativeAt.unique with slopeDerivative, zeroDerivative
  witness T
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have fA := FunctionBetween.apply_closed with function, realA
  have fB := FunctionBetween.apply_closed with function, realB
  have typedFA : Real(F(A)) by exact fA
  have typedFB : Real(F(B)) by exact fB
  have deltaReal := realSubValue.real with typedFB, typedFA
  have equation : E * (B - A) = F(B) - F(A)
    have transform : E * (B - A) =
        ((B - A) * E - (F(B) - F(A))) +
          (F(B) - F(A))
      ring
    rw unique at transform
    have zero := realAddValue.zero_left with deltaReal
    rwa zero at transform
  refine ⟨realT, left, right, E, realE, derivative, equation⟩

-- A differentiable primitive provides every mean-value tag required by the
-- checked tagged-partition endpoint theorem.

-- MeanValueIntegration
theorem CellMeanValueProperty.of_derivative (f F : Set)
  requires fFunction : f : ℝ → ℝ
  requires continuous : Continuous(F)
  requires derivative : ∀ C ∈ ℝ, HasDerivativeAt(F, f(C), C)
  shows CellMeanValueProperty(f, F)
proof
  have function := Continuous.function with continuous
  intros A realA B realB ordered
  have subset := closedInterval.subset_reals at A, B with *
  have onInterval := Continuous.continuous_on with continuous, subset
  have differentiable : ∀ C ∈ ℝ, A < C → C < B →
      ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)
    intros C realC left right
    have derivativeValue := FunctionBetween.apply_closed with fFunction, realC
    have value := derivative with C, realC
    witness f(C)
    refine ⟨derivativeValue, value⟩
  obtain ⟨T, realT, left, right, D, realD, derivativeD, equation⟩ := MeanValue.theorem with
    ordered, onInterval, differentiable
  have typedT : Real(T)
    unfold Real
    exact realT
  have derivativeValue := FunctionBetween.apply_closed with fFunction, realT
  have derivativeF := derivative with T, realT
  have equal := HasDerivativeAt.unique with derivativeD, derivativeF
  have member : T ∈ closedInterval(A, B)
    have lower := realLess.implies_le with left
    have upper := realLess.implies_le with right
    have data : T ∈ ℝ ∧ A ≤ T ∧ T ≤ B by refine ⟨realT, lower, upper⟩
    exact closedInterval.membership.backward with data
  witness T
  constructor
  . exact member
  . unfold realMulValue
    unfold call2 at equation
    rwa equal at equation

theorem HasRiemannIntegral.eq_endpoint_of_derivative (f F : Set) (A B I : Real)
  requires fFunction : f : ℝ → ℝ
  requires continuous : Continuous(F)
  requires derivative : ∀ C ∈ ℝ, HasDerivativeAt(F, f(C), C)
  requires integral : HasRiemannIntegral(f, A, B, I)
  shows I = F(B) - F(A)
proof
  have function := Continuous.function with continuous
  have meanValue := CellMeanValueProperty.of_derivative with fFunction, continuous, derivative
  exact HasRiemannIntegral.eq_endpoint_of_mean_value with function, integral, meanValue