-- Real analysis: L'Hôpital's rule
-- 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.LHopital
import CauchyMeanValue

-- Section: Preparations
theorem openBall.right_between (A C X E : Real)
  requires member : X ∈ openBall(A, E)
  requires left : A < C
  requires right : C < X
  shows C ∈ openBall(A, E)
proof
  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with member
  have data : A - E < C ∧ C < A + E
    constructor
    . linarith
    . linarith
  exact openBall.order_characterization.backward with data

theorem openBall.left_between (A C X E : Real)
  requires member : X ∈ openBall(A, E)
  requires left : X < C
  requires right : C < A
  shows C ∈ openBall(A, E)
proof
  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with member
  have data : A - E < C ∧ C < A + E
    constructor
    . linarith
    . linarith
  exact openBall.order_characterization.backward with data

theorem closedInterval.subset_ball_right (A X W : Real)
  requires member : X ∈ openBall(A, W)
  requires positive : 0 < W
  shows closedInterval(A, X) ⊆ openBall(A, W)
proof
  intros Y memberY
  obtain ⟨realY, lower, upper⟩ := closedInterval.membership.forward with memberY
  have typedY : Real(Y) by exact realY
  obtain ⟨lowerX, upperX⟩ := openBall.order_characterization.forward with member
  have data : A - W < Y ∧ Y < A + W
    constructor
    . linarith
    . linarith
  exact openBall.order_characterization.backward with data

theorem closedInterval.subset_ball_left (X A W : Real)
  requires member : X ∈ openBall(A, W)
  requires positive : 0 < W
  shows closedInterval(X, A) ⊆ openBall(A, W)
proof
  intros Y memberY
  obtain ⟨realY, lower, upper⟩ := closedInterval.membership.forward with memberY
  have typedY : Real(Y) by exact realY
  obtain ⟨lowerX, upperX⟩ := openBall.order_characterization.forward with member
  have data : A - W < Y ∧ Y < A + W
    constructor
    . linarith
    . linarith
  exact openBall.order_characterization.backward with data

-- Section: OneSidedQuotients
-- To the right of A, the quotient f/g at X is the quotient of the
-- derivatives at some point strictly between A and X.
theorem LHopital.right (f g : ℝ → ℝ) (A W X : Real)
  requires radius : 0 < W
  requires differentiableF : ∀ Y ∈ openBall(A, W), DifferentiableAt(f, Y)
  requires differentiableG : ∀ Y ∈ openBall(A, W), DifferentiableAt(g, Y)
  requires nonzero : ∀ Y ∈ openBall(A, W), Y ≠ A → g′(Y) ≠ (0:R)
  requires zeroF : f(A) = 0
  requires zeroG : g(A) = 0
  requires member : X ∈ openBall(A, W)
  requires right : A < X
  shows ∃ C ∈ ℝ, A < C ∧ C < X ∧
    pointwiseDiv(f, g)(X) = pointwiseDiv(f′, g′)(C)
