Mathlib.Analysis.Calculus.Derivative

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Topology.Metric.Basic
import Mathlib.LinearAlgebra.VectorSpace
import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Analysis.LinearMap

def FrechetRemainder.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (h : X), Y :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun h => @vsub.{w} Y yadd yneg (f (xadd point h)) (yadd (f point) (df h))

def FrechetDerivativeAt.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun bound => fun remainder_small => forall (P : Prop), forall (mk : forall (linear_law : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df), forall (operator_bound_law : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound), forall (remainder_law : forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)), P), P

def FrechetDifferentiableAt.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => forall (P : Prop), forall (mk : forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), P), P

def FrechetDifferentiableOn.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (domain : forall (x : X), Prop), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun domain => forall (x : X), forall (hx : domain x), @FrechetDifferentiableAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f x

def DerivativeUniqueArgs.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => forall (df_left : forall (h : X), Y), forall (bound_left : Scalar), forall (remainder_left : forall (r : Y), Prop), forall (df_right : forall (h : X), Y), forall (bound_right : Scalar), forall (remainder_right : forall (r : Y), Prop), forall (left_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df_left bound_left remainder_left), forall (right_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df_right bound_right remainder_right), forall (h : X), @Eq.{w} Y (df_left h) (df_right h)

def ConstMap.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (value : Y), forall (x : X), Y :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun value => fun x => value

def ZeroMap.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (h : X), Y :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun h => yzero

def PairMap.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (y : Y), forall (z : Z), Product), forall (fst : forall (point : Product), Y), forall (snd : forall (point : Product), Z), forall (f : forall (x : X), Y), forall (g : forall (x : X), Z), forall (point : X), Product :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun f => fun g => fun point => pair (f point) (g point)

def PartialXMap.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (base_y : Y), forall (x : X), Z :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun base_y => fun x => F (pair x base_y)

def PartialYMap.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (base_x : X), forall (y : Y), Z :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun base_x => fun y => F (pair base_x y)

def PartialXDerivativeMap.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (dF : forall (h : Product), Z), forall (h : X), Z :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun dF => fun h => dF (pair h yzero)

def PartialYDerivativeMap.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (dF : forall (h : Product), Z), forall (h : Y), Z :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun dF => fun h => dF (pair xzero h)

def DerivativeConstRuleArgs.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => forall (point : X), forall (value : Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm (@ConstMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm value) point (@ZeroMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm) bound remainder_small

def DerivativeIdRuleArgs.{u,v} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => forall (point : Vector), forall (bound : Scalar), forall (remainder_small : forall (r : Vector), Prop), @FrechetDerivativeAt.{u,v,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm Vector vzero vadd vneg smul norm (@LinearId.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm) point (@LinearId.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm) bound remainder_small

def DerivativeFstRuleArgs.{p,u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => forall (point : Product), forall (bound : Scalar), forall (remainder_small : forall (r : X), Prop), @FrechetDerivativeAt.{u,p,v} Scalar zero one add neg sub mul le_rel Product (@ProductZero.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) X xzero xadd xneg xsmul xnorm fst point fst bound remainder_small

def DerivativeSndRuleArgs.{p,u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => forall (point : Product), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), @FrechetDerivativeAt.{u,p,w} Scalar zero one add neg sub mul le_rel Product (@ProductZero.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) Y yzero yadd yneg ysmul ynorm snd point snd bound remainder_small

def DerivativePairRuleArgs.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (y : Y), forall (z : Z), Product), forall (fst : forall (point : Product), Y), forall (snd : forall (point : Product), Z), forall (f : forall (x : X), Y), forall (g : forall (x : X), Z), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun f => fun g => forall (point : X), forall (df : forall (h : X), Y), forall (dg : forall (h : X), Z), forall (f_bound : Scalar), forall (f_remainder : forall (r : Y), Prop), forall (g_bound : Scalar), forall (g_remainder : forall (r : Z), Prop), forall (pair_bound : Scalar), forall (pair_remainder : forall (r : Product), Prop), forall (f_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df f_bound f_remainder), forall (g_at : @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm g point dg g_bound g_remainder), @FrechetDerivativeAt.{u,v,p} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Product pzero padd pneg psmul pnorm (@PairMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd f g) point (@PairMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd df dg) pair_bound pair_remainder

def DerivativeCompRuleArgs.{u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (f : forall (x : X), Y), forall (g : forall (y : Y), Z), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun f => fun g => forall (point : X), forall (df : forall (h : X), Y), forall (dg : forall (h : Y), Z), forall (f_bound : Scalar), forall (f_remainder : forall (r : Y), Prop), forall (g_bound : Scalar), forall (g_remainder : forall (r : Z), Prop), forall (comp_bound : Scalar), forall (comp_remainder : forall (r : Z), Prop), forall (f_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df f_bound f_remainder), forall (g_at : @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm g (f point) dg g_bound g_remainder), @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g) point (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm df dg) comp_bound comp_remainder

def PartialDerivativeRuleArgs.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), Prop :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => forall (base_x : X), forall (base_y : Y), forall (dF : forall (h : Product), Z), forall (F_bound : Scalar), forall (F_remainder : forall (r : Z), Prop), forall (partial_x_bound : Scalar), forall (partial_x_remainder : forall (r : Z), Prop), forall (partial_y_bound : Scalar), forall (partial_y_remainder : forall (r : Z), Prop), forall (F_at : @FrechetDerivativeAt.{u,p,z} Scalar zero one add neg sub mul le_rel Product pzero padd pneg psmul pnorm Z zzero zadd zneg zsmul znorm F (pair base_x base_y) dF F_bound F_remainder), forall (P : Prop), forall (mk : forall (partial_x_at : @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y) base_x (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_x_bound partial_x_remainder), forall (partial_y_at : @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x) base_y (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_y_bound partial_y_remainder), P), P

theorem frechet_remainder_def.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (h : X), @Eq.{w} Y (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h) (@vsub.{w} Y yadd yneg (f (xadd point h)) (yadd (f point) (df h))) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun h => @Eq.refl.{w} Y (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)

theorem frechet_derivative_at_intro.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (linear_law : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df), forall (operator_bound_law : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound), forall (remainder_law : forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)), @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun bound => fun remainder_small => fun linear_law => fun operator_bound_law => fun remainder_law => fun (P : Prop) => fun (mk : forall (linear_law : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df), forall (operator_bound_law : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound), forall (remainder_law : forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)), P) => mk linear_law operator_bound_law remainder_law

