awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
⊢ ∃ (u : Set E),
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
have rcases : ∀ (u : Set E)
  (hu :
    ∀ ⦃x : Set E⦄,
      x ∈ 𝒫 (u ∩ s) →
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) x ∧
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' x))
  (hxu : x ∈ u) (huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u),
  ∃ (u : Set E),
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
Tactic: rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂)
      with ⟨u, ⟨hxu, huo⟩, hu⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)
have obtain : ∀ (u : Set E) (hxu : x ∈ u) (huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u)
  (hfu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u))
  (hgu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)
Tactic: obtain ⟨u, hxu, huo, hfu, hgu⟩ : ∃ u, x ∈ u ∧ IsOpen u ∧
      HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
      HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u)) := by
    have hxt : f x ∈ t := hst.self_of_nhdsWithin hxs
    have hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] (f x)) :=
      tendsto_nhdsWithin_iff.mpr ⟨hf.continuousWithinAt, hst⟩
    have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
      hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi
    have H₂ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' u) :=
      hf_tendsto.image_smallSets.eventually (hg.eventually_hasFTaylorSeriesUpToOn ht hxt hi)
    rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂)
      with ⟨u, ⟨hxu, huo⟩, hu⟩
    exact ⟨u, hxu, huo, hu (by simp [inter_comm])⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDeriv 𝕜 i (g ∘ f) x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeries 𝕜 g (f x)) (ftaylorSeries 𝕜 f x) i)
have simp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
  (iteratedFDerivWithin 𝕜 i (g ∘ f) univ x)
  (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g univ (f x)) (ftaylorSeriesWithin 𝕜 f univ x) i)
Tactic: simp only [← iteratedFDerivWithin_univ, ← ftaylorSeriesWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
hi : (↑(i + 1) : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ LT.lt (α := ℕ∞ω) (↑i : ℕ∞ω) (↑(i + 1) : ℕ∞ω)
have norm_cast : i < i + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
hi : (↑(i + 1) : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 (i + 1) c s x : (a : (i : Fin (i + 1)) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G)
        u :
      G)
have hi₁ : (↑i : ℕ∞ω) < n
Tactic: replace hi : (i : ℕ∞ω) < n := lt_of_lt_of_le (by norm_cast; simp) hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 (i + 1) c s x : (a : (i : Fin (i + 1)) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G)
        u :
      G)
have h_deriv_apply : DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
  (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
Tactic: have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 (i + 1) c s x : (a : (i : Fin (i + 1)) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G)
        u :
      G)
have h_deriv : DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s) s
Tactic: have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
      hc.differentiableOn_iteratedFDerivWithin hi hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 (i + 1) c s x : (a : (i : Fin (i + 1)) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G)
        u :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
        (a : (i : Fin i) → E) → G)
      (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
    G)
  ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                    (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                  (m 0) :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
              (a : (i : Fin i) → E) → F →L[𝕜] G)
            (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
          F →L[𝕜] G) :
        (a : F) → G)
      u :
    G)
Tactic: simp only [iteratedFDerivWithin_succ_apply_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  ((fderivWithin 𝕜
          (fun (y : E) ↦
            (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s y : (a : (i : Fin i) → E) → G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
          s x :
        (a : E) → G)
      (m 0) :
    G)
  ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                    (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                  (m 0) :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
              (a : (i : Fin i) → E) → F →L[𝕜] G)
            (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
          F →L[𝕜] G) :
        (a : F) → G)
      u :
    G)
Tactic: rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
⊢ Eq.{u_4 + 1} (α := G)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s y : (a : (i : Fin i) → E) → G)
                (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
            s x :
          (a : E) → G)
        (m 0) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  ((fderivWithin 𝕜
          (fun (x : E) ↦
            (((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G)
                    (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
                  F →L[𝕜] G) :
                (a : F) → G)
              u)
          s x :
        (a : E) → G)
      (m 0) :
    G)
  ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                    (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                  (m 0) :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
              (a : (i : Fin i) → E) → F →L[𝕜] G)
            (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
          F →L[𝕜] G) :
        (a : F) → G)
      u :
    G)
Tactic: rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜
                  (fun (y : E) ↦
                    (iteratedFDerivWithin 𝕜 i c s y : (a : (i : Fin i) → E) → F →L[𝕜] G)
                      (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
                  s x :
                (a : E) → F →L[𝕜] G)
              (m 0) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
have succ : Eq.{u_4 + 1} (α := G)
  ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                    (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                  (m 0) :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
              (a : (i : Fin i) → E) → F →L[𝕜] G)
            (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
          F →L[𝕜] G) :
        (a : F) → G)
      u :
    G)
  ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                    (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                  (m 0) :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
              (a : (i : Fin i) → E) → F →L[𝕜] G)
            (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
          F →L[𝕜] G) :
        (a : F) → G)
      u :
    G)
Tactic: rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : F
m : Fin i → E
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
have zero : ∀ (hi : (↑0 : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin 0 → E},
  Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin 0) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 0 c s x : (a : (i : Fin 0) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
Tactic: induction i generalizing x with
  | zero => simp
  | succ i ih =>
    replace hi : (i : ℕ∞ω) < n := lt_of_lt_of_le (by norm_cast; simp) hi
    have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
    have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
      hc.differentiableOn_iteratedFDerivWithin hi hs
    simp only [iteratedFDerivWithin_succ_apply_left]
    rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
    rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
    rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
      (differentiableWithinAt_const u)]
    rw [fderivWithin_const_apply]
    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
    rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]
Cleared hypotheses: i, hi, x, hx, m