proof
  have realA : A ∈ ℝ by simp [Real]
  have realX : X ∈ ℝ by simp [Real]
  have fFunction : f : ℝ → ℝ by assumption
  have gFunction : g : ℝ → ℝ by assumption
  have subset := closedInterval.subset_ball_right at A, X, W with member, radius
  have intervalReal := closedInterval.subset_reals at A, X with *
  have onIntervalF : ∀ Y ∈ closedInterval(A, X), DifferentiableAt(f, Y)
    intros Y memberY
    have inBall := subset with Y, memberY
    exact differentiableF with Y, inBall
  have onIntervalG : ∀ Y ∈ closedInterval(A, X), DifferentiableAt(g, Y)
    intros Y memberY
    have inBall := subset with Y, memberY
    exact differentiableG with Y, inBall
  have continuousF := ContinuousOn.of_differentiable with
    fFunction, intervalReal, onIntervalF
  have continuousG := ContinuousOn.of_differentiable with
    gFunction, intervalReal, onIntervalG
  have interiorF : ∀ C ∈ ℝ, A < C → C < X → DifferentiableAt(f, C)
    intros C realC left rightC
    have typedC : Real(C) by exact realC
    have inBall := openBall.right_between at A, C, X, W with
      member, left, rightC
    exact differentiableF with C, inBall
  have interiorG : ∀ C ∈ ℝ, A < C → C < X → DifferentiableAt(g, C)
    intros C realC left rightC
    have typedC : Real(C) by exact realC
    have inBall := openBall.right_between at A, C, X, W with
      member, left, rightC
    exact differentiableG with C, inBall
  have typedFX : Real(f(X))
    exact FunctionBetween.apply_closed with fFunction, realX
  have typedGX : Real(g(X))
    exact FunctionBetween.apply_closed with gFunction, realX
  have nonzeroGX : g(X) ≠ (0:R)
    intro vanishes
    have endpoints : g(A) = g(X)
      rw [zeroG, vanishes]
      rfl
    have unfoldedG : ∀ C ∈ ℝ, A < C → C < X → ∃ D ∈ ℝ, HasDerivativeAt(g, D, C)
      intros C realC left rightC
      have differentiableAt := interiorG with C, realC, left, rightC
      unfold DifferentiableAt at differentiableAt
      exact differentiableAt
    obtain ⟨C, realC, left, rightC, zeroDerivative⟩ := Rolle.theorem with
      right, continuousG, endpoints, unfoldedG
    have typedC : Real(C) by exact realC
    have value := derivative.of_has_derivative with zeroDerivative
    have inBall := openBall.right_between at A, C, X, W with
      member, left, rightC
    have distinct : C ≠ A
      intro equal
      rw equal at left
      linarith
    have nonzeroC := nonzero with C, inBall, distinct
    exact nonzeroC with value
  obtain ⟨C, realC, left, rightC, equation⟩ := CauchyMeanValue.theorem with
    fFunction, gFunction, right, continuousF, continuousG, interiorF, interiorG
  have typedC : Real(C) by exact realC
  have inBall := openBall.right_between at A, C, X, W with member, left, rightC
  have distinct : C ≠ A
    intro equal
    rw equal at left
    linarith
  have nonzeroC := nonzero with C, inBall, distinct
  have typedDF := derivative.real at f, C
  have typedDG := derivative.real at g, C
  have cross : derivative(f)(C) * g(X) = derivative(g)(C) * f(X)
    rw [zeroF, zeroG] at equation
    linear_combination equation
  have quotientValue := pointwiseDiv.value at f, g, X with
    fFunction, gFunction, typedFX, typedGX
  have derivativeFFunction := derivative.function at f
  have derivativeGFunction := derivative.function at g
  have derivativeQuotient := pointwiseDiv.value at
    derivative(f), derivative(g), C with
      derivativeFFunction, derivativeGFunction, typedDF, typedDG
  have equal := realDiv.eq_of_cross at
    f(X), g(X), derivative(f)(C), derivative(g)(C) with
      typedFX, typedGX, typedDF, typedDG, nonzeroGX, nonzeroC, cross
  witness C
  refine ⟨realC, left, rightC, _⟩
  rw [quotientValue, derivativeQuotient]
  exact equal

theorem LHopital.left (f g : ℝ → ℝ) (A W X : Real)
  requires radius : 0 < W
  requires differentiableF : ∀ Y ∈ openBall(A, W), DifferentiableAt(f, Y)
  requires differentiableG : ∀ Y ∈ openBall(A, W), DifferentiableAt(g, Y)
  requires nonzero : ∀ Y ∈ openBall(A, W), Y ≠ A → g′(Y) ≠ (0:R)
  requires zeroF : f(A) = 0
  requires zeroG : g(A) = 0
  requires member : X ∈ openBall(A, W)
  requires left : X < A
  shows ∃ C ∈ ℝ, X < C ∧ C < A ∧
    pointwiseDiv(f, g)(X) = pointwiseDiv(f′, g′)(C)
proof
  have realA : A ∈ ℝ by simp [Real]
  have realX : X ∈ ℝ by simp [Real]
  have fFunction : f : ℝ → ℝ by assumption
  have gFunction : g : ℝ → ℝ by assumption
  have subset := closedInterval.subset_ball_left at X, A, W with member, radius
  have intervalReal := closedInterval.subset_reals at X, A with *
  have onIntervalF : ∀ Y ∈ closedInterval(X, A), DifferentiableAt(f, Y)
    intros Y memberY
    have inBall := subset with Y, memberY
    exact differentiableF with Y, inBall
  have onIntervalG : ∀ Y ∈ closedInterval(X, A), DifferentiableAt(g, Y)
    intros Y memberY
    have inBall := subset with Y, memberY
    exact differentiableG with Y, inBall
  have continuousF := ContinuousOn.of_differentiable with
    fFunction, intervalReal, onIntervalF
  have continuousG := ContinuousOn.of_differentiable with
    gFunction, intervalReal, onIntervalG
  have interiorF : ∀ C ∈ ℝ, X < C → C < A → DifferentiableAt(f, C)
    intros C realC leftC rightC
    have typedC : Real(C) by exact realC
    have inBall := openBall.left_between at A, C, X, W with
      member, leftC, rightC
    exact differentiableF with C, inBall
  have interiorG : ∀ C ∈ ℝ, X < C → C < A → DifferentiableAt(g, C)
    intros C realC leftC rightC
    have typedC : Real(C) by exact realC
    have inBall := openBall.left_between at A, C, X, W with
      member, leftC, rightC
    exact differentiableG with C, inBall
  have typedFX : Real(f(X))
    exact FunctionBetween.apply_closed with fFunction, realX
  have typedGX : Real(g(X))
    exact FunctionBetween.apply_closed with gFunction, realX
  have nonzeroGX : g(X) ≠ (0:R)
    intro vanishes
    have endpoints : g(X) = g(A)
      rw [zeroG, vanishes]
      rfl
    have unfoldedG : ∀ C ∈ ℝ, X < C → C < A → ∃ D ∈ ℝ, HasDerivativeAt(g, D, C)
      intros C realC leftC rightC
      have differentiableAt := interiorG with C, realC, leftC, rightC
      unfold DifferentiableAt at differentiableAt
      exact differentiableAt
    obtain ⟨C, realC, leftC, rightC, zeroDerivative⟩ := Rolle.theorem with
      left, continuousG, endpoints, unfoldedG
    have typedC : Real(C) by exact realC
    have value := derivative.of_has_derivative with zeroDerivative
    have inBall := openBall.left_between at A, C, X, W with
      member, leftC, rightC
    have distinct : C ≠ A
      intro equal
      rw equal at rightC
      linarith
    have nonzeroC := nonzero with C, inBall, distinct
    exact nonzeroC with value
  obtain ⟨C, realC, leftC, rightC, equation⟩ := CauchyMeanValue.theorem with
    fFunction, gFunction, left, continuousF, continuousG, interiorF, interiorG
  have typedC : Real(C) by exact realC
  have inBall := openBall.left_between at A, C, X, W with member, leftC, rightC
  have distinct : C ≠ A
    intro equal
    rw equal at rightC
    linarith
  have nonzeroC := nonzero with C, inBall, distinct
  have typedDF := derivative.real at f, C
  have typedDG := derivative.real at g, C
  have cross : derivative(f)(C) * g(X) = derivative(g)(C) * f(X)
    rw [zeroF, zeroG] at equation
    symm
    linear_combination equation
  have quotientValue := pointwiseDiv.value at f, g, X with
    fFunction, gFunction, typedFX, typedGX
  have derivativeFFunction := derivative.function at f
  have derivativeGFunction := derivative.function at g
  have derivativeQuotient := pointwiseDiv.value at
    derivative(f), derivative(g), C with
      derivativeFFunction, derivativeGFunction, typedDF, typedDG
  have equal := realDiv.eq_of_cross at
    f(X), g(X), derivative(f)(C), derivative(g)(C) with
      typedFX, typedGX, typedDF, typedDG, nonzeroGX, nonzeroC, cross
  witness C
  refine ⟨realC, leftC, rightC, _⟩
  rw [quotientValue, derivativeQuotient]
  exact equal

