awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (Function.comp (β := F)
      (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDerivWithin n f s)
have rw₁ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
  (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (Function.comp (β := F)
        (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        (⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
      ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (Function.comp (β := F)
      (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
rw₁ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := F)
          (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
          (⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDerivWithin n f s)
have rw₂ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
  (id ∘ iteratedFDerivWithin 𝕜 n f s)
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (Function.comp (β := F)
      (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
rw₁ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := F)
          (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
          (⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
rw₂ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (id ∘ iteratedFDerivWithin 𝕜 n f s)
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDerivWithin n f s)
have rw₃ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
  (iteratedFDerivWithin 𝕜 n f s)
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) m =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ i : Fin n, m i) (iteratedDerivWithin n f s x)
have rw : Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) m : F)
  ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (i : Fin n) ↦ HSMul.hSMul (β := 𝕜) (m i) 1 : F)
Tactic: rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← ContinuousMultilinearMap.map_smul_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    ‖iteratedDerivWithin n f s x‖
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
  norm.{u_2} (E := F)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    norm.{u_2} (E := F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    ‖iteratedDerivWithin n f s x‖
have rw₁ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
  norm.{u_2} (E := F)
    ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDerivWithin 𝕜 n f s x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
      F)
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    norm.{u_2} (E := F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    norm.{u_2} (E := F)
      ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
          (iteratedFDerivWithin 𝕜 n f s x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
        F)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    ‖iteratedDerivWithin n f s x‖
have rw₂ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (iteratedFDerivWithin 𝕜 n f s x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin 0 f s = f
have h : ∀ (x : 𝕜), iteratedDerivWithin 0 f s x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin 1 f s = derivWithin f s
have h : ∀ (x : 𝕜), iteratedDerivWithin 1 f s x = derivWithin f s x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x
have pos : ∀ (hsx : AccPt x (𝓟 s)), iteratedDerivWithin 1 f s x = derivWithin f s x
Tactic: by_cases hsx : AccPt x (𝓟 s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
pos : ∀ (hsx : AccPt x (𝓟 s)), iteratedDerivWithin 1 f s x = derivWithin f s x
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x
have neg : ∀ (hsx : ¬AccPt x (𝓟 s)), iteratedDerivWithin 1 f s x = derivWithin f s x
Tactic: by_cases hsx : AccPt x (𝓟 s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContinuousOn.{u_1, u_2} (Y := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hdiff :
  ∀ (m : ℕ), (↑m : ℕ∞) < n → DifferentiableOn.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
have Hcont₁ : ∀ (m : ℕ),
  (↑m : ℕ∞) ≤ n →
    ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
      (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Tactic: apply contDiffOn_of_continuousOn_differentiableOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContinuousOn.{u_1, u_2} (Y := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hdiff :
  ∀ (m : ℕ), (↑m : ℕ∞) < n → DifferentiableOn.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hcont₁ :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
        (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
have Hdiff₁ : ∀ (m : ℕ),
  (↑m : ℕ∞) < n →
    DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
      (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Tactic: apply contDiffOn_of_continuousOn_differentiableOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
have h₁ : ∀ (m : ℕ),
  (↑m : ℕ∞) ≤ n →
    DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 m f s) s
Tactic: apply contDiffOn_of_differentiableOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
have rw : ((∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → ContinuousOn (iteratedDerivWithin m f s) s) ∧
    ∀ (m : ℕ), LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
  (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
Tactic: rw [show n = ((n : ℕ∞) : ℕ∞ω) from rfl,
    contDiffOn_iff_continuousOn_differentiableOn_deriv hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin (n + 1) f s = derivWithin (iteratedDerivWithin n f s) s
have h : ∀ (x : 𝕜), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
have pos : ∀ (hxs : AccPt x (𝓟 s)), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
Tactic: by_cases hxs : AccPt x (𝓟 s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
pos : ∀ (hxs : AccPt x (𝓟 s)), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
have neg : ∀ (hxs : ¬AccPt x (𝓟 s)), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
Tactic: by_cases hxs : AccPt x (𝓟 s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
have pos : Eq.{u_2 + 1} (α := F)
  ((((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                (↑(↑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
                      F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
                  F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
                (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) :
              𝕜 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
            (a : 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
          1 :
        (a : (i : Fin n) → 𝕜) → F)
      (Fin.tail (α := fun (i : Fin (n + 1)) ↦ 𝕜) fun (x : Fin (n + 1)) ↦ 1 : (i : Fin n) → 𝕜) :
    F)
  (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
      iteratedFDerivWithin_eq_equiv_comp,
      LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt, derivWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ Eq.{u_2 + 1} (α := F)
    ((((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                  (↑(↑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
                        F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
                    F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
                  (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) :
                𝕜 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
              (a : 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
            1 :
          (a : (i : Fin n) → 𝕜) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ 𝕜) fun (x : Fin (n + 1)) ↦ 1 : (i : Fin n) → 𝕜) :
      F)
    (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have pos : Eq.{u_2 + 1} (α := F)
  (((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n)
            (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1) :
          ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1 :
    F)
  (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
      (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
      (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x
have succ : derivWithin (iteratedDerivWithin n f s) s x =
  ((fun (g : 𝕜 → F) ↦ derivWithin g s) ∘ (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n]) f x
Tactic: rw [iteratedDerivWithin_succ, Function.iterate_succ']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x
have zero : ∀ {x : 𝕜}, iteratedDerivWithin 0 f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[0] f x
Tactic: induction n generalizing x with
  | zero => simp
  | succ n IH =>
    rw [iteratedDerivWithin_succ, Function.iterate_succ']
    exact derivWithin_congr (fun y hy => IH) IH
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
zero : ∀ {x : 𝕜}, iteratedDerivWithin 0 f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[0] f x
⊢ iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x
have succ : ∀ (n : ℕ) (IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x) {x : 𝕜},
  iteratedDerivWithin (n + 1) f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x
Tactic: induction n generalizing x with
  | zero => simp
  | succ n IH =>
    rw [iteratedDerivWithin_succ, Function.iterate_succ']
    exact derivWithin_congr (fun y hy => IH) IH
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin (n + 1) f s = iteratedDerivWithin n (derivWithin f s) s
have h : ∀ (x : 𝕜), iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x
have h : (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] (derivWithin f s) x
Tactic: rw [iteratedDerivWithin_eq_iterate, iteratedDerivWithin_eq_iterate]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s ↔ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s ∧ ContDiffOn 𝕜 1 (iteratedDerivWithin n f s) s
have simp : ((∀ m ≤ n + 1, ContinuousOn (iteratedDerivWithin m f s) s) ∧
    ∀ m < n + 1, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
  ((∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ∧
    DifferentiableOn 𝕜 (iteratedDerivWithin n f s) s ∧ ContinuousOn (iteratedDerivWithin (n + 1) f s) s
Tactic: simp only [contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, hs,
    contDiffOn_one_iff_derivWithin, ← iteratedDerivWithin_succ]