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 :
  ∀ 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)
i : ℕ
h : i ∈ Finset.range (n + 1)
⊢ LE.le (α := ℝ) (↑(n - i)! : ℝ)⁻¹ 1
have h : LE.le (α := ℝ) 1 (↑(n - i)! : ℝ)
Tactic: apply inv_le_one_of_one_le₀
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have have : ∀ (isoF : Fu ≃ₗᵢ[𝕜] F),
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
Tactic: have isoF : Fu ≃ₗᵢ[𝕜] F := LinearIsometryEquiv.ulift 𝕜 F
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have have : ∀ (isoG : Gu ≃ₗᵢ[𝕜] G),
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
Tactic: have isoG : Gu ≃ₗᵢ[𝕜] G := LinearIsometryEquiv.ulift 𝕜 G
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have htu : UniqueDiffOn 𝕜 tu
Tactic: have htu : UniqueDiffOn 𝕜 tu := isoF.toContinuousLinearEquiv.uniqueDiffOn_preimage_iff.2 ht
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have hstu : MapsTo fu s tu
Tactic: have hstu : MapsTo fu s tu := fun y hy ↦ by
    simpa only [fu, tu, mem_preimage, comp_apply, LinearIsometryEquiv.apply_symm_apply] using hst hy
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have Ffu : (isoF : (a : Fu) → F) (fu x) = f x
Tactic: have Ffu : isoF (fu x) = f x := by
    simp only [fu, comp_apply, LinearIsometryEquiv.apply_symm_apply]
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
Tactic: have hfu : ContDiffOn 𝕜 n fu s := isoF.symm.contDiff.comp_contDiffOn (hf.of_le hn)
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Tactic: have hgu : ContDiffOn 𝕜 n gu tu :=
    isoG.symm.contDiff.comp_contDiffOn
      ((hg.of_le hn).comp_continuousLinearMap (isoF : Fu →L[𝕜] F))
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
i : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
have rw : norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
Tactic: rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have Nfu : ∀ (i : ℕ),
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
Tactic: have Nfu : ∀ i, ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖ := fun i ↦ by
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have hD₁ : ∀ (i : ℕ),
  1 ≤ i →
    i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
Tactic: simp_rw [← Nfu] at hD
Cleared hypotheses: hD
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDerivWithin 𝕜 i g t (f x))
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) G)
    (iteratedFDerivWithin 𝕜 i (g ∘ (⇑isoF : (a : Fu) → F)) tu (fu x)) =
  norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDerivWithin 𝕜 i g t (f x))
Tactic: rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ htu (hstu 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) G)
      (iteratedFDerivWithin 𝕜 i (g ∘ (⇑isoF : (a : Fu) → F)) tu (fu x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDerivWithin 𝕜 i g t (f x))
have hx₁ : Membership.mem (α := F) t ((isoF : (a : Fu) → F) (fu x) : F)
Tactic: rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right _ _ ht, Ffu]
-- 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
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
⊢ Membership.mem (α := F) t ((isoF : (a : Fu) → F) (fu x) : F)
have hx₁ : f x ∈ t
Tactic: rw [Ffu]