-- Section: LHopital
-- L'Hôpital's rule in the 0/0 form at a point: when f and g are
-- differentiable near A with f(A) = g(A) = 0 and g′ nonzero away from A,
-- f′/g′ → L at A forces f/g → L at A.
theorem LHopital.theorem (f g : ℝ → ℝ) (A L W : Real)
  requires radius : 0 < W
  requires differentiableF : ∀ X ∈ openBall(A, W), DifferentiableAt(f, X)
  requires differentiableG : ∀ X ∈ openBall(A, W), DifferentiableAt(g, X)
  requires nonzero : ∀ X ∈ openBall(A, W), X ≠ A → g′(X) ≠ (0:R)
  requires zeroF : f(A) = 0
  requires zeroG : g(A) = 0
  requires limit : TendsToAt(pointwiseDiv(f′, g′), L, A)
  shows TendsToAt(pointwiseDiv(f, g), L, A)
proof
  have fFunction : f : ℝ → ℝ by assumption
  have gFunction : g : ℝ → ℝ by assumption
  have quotientFunction := pointwiseDiv.function with fFunction, gFunction
  constructor
  . exact quotientFunction
  . intros E realE positive
    obtain ⟨D, realD, positiveD, maps⟩ := TendsToAt.eventually with
      limit, positive
    have typedD : Real(D) by exact realD
    obtain ⟨S, realS, positiveS, belowD, belowW⟩ :=
      positiveRadius.common with positiveD, radius
    have typedS : Real(S) by exact realS
    witness S
    refine ⟨realS, positiveS, _⟩
    intros X realX distinct near
    have typedX : Real(X) by exact realX
    have nearD := openBall.mono with near, belowD
    have nearW := openBall.mono with near, belowW
    have order := realLess.trichotomy at X, A
    rcases order with below | equal | above
    . obtain ⟨C, realC, leftC, rightC, value⟩ := LHopital.left with
        fFunction, gFunction, radius, differentiableF, differentiableG, nonzero,
        zeroF, zeroG, nearW, below
      have typedC : Real(C) by exact realC
      have inBallD := openBall.left_between at A, C, X, D with
        nearD, leftC, rightC
      have distinctC : C ≠ A
        intro equalC
        rw equalC at rightC
        linarith
      have mapped := maps with C, realC, distinctC, inBallD
      rw value
      exact mapped
    . exfalso
      exact distinct with equal
    . obtain ⟨C, realC, leftC, rightC, value⟩ := LHopital.right with
        fFunction, gFunction, radius, differentiableF, differentiableG, nonzero,
        zeroF, zeroG, nearW, above
      have typedC : Real(C) by exact realC
      have inBallD := openBall.right_between at A, C, X, D with
        nearD, leftC, rightC
      have distinctC : C ≠ A
        intro equalC
        rw equalC at leftC
        linarith
      have mapped := maps with C, realC, distinctC, inBallD
      rw value
      exact mapped