awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℝ
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
Ngu :
  ∀ (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))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
this : gu ∘ fu = (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f
rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 n ((⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f) s x)
rw₁ rw₂ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x)

Tactic:
rw [this, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]

Premises used: LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℝ
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
Ngu :
  ∀ (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))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x)

Tactic:
have Nfgu :
      ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x‖ := by
    have : gu ∘ fu = isoG.symm ∘ g ∘ f := by
      ext x
      simp only [fu, gu, comp_apply,
        LinearIsometryEquiv.apply_symm_apply]
    rw [this, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℝ
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
Ngu :
  ∀ (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))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
Nfgu :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x)
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
⊢ 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:
rw [Nfgu]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℝ
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
Ngu :
  ∀ (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))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
Nfgu :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
norm_iteratedFDerivWithin_comp_le_aux hgu hfu htu hs hstu hx hC hD

Premises used: norm_iteratedFDerivWithin_comp_le_aux
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℝ
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
Ngu :
  ∀ (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))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
Nfgu :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
exact norm_iteratedFDerivWithin_comp_le_aux hgu hfu htu hs hstu hx hC hD

Premises used: norm_iteratedFDerivWithin_comp_le_aux
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℕ
N : ℕ∞ω
t : Set F
ht : range f ⊆ t
ht' : UniqueDiffOn 𝕜 t
hg : ContDiffOn 𝕜 N g t
hf : ContDiff 𝕜 N f
hn : (↑n : ℕ∞ω) ≤ N
x : E
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) (iteratedFDeriv 𝕜 i f x) ≤ D ^ i
simp_rw :
  ∀
    (hD :
      ∀ (i : ℕ),
        1 ≤ i →
          i ≤ n →
            norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
                (iteratedFDerivWithin 𝕜 i f univ x) ≤
              D ^ i),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
        (iteratedFDerivWithin 𝕜 n (g ∘ f) univ x) ≤
      (↑n ! : ℝ) * C * D ^ n
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G) (iteratedFDeriv 𝕜 n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
simp_rw [← iteratedFDerivWithin_univ] at hD ⊢

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℕ
N : ℕ∞ω
t : Set F
ht : range f ⊆ t
ht' : UniqueDiffOn 𝕜 t
hg : ContDiffOn 𝕜 N g t
hf : ContDiff 𝕜 N f
hn : (↑n : ℕ∞ω) ≤ N
x : E
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 univ x) ≤
          D ^ i
⊢ MapsTo f univ t

Tactic:
simp [mapsTo_iff_subset_preimage, ht]

Premises used: Set.mapsTo_iff_subset_preimage
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℕ
N : ℕ∞ω
t : Set F
ht : range f ⊆ t
ht' : UniqueDiffOn 𝕜 t
hg : ContDiffOn 𝕜 N g t
hf : ContDiff 𝕜 N f
hn : (↑n : ℕ∞ω) ≤ N
x : E
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 univ x) ≤
          D ^ i
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) univ x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
exact norm_iteratedFDerivWithin_comp_le hg hf.contDiffOn hn ht' uniqueDiffOn_univ
    (by simp [mapsTo_iff_subset_preimage, ht]) (mem_univ x) hC hD

Premises used: ContDiff.contDiffOn, uniqueDiffOn_univ, norm_iteratedFDerivWithin_comp_le, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℕ
N : ℕ∞ω
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : (↑n : ℕ∞ω) ≤ N
x : E
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDeriv 𝕜 i g (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x) ≤ D ^ i
⊢ ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g univ (f x)) ≤
      C

Tactic:
simp_rw [← iteratedFDerivWithin_univ] at hC

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℕ
N : ℕ∞ω
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : (↑n : ℕ∞ω) ≤ N
x : E
C D : ℝ
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x) ≤ D ^ i
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g univ (f x)) ≤
      C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G) (iteratedFDeriv 𝕜 n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
norm_iteratedFDeriv_comp_le' (subset_univ _) uniqueDiffOn_univ hg.contDiffOn hf hn x hC hD

Premises used: norm_iteratedFDeriv_comp_le', ContDiff.contDiffOn, Set.subset_univ, uniqueDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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 : ℕ
N : ℕ∞ω
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : (↑n : ℕ∞ω) ≤ N
x : E
C D : ℝ
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x) ≤ D ^ i
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g univ (f x)) ≤
      C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G) (iteratedFDeriv 𝕜 n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
exact norm_iteratedFDeriv_comp_le' (subset_univ _) uniqueDiffOn_univ hg.contDiffOn hf hn x hC hD

Premises used: norm_iteratedFDeriv_comp_le', ContDiff.contDiffOn, Set.subset_univ, uniqueDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
simp : norm (E := (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G) (ContinuousLinearMap.id 𝕜 (F →L[𝕜] G)) ≤ 1
⊢ ‖B‖ ≤ 1

Tactic:
simp only [B, ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.apply]

Premises used: ContinuousLinearMap.apply, ContinuousLinearMap.opNorm_flip
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G) (ContinuousLinearMap.id 𝕜 (F →L[𝕜] G)) ≤ 1

Tactic:
ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun f => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, zero_le_one
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
refine :
  ∀ (f : F →L[𝕜] G),
    norm (E := F →L[𝕜] G) ((ContinuousLinearMap.id 𝕜 (F →L[𝕜] G) : (a : F →L[𝕜] G) → F →L[𝕜] G) f : F →L[𝕜] G) ≤ 1 * ‖f‖
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G) (ContinuousLinearMap.id 𝕜 (F →L[𝕜] G)) ≤ 1

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun f => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, zero_le_one
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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
f_1 : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f_1 s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
f : F →L[𝕜] G
simp : ‖f‖ ≤ ‖f‖
⊢ norm (E := F →L[𝕜] G) ((ContinuousLinearMap.id 𝕜 (F →L[𝕜] G) : (a : F →L[𝕜] G) → F →L[𝕜] G) f : F →L[𝕜] G) ≤ 1 * ‖f‖

Tactic:
simp only [ContinuousLinearMap.coe_id', id, one_mul]

Premises used: id, ContinuousLinearMap.coe_id', one_mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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
f_1 : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f_1 s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
f : F →L[𝕜] G
⊢ ‖f‖ ≤ ‖f‖

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
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
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
⊢ ‖B‖ ≤ 1

Tactic:
have hB : ‖B‖ ≤ 1 := by
    simp only [B, ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.apply]
    refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun f => ?_
    simp only [ContinuousLinearMap.coe_id', id, one_mul]
    rfl