LeanEconTheory
Envelope Theorem

Imports

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Comp
import Mathlib.Analysis.Calculus.FDeriv.Prod
import Mathlib.Analysis.Calculus.FDeriv.Add

Envelope Theorem

Introduction

This page lays out the Lean formalization code of the Envelope Theorem. A graphical visualization of the relevant mathematical dependencies can be viewed here.

Setup

In the setup, I tell Lean we are not using any functions for computation, but just for symbolic manipulation. Furthermore, I tell Lean to interpret any use of X, A, and Y to be of NormedAddCommGroup, NormedSpace type the curly braces denote the implicit argument and type inferred by Lean. I also define variables present in the Lagrangian, and I define the Lagrange multiplier as a continuous linear map from the space of restrictions to the value function codomain.

              noncomputable sectionvariable {X A Y : Type*}variable [NormedAddCommGroup X] [NormedSpace ℝ X]variable [NormedAddCommGroup A] [NormedSpace ℝ A]variable [NormedAddCommGroup Y] [NormedSpace ℝ Y]variable (f : X × A → ℝ)variable (g : X × A → Y)variable (x_star : A → X)variable (lambda_star : A → (Y →L[ℝ] ℝ))

Definition: Value Function

The value function as a function of the parameters α is given by V(α) = f(x^*(α), α), where x^*(α) is the unique maximizer of f given the parameters α, and subject to the constraint g(x, α) = 0.

def V (f : X × A → ℝ) (x_star : A → X) (α : A) : ℝ :=
  f (x_star α, α)

Definition: Lagrangian

The Lagrangian is given by L(x, α) = f(x, α) + λ g(x, α).

def Lagrangian (f : X × A → ℝ) (g : X × A → Y) (x : X) (α : A) (Λ : Y →L[ℝ] ℝ) : ℝ :=
  f (x, α) + Λ (g (x, α))

Theorem: Envelope Theorem

\frac{dV}{dα} = \left.\frac{∂L}{∂α}\right|_{(x^*, λ^*)} Proof.
Define L'(x, α) := f(x, α) + λ^* (g(x, α)). As we always have g(x^*(α), α) = 0, α ∈ A, x \in X for the specified spaces A and X, we obtain that V(α) = f(x^*(α), α) + 0 = f(x^*(α), α) + λ^*(0) =: L'(x^*(α), α), because λ^* is a linear continuous map.

By then applying the chain rule under this formulation, we get that \frac{dV}{dα} = \left.\frac{∂L'}{∂x}·\frac{∂x^*}{dα}\right|_{(x^*, λ^*)} + \left.\frac{∂L'}{∂α}\right|_{(x^*, λ^*)}, because at the optimum we have that \left.\frac{∂L}{∂x}\right|_{(x^*, λ^*)} = 0.

Therefore, we obtain that \frac{dV}{dα} = 0 + \left.\frac{∂L}{∂α}\right|_{(x^*, λ^*)} = \left.\frac{∂L}{∂α}\right|_{(x^*, λ^*)}. ■

