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
h₁ :
  ∀ (a : E)
    (h₁a :
      ∀ᶠ (x : E) in 𝓝[s] a,
        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)) (iteratedFDerivWithin 𝕜' n f s) x)
          (iteratedFDerivWithin 𝕜 n f s x))
    (h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a) (h₄a : a ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin (n + 1)) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin (n + 1)) ↦ E)) (iteratedFDerivWithin 𝕜' (n + 1) f s) a)
      (iteratedFDerivWithin 𝕜 (n + 1) f s a)
⊢ (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin (n + 1)) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin (n + 1)) ↦ E)) (iteratedFDerivWithin 𝕜' (n + 1) f s))
    (iteratedFDerivWithin 𝕜 (n + 1) f s)

Tactic:
filter_upwards [eventually_eventually_nhdsWithin.2 (hn t₀), t₁,
      eventually_mem_nhdsWithin (a := x) (s := s)] with a h₁a h₃a h₄a

Premises used: Iff.mpr, eventually_mem_nhdsWithin, eventually_eventually_nhdsWithin
-- 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 :
  ∀ᶠ (x : E) in 𝓝[s] a,
    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)) (iteratedFDerivWithin 𝕜' n f s) x)
      (iteratedFDerivWithin 𝕜 n f s x)
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a
h₄a : a ∈ s
⊢ (𝓝[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)

Tactic:
rw [← Filter.EventuallyEq] at h₁a

Premises used: Filter.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_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 :
  ∀ᶠ (x : E) in 𝓝[s] a,
    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)) (iteratedFDerivWithin 𝕜' n f s) x)
      (iteratedFDerivWithin 𝕜 n f s x)
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a
h₄a : a ∈ s
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)
⊢ ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a

Tactic:
rw [← Filter.EventuallyEq] at h₁a

Premises used: Filter.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_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 :
  ∀ᶠ (x : E) in 𝓝[s] a,
    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)) (iteratedFDerivWithin 𝕜' n f s) x)
      (iteratedFDerivWithin 𝕜 n f s x)
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a
h₄a : a ∈ s
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
⊢ a ∈ s

Tactic:
rw [← Filter.EventuallyEq] at h₁a

Premises used: Filter.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_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
h₁ :
  ∀ (m : (i : Fin (n + 1)) → E),
    Eq.{u_4 + 1} (α := F)
      ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin (n + 1)) ↦ E) F)
              (restrictScalars 𝕜 (M₁ := fun (i : Fin (n + 1)) ↦ E)) (iteratedFDerivWithin 𝕜' (n + 1) f s) a :
            (a : (i : Fin (n + 1)) → E) → F)
          m :
        F)
      ((iteratedFDerivWithin 𝕜 (n + 1) f s a : (a : (i : Fin (n + 1)) → E) → F) m : F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin (n + 1)) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin (n + 1)) ↦ E)) (iteratedFDerivWithin 𝕜' (n + 1) f s) a)
    (iteratedFDerivWithin 𝕜 (n + 1) f s a)

Tactic:
ext m
-- 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
h₁ :
  Eq.{u_4 + 1} (α := F)
    ((((fderivWithin 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a :
                (a : E) → ContinuousMultilinearMap 𝕜' (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s a :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)
⊢ Eq.{u_4 + 1} (α := F)
    ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin (n + 1)) ↦ E) F)
            (restrictScalars 𝕜 (M₁ := fun (i : Fin (n + 1)) ↦ E)) (iteratedFDerivWithin 𝕜' (n + 1) f s) a :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)
    ((iteratedFDerivWithin 𝕜 (n + 1) f s a : (a : (i : Fin (n + 1)) → E) → F) m : F)

Tactic:
simp only [Function.comp_apply, coe_restrictScalars, iteratedFDerivWithin_succ_apply_left]

Premises used: iteratedFDerivWithin_succ_apply_left, ContinuousMultilinearMap.coe_restrictScalars, Function.comp_apply
-- 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
⊢ Eq.{u_4 + 1} (α := F)
    ((((fderivWithin 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a :
                (a : E) → ContinuousMultilinearMap 𝕜' (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)
    ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
            (restrictScalars 𝕜 (M₁ := fun (x : Fin n) ↦ E))
            (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a)) :
              (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F)
            (m 0) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)

Tactic:
simp
-- 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
h₁ : LT.lt (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
h₂ : UniqueDiffOn 𝕜' (insert a s)
⊢ DifferentiableWithinAt 𝕜' (F := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜' n f s) s a

Tactic:
apply h₃a.differentiableWithinAt_iteratedFDerivWithin

Premises used: ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin
-- 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
h₁ : n < n + 1
⊢ LT.lt (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)

Tactic:
rw [Nat.cast_lt]

Premises used: Nat.cast_lt
-- 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
⊢ n < n + 1

Tactic:
simp
-- 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
⊢ UniqueDiffOn 𝕜' s

Tactic:
have : UniqueDiffOn 𝕜' s := hs.mono_field
-- 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
this : UniqueDiffOn 𝕜' s
⊢ UniqueDiffOn 𝕜' (insert a s)

Tactic:
simpa [s.insert_eq_of_mem h₄a]

Premises used: Set.insert_eq_of_mem