Analysis II (Tao, 2022) -- Chapter 06 -- Section 04 -- Part 1

section Chap06section Section04

Theorem 6.3 (Several variable calculus chain rule): let and , , and . If Unknown identifier `x₀`x₀ is an interior point of Unknown identifier `E`E and Unknown identifier `f`f is differentiable at Unknown identifier `x₀`x₀, and if Unknown identifier `f`f x₀ is an interior point of Unknown identifier `F`F and Unknown identifier `g`g is differentiable at Unknown identifier `f`f x₀, then Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f is differentiable at Unknown identifier `x₀`x₀ and .

theorem severalVariableCalculus_chainRule
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (unused variable `h_map`

Note: This linter can be disabled with `set_option linter.unusedVariables false`h_map : Set.MapsTo f E F)
    (unused variable `hx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hx0 : x0 ∈ interior E)
    (hf : DifferentiableAt ℝ f x0)
    (unused variable `hfx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hfx0 : f x0 ∈ interior F)
    (hg : DifferentiableAt ℝ g (f x0)) :
    DifferentiableAt ℝ (g ∘ f) x0 ∧
      fderiv ℝ (g ∘ f) x0 = (fderiv ℝ g (f x0)).comp (fderiv ℝ f x0) := by
  constructor
  · exact hg.comp x0 hf
  · simpa using fderiv_comp x0 hg hf

Helper for Theorem 6.4: a matrix identity follows from the corresponding within-derivative composition identity.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  rw [hcomp]
  simpa using
    (LinearMap.toMatrix_comp
      (Pi.basisFun ℝ (Fin n))
      (Pi.basisFun ℝ (Fin m))
      (Pi.basisFun ℝ (Fin p))
      (fderivWithin ℝ g F (f x0)).toLinearMap
      (fderivWithin ℝ f E x0).toLinearMap)

Helper for Theorem 6.4: the matrix identity in the chain-rule statement is equivalent to the corresponding equality of selected within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_iff_fderivWithin_comp
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ} :
    (LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap) ↔
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  constructor
  · intro hMatrix
    have hLinearEq :
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
          (fderivWithin ℝ g F (f x0)).toLinearMap.comp
            (fderivWithin ℝ f E x0).toLinearMap := by
      apply (LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))).injective
      calc
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ (g ∘ f) E x0).toLinearMap
            =
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
              (fderivWithin ℝ g F (f x0)).toLinearMap *
            LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
              (fderivWithin ℝ f E x0).toLinearMap := hMatrix
        _ =
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
            ((fderivWithin ℝ g F (f x0)).toLinearMap.comp
              (fderivWithin ℝ f E x0).toLinearMap) := by
          simpa using
            (LinearMap.toMatrix_comp
              (Pi.basisFun ℝ (Fin n))
              (Pi.basisFun ℝ (Fin m))
              (Pi.basisFun ℝ (Fin p))
              (fderivWithin ℝ g F (f x0)).toLinearMap
              (fderivWithin ℝ f E x0).toLinearMap).symm
    ext x i
    simpa using congrArg (fun L : (Fin n → ℝ) →ₗ[ℝ] (Fin p → ℝ) => L x i) hLinearEq
  · intro hcomp
    exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
        hcomp

Helper for Theorem 6.4: composing the selected within-derivatives of Unknown identifier `g`g and Unknown identifier `f`f gives a within-derivative of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f.

theorem helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0)) :
    HasFDerivWithinAt (g ∘ f)
      ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
  exact hg.hasFDerivWithinAt.comp x0 hf.hasFDerivWithinAt hMaps

Helper for Theorem 6.4: on a UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt set, any two within-derivative witnesses for the same map at the same point are equal.

