English
A chain rule-type equality holds for mfderiv of the composition with eEF and f.embeddingPiTangent.
Русский
Справедливо правило цепи для mfderiv композиции с eEF и f.embeddingPiTangent.
LaTeX
$$$\text{mfderiv} \; I \; \mathcal I(\mathbb R,\iota \to E\times\mathbb R)\; (eEF \circ f.embeddingPiTangent) = \text{...}$$$
Lean4
theorem comp_embeddingPiTangent_mfderiv (x : M) (hx : x ∈ s) :
((ContinuousLinearMap.fst ℝ E ℝ).comp
(@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))).comp
(mfderiv I 𝓘(ℝ, ι → E × ℝ) f.embeddingPiTangent x) =
mfderiv I I (chartAt H (f.c (f.ind x hx))) x :=
by
set L :=
(ContinuousLinearMap.fst ℝ E ℝ).comp
(@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))
have := L.hasMFDerivAt.comp x (f.embeddingPiTangent.contMDiff.mdifferentiableAt (mod_cast le_top)).hasMFDerivAt
convert hasMFDerivAt_unique this _
refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
refine (f.eventuallyEq_one x hx).mono fun y hy => ?_
simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp', (· ∘ ·), ContinuousLinearMap.coe_fst',
ContinuousLinearMap.proj_apply]
rw [hy, Pi.one_apply, one_smul]
