awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 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))
Tactic: have Ngu : ∀ i,
      ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ := fun i ↦ by
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ htu (hstu hx)]
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right _ _ ht, Ffu]
    rw [Ffu]
    exact hst 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
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))
⊢ 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 hC₁ : ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
Tactic: simp_rw [← Ngu] at hC
Cleared hypotheses: hC
-- 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 : ℝ
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
⊢ gu ∘ fu = (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f
have h : ∀ (x : E), ULift.down.{uF, uG} ((gu ∘ fu) x) = ULift.down.{uF, uG} (((⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f) x)
Tactic: ext x
-- 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 : ℝ
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)
have this : gu ∘ fu = (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f
Tactic: have : gu ∘ fu = isoG.symm ∘ g ∘ f := by
      ext x
      simp only [fu, gu, comp_apply,
        LinearIsometryEquiv.apply_symm_apply]
-- 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 : ℝ
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
⊢ 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)
have 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)
Tactic: rw [this, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ 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
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)
⊢ 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)
have 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)
Tactic: rw [this, 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 : ℝ
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) ≤
    (↑n ! : ℝ) * C * D ^ n
have 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)
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]
-- 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 : ℝ
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.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) Gu) (iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x) ≤
  (↑n ! : ℝ) * C * D ^ n
Tactic: rw [Nfgu]
-- 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 : ℕ
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
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G) (iteratedFDeriv 𝕜 n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C * D ^ n
have 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
Tactic: simp_rw [← iteratedFDerivWithin_univ] at hD ⊢
Cleared hypotheses: hD
-- 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 : ℕ
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
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G) (iteratedFDeriv 𝕜 n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C * D ^ n
have hC₁ : ∀ 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
Cleared hypotheses: hC
-- 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
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
have simp : norm (E := (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G) (ContinuousLinearMap.id 𝕜 (F →L[𝕜] G)) ≤ 1
Tactic: simp only [B, ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.apply]
-- 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
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
have 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‖
Tactic: refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun 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
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
⊢ norm (E := F →L[𝕜] G) ((ContinuousLinearMap.id 𝕜 (F →L[𝕜] G) : (a : F →L[𝕜] G) → F →L[𝕜] G) f : F →L[𝕜] G) ≤ 1 * ‖f‖
have simp : ‖f‖ ≤ ‖f‖
Tactic: simp only [ContinuousLinearMap.coe_id', id, one_mul]