awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ i
this :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (j + 1)) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 (j + 1) g t (f x))
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)) ≤
    C
have hC₁ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (j + 1)) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 (j + 1) g t (f x)) ≤ C
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x) ≤
    (↑(n + 1)! : ℝ) * C * D ^ (n + 1)
have I : ∀ i ∈ Finset.range (n + 1),
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
    (↑i ! : ℝ) * C * D ^ i
Tactic: have I : ∀ i ∈ Finset.range (n + 1),
      ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ i ! * C * D ^ i := by
    intro i hi
    simp only [Finset.mem_range_succ_iff] at hi
    apply IH i hi
    · apply hg.fderivWithin ht
      grw [Nat.cast_succ, hi]
    · apply hf.of_le (Nat.cast_le.2 (hi.trans n.le_succ))
    · intro j hj
      have : ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ =
          ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖ := by
        rw [iteratedFDerivWithin_succ_eq_comp_right ht (hst hx), comp_apply,
          LinearIsometryEquiv.norm_map]
      rw [this]
      exact hC (j + 1) (add_le_add (hj.trans hi) le_rfl)
    · intro j hj h'j
      exact hD j hj (h'j.trans (hi.trans n.le_succ))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
i : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
      (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
    D ^ (n - i + 1)
have this : norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n - i + 1)) ↦ E) Fu)
    (iteratedFDerivWithin 𝕜 (n - i + 1) f s x) ≤
  D ^ (n - i + 1)
Tactic: have : ‖iteratedFDerivWithin 𝕜 (n - i + 1) f s x‖ ≤ D ^ (n - i + 1) :=
      hD (n - i + 1) (by simp) (Nat.succ_le_succ tsub_le_self)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x) ≤
    (↑(n + 1)! : ℝ) * C * D ^ (n + 1)
have J : ∀ (i : ℕ),
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
      (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
    D ^ (n - i + 1)
Tactic: have J : ∀ i, ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1) := by
    intro i
    have : ‖iteratedFDerivWithin 𝕜 (n - i + 1) f s x‖ ≤ D ^ (n - i + 1) :=
      hD (n - i + 1) (by simp) (Nat.succ_le_succ tsub_le_self)
    simpa [iteratedFDerivWithin_succ_eq_comp_right hs hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
J :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
        (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
      D ^ (n - i + 1)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : E) ↦
          (((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
                  (fderivWithin 𝕜 g t (f y)) :
                (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
              (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
            (fderivWithin 𝕜 f s y))
        s x)
have e_a : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
  (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)
  (iteratedFDerivWithin 𝕜 n
    (fun (y : E) ↦
      (((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
              (fderivWithin 𝕜 g t (f y)) :
            (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
          (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
        (fderivWithin 𝕜 f s y))
    s x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
J :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
        (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
      D ^ (n - i + 1)
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
    (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)
    (iteratedFDerivWithin 𝕜 n
      (fun (y : E) ↦
        (((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
                (fderivWithin 𝕜 g t (f y)) :
              (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
            (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
          (fderivWithin 𝕜 f s y))
      s x)
have e_a : ∀ (y : E) (hy : y ∈ s),
  Eq (α := E →L[𝕜] Gu) (fderivWithin 𝕜 (g ∘ f) s y)
    ((((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
            (fderivWithin 𝕜 g t (f y)) :
          (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
        (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
      (fderivWithin 𝕜 f s y))
Tactic: refine iteratedFDerivWithin_congr (fun y hy => ?_) hx _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
J :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
        (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
      D ^ (n - i + 1)
y : E
hy : y ∈ s
⊢ Eq (α := E →L[𝕜] Gu) (fderivWithin 𝕜 (g ∘ f) s y)
    ((((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
            (fderivWithin 𝕜 g t (f y)) :
          (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
        (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
      (fderivWithin 𝕜 f s y))
have apply : DifferentiableWithinAt 𝕜 g t (f y)
Tactic: apply fderivWithin_comp _ _ _ hst (hs y hy)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
J :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
        (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
      D ^ (n - i + 1)
y : E
hy : y ∈ s
apply : DifferentiableWithinAt 𝕜 g t (f y)
⊢ Eq (α := E →L[𝕜] Gu) (fderivWithin 𝕜 (g ∘ f) s y)
    ((((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
            (fderivWithin 𝕜 g t (f y)) :
          (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
        (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
      (fderivWithin 𝕜 f s y))
have apply₁ : DifferentiableWithinAt 𝕜 f s y
Tactic: apply fderivWithin_comp _ _ _ hst (hs y hy)