theorem helperForTheorem_6_4_matrixForm_chainRule_eq_of_two_hasFDerivWithinAt_of_uniqueDiff
    {n p : ℕ}
    {E : Set (Fin n → ℝ)}
    {h : (Fin n → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    {L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)}
    (hL1 : HasFDerivWithinAt h L1 E x0)
    (hL2 : HasFDerivWithinAt h L2 E x0)
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    L1 = L2 := by
  have hEq1 : fderivWithin ℝ h E x0 = L1 := by
    exact hL1.fderivWithin hUnique
  have hEq2 : fderivWithin ℝ h E x0 = L2 := by
    exact hL2.fderivWithin hUnique
  exact hEq1.symm.trans hEq2

Helper for Theorem 6.4: UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt provides a canonicity principle for within-derivative witnesses at a fixed point.

theorem helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_canonicity_of_uniqueDiff
    {n p : ℕ}
    {E : Set (Fin n → ℝ)}
    {h : (Fin n → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
      HasFDerivWithinAt h L1 E x0 →
      HasFDerivWithinAt h L2 E x0 →
      L1 = L2 := by
  intro L1 L2 hL1 hL2
  exact
    helperForTheorem_6_4_matrixForm_chainRule_eq_of_two_hasFDerivWithinAt_of_uniqueDiff
      hL1 hL2 hUnique

Helper for Theorem 6.4: to prove the selected within-derivative composition identity, it is enough to have the two derivative witnesses and a canonicity principle identifying any two such witnesses.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_twoHasFDerivWithinAt_witnesses_and_canonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hDerivSelected :
      HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0)
    (hDerivComp :
      HasFDerivWithinAt (g ∘ f)
        ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0)
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  exact hCanonicity _ _ hDerivSelected hDerivComp

Helper for Theorem 6.4: under UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt, the selected within-derivative of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f agrees with the composition of selected within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_uniqueDiff_from_selectedWithinDerivatives
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  have hDerivSelected :
      HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 := by
    exact (hg.comp x0 hf hMaps).hasFDerivWithinAt
  have hDerivComp :
      HasFDerivWithinAt (g ∘ f)
        ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives
        hMaps hf hg
  have hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2 := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_canonicity_of_uniqueDiff
        hUnique
  exact
    helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_twoHasFDerivWithinAt_witnesses_and_canonicity
      hDerivSelected hDerivComp hCanonicity

Helper for Theorem 6.4: under UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt, the within-derivative matrix of a composition is the product of within-derivative matrices.

theorem helperForTheorem_6_4_matrixForm_chainRule_of_uniqueDiff
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_uniqueDiff_from_selectedWithinDerivatives
        hMaps hf hg hUnique
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: under UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt, both the within-set chain-rule differentiability and the matrix identity hold.

theorem helperForTheorem_6_4_matrixForm_chainRule_conclusion_of_uniqueDiff
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  refine ⟨?_, ?_⟩
  · exact hg.comp x0 hf hMaps
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_of_uniqueDiff
        hMaps hf hg hUnique

Helper for Theorem 6.4: the within-set differentiability conclusion for the composition Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f does not require UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt.

theorem helperForTheorem_6_4_matrixForm_chainRule_differentiableWithin
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0)) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 := by
  exact hg.comp x0 hf hMaps

Helper for Theorem 6.4: under UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt, the matrix identity in Theorem 6.4 is obtained from the corresponding conjunction helper.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_uniqueDiff
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    (helperForTheorem_6_4_matrixForm_chainRule_conclusion_of_uniqueDiff
      hMaps hf hg hUnique
    ).2

Helper for Theorem 6.4: with the exact hypotheses of Unknown identifier `matrixForm_chainRule`matrixForm_chainRule, the matrix identity follows in the UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_uniqueDiff_mainHypotheses
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (unused variable `hx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hx0 : x0 ∈ E)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (unused variable `hfx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hfx0 : f x0 ∈ F)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_uniqueDiff
      hMaps hf hg hUnique

Helper for Theorem 6.4: if Unknown identifier `f`f has zero within-derivative at Unknown identifier `x0`x0, then the matrix identity for the chain rule holds.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hZeroDerivF : HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  have hZeroDerivComp :
      HasFDerivWithinAt (g ∘ f) (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) E x0 := by
    simpa using (hg.hasFDerivWithinAt.comp x0 hZeroDerivF hMaps)
  have hfderivWithinFZero :
      fderivWithin ℝ f E x0 = (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) := by
    simp [fderivWithin, hZeroDerivF]
  have hfderivWithinCompZero :
      fderivWithin ℝ (g ∘ f) E x0 = (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) := by
    simp [fderivWithin, hZeroDerivComp]
  rw [hfderivWithinCompZero, hfderivWithinFZero]
  simp