theorem frechet_derivative_linear_from_at.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun bound => fun remainder_small => fun derivative_at => derivative_at (@LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df) (fun (linear_arg : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df) => fun (bound_arg : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound) => fun (remainder_arg : forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)) => linear_arg)

theorem frechet_derivative_bound_from_at.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun bound => fun remainder_small => fun derivative_at => derivative_at (@OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound) (fun (linear_arg : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df) => fun (bound_arg : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound) => fun (remainder_arg : forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)) => bound_arg)

theorem frechet_derivative_remainder_from_at.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun bound => fun remainder_small => fun derivative_at => fun h => derivative_at (remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)) (fun (linear_arg : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df) => fun (bound_arg : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df bound) => fun (remainder_arg : forall (h : X), remainder_small (@FrechetRemainder.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df h)) => remainder_arg h)

theorem frechet_differentiable_at_intro.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), @FrechetDifferentiableAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun bound => fun remainder_small => fun derivative_at => fun (P : Prop) => fun (mk : forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), P) => mk df bound remainder_small derivative_at

theorem frechet_differentiable_at_elim.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (diff_at : @FrechetDifferentiableAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point), forall (P : Prop), forall (mk : forall (df : forall (h : X), Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), forall (derivative_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df bound remainder_small), P), P :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun diff_at => fun P => fun mk => diff_at P mk

theorem frechet_differentiable_on_apply.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (domain : forall (x : X), Prop), forall (diff_on : @FrechetDifferentiableOn.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f domain), forall (x : X), forall (hx : domain x), @FrechetDifferentiableAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f x :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun domain => fun diff_on => fun x => fun hx => diff_on x hx

theorem derivative_unique_from_args.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (unique_args : @DerivativeUniqueArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point), forall (df_left : forall (h : X), Y), forall (bound_left : Scalar), forall (remainder_left : forall (r : Y), Prop), forall (df_right : forall (h : X), Y), forall (bound_right : Scalar), forall (remainder_right : forall (r : Y), Prop), forall (left_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df_left bound_left remainder_left), forall (right_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df_right bound_right remainder_right), forall (h : X), @Eq.{w} Y (df_left h) (df_right h) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun unique_args => fun df_left => fun bound_left => fun remainder_left => fun df_right => fun bound_right => fun remainder_right => fun left_at => fun right_at => fun h => unique_args df_left bound_left remainder_left df_right bound_right remainder_right left_at right_at h

theorem const_map_def.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (value : Y), forall (x : X), @Eq.{w} Y (@ConstMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm value x) value :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun value => fun x => @Eq.refl.{w} Y (@ConstMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm value x)

theorem zero_map_def.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (h : X), @Eq.{w} Y (@ZeroMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm h) yzero :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun h => @Eq.refl.{w} Y (@ZeroMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm h)

