awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n_1 : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn :
  ∀ (h : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x),
    (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
      (iteratedFDerivWithin 𝕜 n f s)
h : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s x
t₀ : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x
t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y
a : E
h₁a :
  (𝓝[s] a).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
    (iteratedFDerivWithin 𝕜 n f s)
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a
h₄a : a ∈ s
m : (i : Fin (n + 1)) → E
⊢ UniqueDiffWithinAt 𝕜 s a

Tactic:
apply hs a h₄a
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
⊢ ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x

Tactic:
have h' : ContDiffWithinAt 𝕜' n f Set.univ x := h
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
⊢ (𝓝[Set.univ] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f Set.univ))
    (iteratedFDerivWithin 𝕜 n f Set.univ)

Tactic:
(h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial)

Premises used: trivial, ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
h₁ : 𝓝 x = 𝓝[Set.univ] x
h₂ :
  Eq (α := E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜' n f)
    (iteratedFDerivWithin 𝕜' n f Set.univ)
h₃ :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f)
    (iteratedFDerivWithin 𝕜 n f Set.univ)
convert_8 : UniqueDiffOn.{u_1, u_3} 𝕜 (E := E) Set.univ
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDeriv 𝕜' n f))
    (iteratedFDeriv 𝕜 n f)

Tactic:
convert! (h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial)

Premises used: trivial, ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
⊢ 𝓝 x = 𝓝[Set.univ] x

Tactic:
simp [iteratedFDerivWithin_univ.symm, uniqueDiffOn_univ]

Premises used: uniqueDiffOn_univ, Eq.symm, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
⊢ Eq (α := E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜' n f)
    (iteratedFDerivWithin 𝕜' n f Set.univ)

Tactic:
simp [iteratedFDerivWithin_univ.symm, uniqueDiffOn_univ]

Premises used: uniqueDiffOn_univ, Eq.symm, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f)
    (iteratedFDerivWithin 𝕜 n f Set.univ)

Tactic:
simp [iteratedFDerivWithin_univ.symm, uniqueDiffOn_univ]

Premises used: uniqueDiffOn_univ, Eq.symm, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
⊢ UniqueDiffOn.{u_1, u_3} 𝕜 (E := E) Set.univ

Tactic:
simp [iteratedFDerivWithin_univ.symm, uniqueDiffOn_univ]

Premises used: uniqueDiffOn_univ, Eq.symm, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDeriv 𝕜' n f) x)
    (iteratedFDeriv 𝕜 n f x)

Tactic:
h.restrictScalars_iteratedFDeriv_eventuallyEq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
rw :
  (∀ (i : ι),
      ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n
        (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t y
⊢ ContDiffWithinAt 𝕜 n f t y ↔
    ∀ (i : ι), ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffWithinAt_iff, contDiffWithinAt_pi]

Premises used: ContinuousLinearEquiv.comp_contDiffWithinAt_iff, contDiffWithinAt_pi, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι),
      ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n
        (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
hf : ∀ (i : ι), ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t y
⊢ ContDiffWithinAt 𝕜 n f t y

Tactic:
(contDiffWithinAt_piLp p).2 hf

Premises used: Iff.mpr, contDiffWithinAt_piLp
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Fintype ι
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
n : WithTop ℕ∞
i : ι
t : Set (PiLp p E)
y : PiLp p E
⊢ ContDiffWithinAt 𝕜 (F := E i) n (fun (f : PiLp p E) ↦ f.ofLp i) t y

Tactic:
(contDiffWithinAt_piLp p).1 contDiffWithinAt_id i

Premises used: Iff.mp, contDiffWithinAt_piLp, contDiffWithinAt_id
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
rw :
  (∀ (i : ι),
      ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n
        (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) y
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffAt_iff, contDiffAt_pi]

Premises used: contDiffAt_pi, ContinuousLinearEquiv.comp_contDiffAt_iff, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ (∀ (i : ι),
      ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n
        (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
hf : ∀ (i : ι), ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) y
⊢ ContDiffAt 𝕜 n f y

Tactic:
(contDiffAt_piLp p).2 hf

Premises used: Iff.mpr, contDiffAt_piLp
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Fintype ι
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
n : WithTop ℕ∞
i : ι
y : PiLp p E
⊢ ContDiffAt 𝕜 (F := E i) n (fun (f : PiLp p E) ↦ f.ofLp i) y

Tactic:
(contDiffAt_piLp p).1 contDiffAt_id i

Premises used: contDiffAt_id, Iff.mp, contDiffAt_piLp
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
rw :
  (∀ (i : ι),
      ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n
        (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffOn_iff, contDiffOn_pi]

Premises used: ContinuousLinearEquiv.comp_contDiffOn_iff, contDiffOn_pi, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι),
      ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n
        (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
hf : ∀ (i : ι), ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t
⊢ ContDiffOn 𝕜 n f t

Tactic:
(contDiffOn_piLp p).2 hf

Premises used: Iff.mpr, contDiffOn_piLp
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Fintype ι
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
n : WithTop ℕ∞
i : ι
t : Set (PiLp p E)
⊢ ContDiffOn 𝕜 (F := E i) n (fun (f : PiLp p E) ↦ f.ofLp i) t

Tactic:
(contDiffOn_piLp p).1 contDiffOn_id i

Premises used: contDiffOn_piLp, Iff.mp, contDiffOn_id
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
rw :
  (∀ (i : ι),
      ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦
        ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦ (f x).ofLp i
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦ (f x).ofLp i

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiff_iff, contDiff_pi]

Premises used: ContinuousLinearEquiv.comp_contDiff_iff, contDiff_pi, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ (∀ (i : ι),
      ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦
        ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦ (f x).ofLp i

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Fintype ι
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
n : WithTop ℕ∞
i : ι
⊢ ContDiff 𝕜 (F := E i) n fun (f : PiLp p E) ↦ f.ofLp i

Tactic:
(contDiff_piLp p).1 contDiff_id i

Premises used: contDiff_id, contDiff_piLp, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Fintype ι
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
n : WithTop ℕ∞
⊢ ContDiff 𝕜 (E := WithLp p ((i : ι) → E i)) n ofLp

Tactic:
(continuousLinearEquiv p 𝕜 E).contDiff

Premises used: PiLp.continuousLinearEquiv, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Fintype ι
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
n : WithTop ℕ∞
⊢ ContDiff 𝕜 (E := (i : ι) → E i) n (toLp p)

Tactic:
(continuousLinearEquiv p 𝕜 E).symm.contDiff

Premises used: ContinuousLinearEquiv.symm, PiLp.continuousLinearEquiv, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
p : ℝ≥0∞
inst_5 : Fact (1 ≤ p)
n : WithTop ℕ∞
⊢ ContDiff 𝕜 (E := WithLp p (E × F)) n ofLp

Tactic:
(prodContinuousLinearEquiv p 𝕜 E F).contDiff

Premises used: WithLp.prodContinuousLinearEquiv, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.WithLp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
p : ℝ≥0∞
inst_5 : Fact (1 ≤ p)
n : WithTop ℕ∞
⊢ ContDiff 𝕜 (E := E × F) n (toLp p)

Tactic:
(prodContinuousLinearEquiv p 𝕜 E F).symm.contDiff

Premises used: ContinuousLinearEquiv.symm, WithLp.prodContinuousLinearEquiv, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
h : ContDiffPointwiseHolderAt k α f a
⊢ ContinuousAt f a

Tactic:
h.contDiffAt.continuousAt

Premises used: ContDiffPointwiseHolderAt.contDiffAt, ContDiffAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
h : ContDiffPointwiseHolderAt k α f a
hk : k ≠ 0
⊢ DifferentiableAt ℝ f a

Tactic:
h.contDiffAt.differentiableAt <| mod_cast hk

Premises used: ContDiffAt.differentiableAt, congrArg, cast, Ne, Nat.cast, ContDiffPointwiseHolderAt.contDiffAt, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
f : E → F
a : E
⊢ ContDiffPointwiseHolderAt k 0 f a ↔ ContDiffAt ℝ (↑k : WithTop ℕ∞) f a

Tactic:
⟨contDiffAt, fun h ↦ ⟨h, ?_⟩⟩

Premises used: ContDiffPointwiseHolderAt.mk, Iff.intro, ContDiffPointwiseHolderAt.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
f : E → F
a : E
refine :
  ∀ (h : ContDiffAt ℝ (↑k : WithTop ℕ∞) f a),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (F := ℝ) (𝓝 a)
      (fun (x : E) ↦
        HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
          (iteratedFDeriv ℝ k f a))
      fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x - a‖ (↑0 : ℝ)
⊢ ContDiffPointwiseHolderAt k 0 f a ↔ ContDiffAt ℝ (↑k : WithTop ℕ∞) f a

Tactic:
refine ⟨contDiffAt, fun h ↦ ⟨h, ?_⟩⟩
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
f : E → F
a : E
h : ContDiffAt ℝ (↑k : WithTop ℕ∞) f a
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
        (iteratedFDeriv ℝ k f a))
    fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x - a‖ (↑0 : ℝ)

Tactic:
simpa using ((h.continuousAt_iteratedFDeriv le_rfl).sub_const _).norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, le_rfl, Filter.Tendsto.norm, Filter.Tendsto.sub_const, ContDiffAt.continuousAt_iteratedFDeriv