Helper for Theorem 6.4: if either UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt holds at Unknown identifier `x0`x0 or Unknown identifier `f`f has zero within-derivative at Unknown identifier `x0`x0, then the selected within-derivative of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f is the composition of selected within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_uniqueDiff_or_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUniqueOrZero :
      UniqueDiffWithinAt ℝ E x0 ∨
        HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  rcases hUniqueOrZero with hUnique | hZeroDerivF
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_uniqueDiff_from_selectedWithinDerivatives
        hMaps hf hg hUnique
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_hasFDerivWithinAt_zero
        hMaps hg hZeroDerivF

Helper for Theorem 6.4: if Unknown identifier `f`f has zero within-derivative at Unknown identifier `x0`x0, then the matrix identity for the chain rule holds.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hZeroDerivF : HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_hasFDerivWithinAt_zero
        hMaps hg hZeroDerivF
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: if Unknown identifier `g`g has zero within-derivative at Unknown identifier `f`f x0, then the selected within-derivative of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f equals the composition of selected within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_hasFDerivWithinAt_zero_right
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hZeroDerivG :
      HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  have hZeroDerivComp :
      HasFDerivWithinAt (g ∘ f) (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) E x0 := by
    simpa using (hZeroDerivG.comp x0 hf.hasFDerivWithinAt hMaps)
  have hfderivWithinCompZero :
      fderivWithin ℝ (g ∘ f) E x0 = (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) := by
    simp [fderivWithin, hZeroDerivComp]
  have hfderivWithinGZero :
      fderivWithin ℝ g F (f x0) = (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) := by
    simp [fderivWithin, hZeroDerivG]
  rw [hfderivWithinCompZero, hfderivWithinGZero]
  simp

Helper for Theorem 6.4: if Unknown identifier `g`g has zero within-derivative at Unknown identifier `f`f x0, then the matrix identity for the chain rule holds.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_right
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hZeroDerivG :
      HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_hasFDerivWithinAt_zero_right
        hMaps hf hZeroDerivG
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f, both the selected within-derivative and the composition of selected within-derivatives are valid within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_twoHasFDerivWithinAt_witnesses
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0)) :
    HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 ∧
      HasFDerivWithinAt (g ∘ f)
        ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
  refine ⟨?_, ?_⟩
  · exact (hg.comp x0 hf hMaps).hasFDerivWithinAt
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives
        hMaps hf hg