theorem pair_map_def.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (y : Y), forall (z : Z), Product), forall (fst : forall (point : Product), Y), forall (snd : forall (point : Product), Z), forall (f : forall (x : X), Y), forall (g : forall (x : X), Z), forall (point : X), @Eq.{p} Product (@PairMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd f g point) (pair (f point) (g point)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun f => fun g => fun point => @Eq.refl.{p} Product (@PairMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd f g point)

theorem derivative_const_from_args.{u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (args : @DerivativeConstRuleArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm), forall (point : X), forall (value : Y), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm (@ConstMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm value) point (@ZeroMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm) bound remainder_small :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun args => fun point => fun value => fun bound => fun remainder_small => args point value bound remainder_small

theorem derivative_id_from_args.{u,v} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (args : @DerivativeIdRuleArgs.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm), forall (point : Vector), forall (bound : Scalar), forall (remainder_small : forall (r : Vector), Prop), @FrechetDerivativeAt.{u,v,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm Vector vzero vadd vneg smul norm (@LinearId.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm) point (@LinearId.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm) bound remainder_small :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun args => fun point => fun bound => fun remainder_small => args point bound remainder_small

theorem derivative_fst_from_args.{p,u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (args : @DerivativeFstRuleArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (point : Product), forall (bound : Scalar), forall (remainder_small : forall (r : X), Prop), @FrechetDerivativeAt.{u,p,v} Scalar zero one add neg sub mul le_rel Product (@ProductZero.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) X xzero xadd xneg xsmul xnorm fst point fst bound remainder_small :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun args => fun point => fun bound => fun remainder_small => args point bound remainder_small

theorem derivative_snd_from_args.{p,u,v,w} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (a : X), forall (b : X), X), forall (xneg : forall (a : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (a : Y), forall (b : Y), Y), forall (yneg : forall (a : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Product : Sort p), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (args : @DerivativeSndRuleArgs.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd), forall (point : Product), forall (bound : Scalar), forall (remainder_small : forall (r : Y), Prop), @FrechetDerivativeAt.{u,p,w} Scalar zero one add neg sub mul le_rel Product (@ProductZero.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductAdd.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNeg.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductSmul.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) (@ProductNorm.{p,u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Product pair fst snd) Y yzero yadd yneg ysmul ynorm snd point snd bound remainder_small :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Product => fun pair => fun fst => fun snd => fun args => fun point => fun bound => fun remainder_small => args point bound remainder_small

theorem derivative_pair_from_args.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (y : Y), forall (z : Z), Product), forall (fst : forall (point : Product), Y), forall (snd : forall (point : Product), Z), forall (f : forall (x : X), Y), forall (g : forall (x : X), Z), forall (args : @DerivativePairRuleArgs.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd f g), forall (point : X), forall (df : forall (h : X), Y), forall (dg : forall (h : X), Z), forall (f_bound : Scalar), forall (f_remainder : forall (r : Y), Prop), forall (g_bound : Scalar), forall (g_remainder : forall (r : Z), Prop), forall (pair_bound : Scalar), forall (pair_remainder : forall (r : Product), Prop), forall (f_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df f_bound f_remainder), forall (g_at : @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm g point dg g_bound g_remainder), @FrechetDerivativeAt.{u,v,p} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Product pzero padd pneg psmul pnorm (@PairMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd f g) point (@PairMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd df dg) pair_bound pair_remainder :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun f => fun g => fun args => fun point => fun df => fun dg => fun f_bound => fun f_remainder => fun g_bound => fun g_remainder => fun pair_bound => fun pair_remainder => fun f_at => fun g_at => args point df dg f_bound f_remainder g_bound g_remainder pair_bound pair_remainder f_at g_at

theorem derivative_comp_from_args.{u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (f : forall (x : X), Y), forall (g : forall (y : Y), Z), forall (args : @DerivativeCompRuleArgs.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g), forall (point : X), forall (df : forall (h : X), Y), forall (dg : forall (h : Y), Z), forall (f_bound : Scalar), forall (f_remainder : forall (r : Y), Prop), forall (g_bound : Scalar), forall (g_remainder : forall (r : Z), Prop), forall (comp_bound : Scalar), forall (comp_remainder : forall (r : Z), Prop), forall (f_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df f_bound f_remainder), forall (g_at : @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm g (f point) dg g_bound g_remainder), @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g) point (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm df dg) comp_bound comp_remainder :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun f => fun g => fun args => fun point => fun df => fun dg => fun f_bound => fun f_remainder => fun g_bound => fun g_remainder => fun comp_bound => fun comp_remainder => fun f_at => fun g_at => args point df dg f_bound f_remainder g_bound g_remainder comp_bound comp_remainder f_at g_at

theorem partial_x_map_def.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (base_y : Y), forall (x : X), @Eq.{z} Z (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y x) (F (pair x base_y)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun base_y => fun x => @Eq.refl.{z} Z (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y x)

theorem partial_y_map_def.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (base_x : X), forall (y : Y), @Eq.{z} Z (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x y) (F (pair base_x y)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun base_x => fun y => @Eq.refl.{z} Z (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x y)

theorem partial_x_derivative_map_def.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (dF : forall (h : Product), Z), forall (h : X), @Eq.{z} Z (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF h) (dF (pair h yzero)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun dF => fun h => @Eq.refl.{z} Z (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF h)

theorem partial_y_derivative_map_def.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (dF : forall (h : Product), Z), forall (h : Y), @Eq.{z} Z (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF h) (dF (pair xzero h)) :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun dF => fun h => @Eq.refl.{z} Z (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF h)

theorem partial_x_derivative_from_args.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (args : @PartialDerivativeRuleArgs.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F), forall (base_x : X), forall (base_y : Y), forall (dF : forall (h : Product), Z), forall (F_bound : Scalar), forall (F_remainder : forall (r : Z), Prop), forall (partial_x_bound : Scalar), forall (partial_x_remainder : forall (r : Z), Prop), forall (partial_y_bound : Scalar), forall (partial_y_remainder : forall (r : Z), Prop), forall (F_at : @FrechetDerivativeAt.{u,p,z} Scalar zero one add neg sub mul le_rel Product pzero padd pneg psmul pnorm Z zzero zadd zneg zsmul znorm F (pair base_x base_y) dF F_bound F_remainder), @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y) base_x (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_x_bound partial_x_remainder :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun args => fun base_x => fun base_y => fun dF => fun F_bound => fun F_remainder => fun partial_x_bound => fun partial_x_remainder => fun partial_y_bound => fun partial_y_remainder => fun F_at => args base_x base_y dF F_bound F_remainder partial_x_bound partial_x_remainder partial_y_bound partial_y_remainder F_at (@FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y) base_x (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_x_bound partial_x_remainder) (fun (partial_x_at : @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y) base_x (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_x_bound partial_x_remainder) => fun (partial_y_at : @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x) base_y (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_y_bound partial_y_remainder) => partial_x_at)

theorem partial_y_derivative_from_args.{p,u,v,w,z} :
  forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (Product : Sort p), forall (pzero : Product), forall (padd : forall (x : Product), forall (y : Product), Product), forall (pneg : forall (x : Product), Product), forall (psmul : forall (a : Scalar), forall (x : Product), Product), forall (pnorm : forall (x : Product), Scalar), forall (pair : forall (x : X), forall (y : Y), Product), forall (fst : forall (point : Product), X), forall (snd : forall (point : Product), Y), forall (F : forall (point : Product), Z), forall (args : @PartialDerivativeRuleArgs.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F), forall (base_x : X), forall (base_y : Y), forall (dF : forall (h : Product), Z), forall (F_bound : Scalar), forall (F_remainder : forall (r : Z), Prop), forall (partial_x_bound : Scalar), forall (partial_x_remainder : forall (r : Z), Prop), forall (partial_y_bound : Scalar), forall (partial_y_remainder : forall (r : Z), Prop), forall (F_at : @FrechetDerivativeAt.{u,p,z} Scalar zero one add neg sub mul le_rel Product pzero padd pneg psmul pnorm Z zzero zadd zneg zsmul znorm F (pair base_x base_y) dF F_bound F_remainder), @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x) base_y (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_y_bound partial_y_remainder :=
  fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun Product => fun pzero => fun padd => fun pneg => fun psmul => fun pnorm => fun pair => fun fst => fun snd => fun F => fun args => fun base_x => fun base_y => fun dF => fun F_bound => fun F_remainder => fun partial_x_bound => fun partial_x_remainder => fun partial_y_bound => fun partial_y_remainder => fun F_at => args base_x base_y dF F_bound F_remainder partial_x_bound partial_x_remainder partial_y_bound partial_y_remainder F_at (@FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x) base_y (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_y_bound partial_y_remainder) (fun (partial_x_at : @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@PartialXMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_y) base_x (@PartialXDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_x_bound partial_x_remainder) => fun (partial_y_at : @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm (@PartialYMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F base_x) base_y (@PartialYDerivativeMap.{p,u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm Product pzero padd pneg psmul pnorm pair fst snd F dF) partial_y_bound partial_y_remainder) => partial_y_at)