theorem EnvelopeTheorem
(α : A)
-- Define the differentiability assumptions
(hf : DifferentiableAt ℝ f (x_star α, α))
(hg : DifferentiableAt ℝ g (x_star α, α))
(hx : DifferentiableAt ℝ x_star α)
-- Define the assumption that the constraint is to be satisfied
-- at any `x_star` from parameters `a`
(h_constraint : ∀ a, g (x_star a, a) = 0)
-- Define the derivative of the Lagrangian at the optimum to be zero
(h_FOC : fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0) :
-- State the result of the Envelope Theorem
fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
  -- Define a Lagrangian with fixed Lagrange multiplier
  -- to simpify the chain rule later on
  let L_fixed : X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
  -- Prove V(a) = L_fixed(x_star a, a) for all a
  have h_V_eq : ∀ a, V f x_star a = L_fixed (x_star a, a) := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    intro aX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)a:A⊢ V f x_star a = L_fixed (x_star a, a)
    unfold VX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)a:A⊢ f (x_star a, a) = L_fixed (x_star a, a)
    -- Expand L_fixed on the RHS
    dsimp [L_fixed]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)a:A⊢ f (x_star a, a) = f (x_star a, a) + (lambda_star α) (g (x_star a, a))
    -- Invoke the constraint being zero
    rw [h_constraint a]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)a:A⊢ f (x_star a, a) = f (x_star a, a) + (lambda_star α) 0
    -- Since lambda_star α is a continuous linear map, applying it to 0 yields 0
    rw [ContinuousLinearMap.map_zero]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)a:A⊢ f (x_star a, a) = f (x_star a, a) + 0
    rw [add_zero]All goals completed! 🐙
  -- Rewrite the objective derivative using h_V_eq
  have h_V_eq_deriv : fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) α := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    have h_fun_eq : V f x_star = fun a ↦ L_fixed (x_star a, a) := funext h_V_eqX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_fun_eq:V f x_star = fun a ↦ L_fixed (x_star a, a)⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) α
    rw [h_fun_eq]All goals completed! 🐙
  rw [h_V_eq_deriv]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) α⊢ fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
  -- Write the lambda function for the Lagrangian as a composite function
  -- for easier reduction of the goal later on
  have h_comp : (fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a) := rflX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)⊢ fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
  rw [h_comp]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)⊢ fderiv ℝ (L_fixed ∘ fun a ↦ (x_star a, a)) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
  -- Rewrite differentiability of the Lagrangian
  have hL_diff : DifferentiableAt ℝ L_fixed (x_star α, α) := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    apply DifferentiableAt.add hfX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)⊢ DifferentiableAt ℝ (fun p ↦ (lambda_star α) (g p)) (x_star α, α)
    exact ContinuousLinearMap.differentiableAt (lambda_star α) |>.comp (x_star α, α) hgAll goals completed! 🐙
  -- Add an auxiliary differentiation result
  have h_tuple_diff : DifferentiableAt ℝ (fun a ↦ (x_star a, a)) α := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    exact DifferentiableAt.prodMk hx differentiableAt_idAll goals completed! 🐙
  -- Apply the chain rule
  rw [fderiv_comp (f := fun a ↦ (x_star a, a)) α hL_diff h_tuple_diff]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) α⊢ (fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α) =
  fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
  -- To prove equality of continuous linear maps,
  -- evaluate both sides at an arbitrary perturbation dα
  ext dαhX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:A⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α) dα
  have dx : X := fderiv ℝ x_star α dαhX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:X⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α) dα
  -- Derive the full derivative of the Lagrangian with respect to α
  have h_L_deriv : (fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α) dα =
                fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) dx +
                fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α dα := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    -- Identify the derivative of the tuple map
    have df_tuple : fderiv ℝ (fun a ↦ (x_star a, a)) α =
                    (fderiv ℝ x_star α).prod (fderiv ℝ id α) := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
      exact DifferentiableAt.fderiv_prodMk hx differentiableAt_idAll goals completed! 🐙
    -- Obtain that the derivative of a product map applied to dα is (dx, dα)
    have prod_app : ((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα =
                    (fderiv ℝ x_star α dα, dα) := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
      simp [ContinuousLinearMap.prod_apply, fderiv_id]All goals completed! 🐙
    -- Copy the FOC assumption in slightly modified notation
    have h_partial_x : fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0 := h_FOCX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
    -- Split the tuple derivative into an axis-directional pair
    have h_split : ((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα) := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
      extfstX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ ((fderiv ℝ x_star α) dα, dα).1 = (((fderiv ℝ x_star α) dα, 0) + (0, dα)).1sndX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ ((fderiv ℝ x_star α) dα, dα).2 = (((fderiv ℝ x_star α) dα, 0) + (0, dα)).2 <;>fstX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ ((fderiv ℝ x_star α) dα, dα).1 = (((fderiv ℝ x_star α) dα, 0) + (0, dα)).1sndX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ ((fderiv ℝ x_star α) dα, dα).2 = (((fderiv ℝ x_star α) dα, 0) + (0, dα)).2 simpAll goals completed! 🐙
    -- Substitute the results into the left hand side
    rw [df_tuple]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp ((fderiv ℝ x_star α).prod (fderiv ℝ id α))) dα =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
    simp only [ContinuousLinearMap.comp_apply]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)⊢ (fderiv ℝ L_fixed (x_star α, α)) (((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
    rw [prod_app]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)⊢ (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, dα) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
    rw [h_split, ContinuousLinearMap.map_add]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)⊢ (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) + (fderiv ℝ L_fixed (x_star α, α)) (0, dα) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
    -- Show that the full derivative with respect to partial null argument
    -- can equate the partial derivative
    have h_eval_x : (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
                    (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα) := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
      -- Show differentiability of a key component
      have h_inner_diff : DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α) :=
        differentiableAt_id.prodMk (differentiableAt_const α)X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)
      -- Express the partial function as a composition
      rw [show (fun x ↦ L_fixed (x, α)) = L_fixed ∘ (fun x ↦ (x, α)) by rfl]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (L_fixed ∘ fun x ↦ (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)
      -- Apply the chain rule
      erw [fderiv_comp (x_star α) hL_diff h_inner_diff]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun x ↦ (x, α)) (x_star α))) ((fderiv ℝ x_star α) dα)
      -- Rearrange
      symmX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun x ↦ (x, α)) (x_star α))) ((fderiv ℝ x_star α) dα) =
  (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0)
      rw [DifferentiableAt.fderiv_prodMk]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp ((fderiv ℝ (fun x ↦ x) (x_star α)).prod (fderiv ℝ (fun x ↦ α) (x_star α))))
    ((fderiv ℝ x_star α) dα) =
  (fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0)hf₁X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ DifferentiableAt ℝ (fun x ↦ x) (x_star α)hf₂X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ DifferentiableAt ℝ (fun x ↦ α) (x_star α)
      simphf₁X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ DifferentiableAt ℝ (fun x ↦ x) (x_star α)hf₂X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ DifferentiableAt ℝ (fun x ↦ α) (x_star α)
      apply differentiableAt_idhf₂X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_inner_diff:DifferentiableAt ℝ (fun x ↦ (x, α)) (x_star α)⊢ DifferentiableAt ℝ (fun x ↦ α) (x_star α)
      apply differentiableAt_constAll goals completed! 🐙
    -- Show that another full derivative with respect to partial null argument
    -- can equate the partial derivative
    have h_eval_a : (fderiv ℝ L_fixed (x_star α, α)) (0, dα) =
                    (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
      -- Show differentiability of a key component
      have h_inner_diff : DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α :=
        (differentiableAt_const (x_star α)).prodMk differentiableAt_idX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ (fderiv ℝ L_fixed (x_star α, α)) (0, dα) = (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
      -- Express the partial function as a composition
      rw [show (fun a ↦ L_fixed (x_star α, a)) = L_fixed ∘ (fun a ↦ (x_star α, a)) by rfl]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ (fderiv ℝ L_fixed (x_star α, α)) (0, dα) = (fderiv ℝ (L_fixed ∘ fun a ↦ (x_star α, a)) α) dα
      -- Apply the chain rule
      erw [fderiv_comp α hL_diff h_inner_diff]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ (fderiv ℝ L_fixed (x_star α, α)) (0, dα) = ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (Prod.mk (x_star α)) α)) dα
      -- Rearrange
      symmX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (Prod.mk (x_star α)) α)) dα = (fderiv ℝ L_fixed (x_star α, α)) (0, dα)
      rw [DifferentiableAt.fderiv_prodMk]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ ((fderiv ℝ L_fixed (x_star α, α)).comp ((fderiv ℝ (fun x ↦ x_star α) α).prod (fderiv ℝ (fun x ↦ x) α))) dα =
  (fderiv ℝ L_fixed (x_star α, α)) (0, dα)hf₁X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ DifferentiableAt ℝ (fun x ↦ x_star α) αhf₂X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ DifferentiableAt ℝ (fun x ↦ x) α
      simphf₁X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ DifferentiableAt ℝ (fun x ↦ x_star α) αhf₂X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ DifferentiableAt ℝ (fun x ↦ x) α
      apply differentiableAt_consthf₂X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_inner_diff:DifferentiableAt ℝ (fun a ↦ (x_star α, a)) α⊢ DifferentiableAt ℝ (fun x ↦ x) α
      exact differentiableAt_idAll goals completed! 🐙
    rw [h_eval_x, h_eval_a, h_partial_x]X:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xdf_tuple:fderiv ℝ (fun a ↦ (x_star a, a)) α = (fderiv ℝ x_star α).prod (fderiv ℝ id α)prod_app:((fderiv ℝ x_star α).prod (fderiv ℝ id α)) dα = ((fderiv ℝ x_star α) dα, dα)h_partial_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0h_split:((fderiv ℝ x_star α) dα, dα) = ((fderiv ℝ x_star α) dα, 0) + (0, dα)h_eval_x:(fderiv ℝ L_fixed (x_star α, α)) ((fderiv ℝ x_star α) dα, 0) =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) ((fderiv ℝ x_star α) dα)h_eval_a:(fderiv ℝ L_fixed (x_star α, α)) (0, dα) = (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα⊢ 0 ((fderiv ℝ x_star α) dα) + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα =
  0 dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα
    simp only [ContinuousLinearMap.zero_apply, zero_add]All goals completed! 🐙
  rw [h_L_deriv]hX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xh_L_deriv:((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα⊢ (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα =
  (fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α) dα
  -- Use h_FOC to show the partial derivative in the Lagrangian with respect to x vanishes
  have h_L_x : fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0 := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    exact h_FOCAll goals completed! 🐙
  rw [h_L_x]hX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xh_L_deriv:((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dαh_L_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ 0 dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα =
  (fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α) dα
  -- The zero linear map applied to dx is 0
  rw [ContinuousLinearMap.zero_apply]hX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xh_L_deriv:((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dαh_L_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ 0 + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα =
  (fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α) dα
  rw [zero_add]hX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0L_fixed:X × A → ℝ := fun p ↦ f p + (lambda_star α) (g p)h_V_eq:∀ (a : A), V f x_star a = L_fixed (x_star a, a)h_V_eq_deriv:fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ L_fixed (x_star a, a)) αh_comp:(fun a ↦ L_fixed (x_star a, a)) = L_fixed ∘ fun a ↦ (x_star a, a)hL_diff:DifferentiableAt ℝ L_fixed (x_star α, α)h_tuple_diff:DifferentiableAt ℝ (fun a ↦ (x_star a, a)) αdα:Adx:Xh_L_deriv:((fderiv ℝ L_fixed (x_star α, α)).comp (fderiv ℝ (fun a ↦ (x_star a, a)) α)) dα =
  (fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α)) dx + (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dαh_L_x:fderiv ℝ (fun x ↦ L_fixed (x, α)) (x_star α) = 0⊢ (fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α) dα = (fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α) dα
  -- Conclude the remainder is exactly the partial derivative of the Lagrangian with respect to α
  have h_L_α : fderiv ℝ (fun a ↦ L_fixed (x_star α, a)) α dα =
               fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α dα := byX:Type u_1A:Type u_2Y:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:NormedAddCommGroup Ainst✝²:NormedSpace ℝ Ainst✝¹:NormedAddCommGroup Yinst✝:NormedSpace ℝ Yf:X × A → ℝg:X × A → Yx_star:A → Xlambda_star:A → Y →L[ℝ] ℝα:Ahf:DifferentiableAt ℝ f (x_star α, α)hg:DifferentiableAt ℝ g (x_star α, α)hx:DifferentiableAt ℝ x_star αh_constraint:∀ (a : A), g (x_star a, a) = 0h_FOC:fderiv ℝ (fun x ↦ Lagrangian f g x α (lambda_star α)) (x_star α) = 0⊢ fderiv ℝ (V f x_star) α = fderiv ℝ (fun a ↦ Lagrangian f g (x_star α) a (lambda_star α)) α
    rflAll goals completed! 🐙
  exact h_L_αAll goals completed! 🐙