Helper for Theorem 6.4: if zero is not a within-derivative and Unknown identifier `h`h is within-differentiable at Unknown identifier `x0`x0, then fderivWithin.{u_4, u_5, u_6} (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : E →L[𝕜] FfderivWithin is the derivative selected by Classical.choose.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : αClassical.choose from that differentiability witness.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_eq_choose_of_not_hasFDerivWithinAt_zero
    {n p : ℕ}
    {E : Set (Fin n → ℝ)}
    {h : (Fin n → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hh : DifferentiableWithinAt ℝ h E x0)
    (hNotZeroDerivH :
      ¬ HasFDerivWithinAt h (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) E x0) :
    fderivWithin ℝ h E x0 = Classical.choose hh := by
  simp [fderivWithin, hNotZeroDerivH, hh]

Helper for Theorem 6.4: when zero is not a valid within-derivative for Unknown identifier `f`f and Unknown identifier `g`g, the composition of selected within-derivatives is itself a within-derivative of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f.

theorem helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives_of_eq_choose
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hfEqChoose : fderivWithin ℝ f E x0 = Classical.choose hf)
    (hgEqChoose : fderivWithin ℝ g F (f x0) = Classical.choose hg) :
    HasFDerivWithinAt (g ∘ f)
      ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
  rw [hfEqChoose, hgEqChoose]
  exact (Classical.choose_spec hg).comp x0 (Classical.choose_spec hf) hMaps

theorem helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives_of_not_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    HasFDerivWithinAt (g ∘ f)
      ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
  have hfEqChoose :
      fderivWithin ℝ f E x0 = Classical.choose hf := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_eq_choose_of_not_hasFDerivWithinAt_zero
        hf hNotZeroDerivF
  have hgEqChoose :
      fderivWithin ℝ g F (f x0) = Classical.choose hg := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_eq_choose_of_not_hasFDerivWithinAt_zero
        hg hNotZeroDerivG
  exact
    helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives_of_eq_choose
      hMaps hf hg hfEqChoose hgEqChoose

Helper for Theorem 6.4: when zero is not a within-derivative for both Unknown identifier `f`f and Unknown identifier `g`g, the selected within-derivative of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f and the composition of the selected within-derivatives are both valid within-derivative witnesses.

theorem helperForTheorem_6_4_matrixForm_chainRule_twoHasFDerivWithinAt_witnesses_of_not_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 ∧
      HasFDerivWithinAt (g ∘ f)
        ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
  refine ⟨?_, ?_⟩
  · exact (hg.comp x0 hf hMaps).hasFDerivWithinAt
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives_of_not_hasFDerivWithinAt_zero
        hMaps hf hg hNotZeroDerivF hNotZeroDerivG

theorem helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_selectedWitness_of_not_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 := by
  exact
    (helperForTheorem_6_4_matrixForm_chainRule_twoHasFDerivWithinAt_witnesses_of_not_hasFDerivWithinAt_zero
      hMaps hf hg hNotZeroDerivF hNotZeroDerivG).1

Helper for Theorem 6.4: when zero is not a within-derivative for both Unknown identifier `f`f and Unknown identifier `g`g, the composition of selected within-derivatives is a valid within-derivative witness for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f.

theorem helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_compWitness_of_not_hasFDerivWithinAt_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    HasFDerivWithinAt (g ∘ f)
      ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
  exact
    (helperForTheorem_6_4_matrixForm_chainRule_twoHasFDerivWithinAt_witnesses_of_not_hasFDerivWithinAt_zero
      hMaps hf hg hNotZeroDerivF hNotZeroDerivG).2

Helper for Theorem 6.4: if Unknown identifier `f`f is differentiable within Unknown identifier `E`E at Unknown identifier `x0`x0 and Unknown identifier `f`f does not admit zero as a within-derivative there, then the selected within-derivative fderivWithin.{u_4, u_5, u_6} (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : E →L[𝕜] FfderivWithin is nonzero.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_ne_zero_of_not_hasFDerivWithinAt_zero
    {n m : ℕ}
    {E : Set (Fin n → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {x0 : Fin n → ℝ}
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0) :
    fderivWithin ℝ f E x0 ≠ (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) := by
  intro hEqZero
  apply hNotZeroDerivF
  exact hEqZero ▸ hf.hasFDerivWithinAt

Helper for Theorem 6.4: in the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch, once the selected within-derivative composition identity is available, the matrix identity follows immediately.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_from_fderivWithin_comp
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: if Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f admits zero as a within-derivative and the composition of selected within-derivatives is also zero, then the matrix identity follows immediately.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_and_comp_eq_zero
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hZeroDerivComp :
      HasFDerivWithinAt (g ∘ f) (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) E x0)
    (hCompZero :
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) =
        (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ))) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hfderivWithinCompZero :
      fderivWithin ℝ (g ∘ f) E x0 = (0 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ)) := by
    simp [fderivWithin, hZeroDerivComp]
  rw [hfderivWithinCompZero, ← hCompZero]
  simpa using
    (LinearMap.toMatrix_comp
      (Pi.basisFun ℝ (Fin n))
      (Pi.basisFun ℝ (Fin m))
      (Pi.basisFun ℝ (Fin p))
      (fderivWithin ℝ g F (f x0)).toLinearMap
      (fderivWithin ℝ f E x0).toLinearMap)

Helper for Theorem 6.4: if zero is excluded as a within-derivative for Unknown identifier `f`f and Unknown identifier `g`g, then any canonicity principle for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f identifies the selected within-derivative with the composed one.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_not_hasFDerivWithinAt_zero_and_canonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  have hDerivSelected :
      HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_selectedWitness_of_not_hasFDerivWithinAt_zero
        hMaps hf hg hNotZeroDerivF hNotZeroDerivG
  have hDerivComp :
      HasFDerivWithinAt (g ∘ f)
        ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_compWitness_of_not_hasFDerivWithinAt_zero
        hMaps hf hg hNotZeroDerivF hNotZeroDerivG
  exact
    helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_twoHasFDerivWithinAt_witnesses_and_canonicity
      hDerivSelected hDerivComp hCanonicity

Helper for Theorem 6.4: assuming canonicity for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f, the selected within-derivative composition identity follows by splitting on the two zero-derivative fallback branches.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_canonicity_by_zeroFallbackSplit
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  by_cases hZeroDerivF : HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_uniqueDiff_or_hasFDerivWithinAt_zero
        hMaps hf hg (Or.inr hZeroDerivF)
  · by_cases hZeroDerivG :
        HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)
    · exact
        helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_hasFDerivWithinAt_zero_right
          hMaps hf hZeroDerivG
    · exact
        helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_not_hasFDerivWithinAt_zero_and_canonicity
          hMaps hf hg hZeroDerivF hZeroDerivG hCanonicity

Helper for Theorem 6.4: in the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch with zero within-derivatives excluded for Unknown identifier `f`f and Unknown identifier `g`g, the matrix identity follows from the same canonicity principle used to identify derivative witnesses.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_not_hasFDerivWithinAt_zero_and_canonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_not_hasFDerivWithinAt_zero_and_canonicity
        hMaps hf hg hNotZeroDerivF hNotZeroDerivG hCanonicity
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_from_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: once canonicity for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f is available, the matrix identity follows by splitting on whether Unknown identifier `f`f or Unknown identifier `g`g admit the zero within-derivative at the relevant basepoints.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_canonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_canonicity_by_zeroFallbackSplit
        hMaps hf hg hCanonicity
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_from_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: once the two zero-derivative fallback branches are excluded, proving the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt matrix identity reduces to a canonicity statement for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_nonzeroFallbacks_reducedToCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    (∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
      HasFDerivWithinAt (g ∘ f) L1 E x0 →
      HasFDerivWithinAt (g ∘ f) L2 E x0 →
      L1 = L2) →
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  intro hCanonicity
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_not_hasFDerivWithinAt_zero_and_canonicity
      hMaps hf hg hNotZeroDerivF hNotZeroDerivG hCanonicity

Helper for Theorem 6.4: once the two zero-derivative fallback branches are excluded, any supplied canonicity principle for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f yields the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt matrix identity directly.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_nonzeroFallbacks_of_canonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hNotZeroDerivF :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0)
    (hNotZeroDerivG :
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_nonzeroFallbacks_reducedToCanonicity
      hMaps hf hg hNotZeroDerivF hNotZeroDerivG hCanonicity

Helper for Theorem 6.4: a witness-form matrix identity for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f upgrades to the selected-fderivWithin.{u_4, u_5, u_6} (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : E →L[𝕜] FfderivWithin matrix identity once within-derivative witnesses are canonical at Unknown identifier `x0`x0.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_witnessForm_and_canonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hDiffComp : DifferentiableWithinAt ℝ (g ∘ f) E x0)
    (hWitness :
      ∃ L : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L E x0 ∧
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
              L.toLinearMap =
            LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
                (fderivWithin ℝ g F (f x0)).toLinearMap *
              LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
                (fderivWithin ℝ f E x0).toLinearMap)
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  rcases hWitness with ⟨L, hLDeriv, hLMatrix⟩
  have hSelectedDeriv :
      HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 := by
    exact hDiffComp.hasFDerivWithinAt
  have hSelectedEq : fderivWithin ℝ (g ∘ f) E x0 = L := by
    exact hCanonicity _ _ hSelectedDeriv hLDeriv
  simpa [hSelectedEq] using hLMatrix

end Section04end Chap06