awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hn : n ≠ 0
hs : Convex ℝ s
hs' : IsCompact s
apply : LocallyLipschitzOn s f
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s

Tactic:
apply LocallyLipschitzOn.exists_lipschitzOnWith_of_compact hs'

Premises used: LocallyLipschitzOn.exists_lipschitzOnWith_of_compact
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hn : n ≠ 0
hs : Convex ℝ s
hs' : IsCompact s
⊢ LocallyLipschitzOn s f

Tactic:
(hf.of_le <| ENat.one_le_iff_ne_zero_withTop.2 hn).locallyLipschitzOn hs

Premises used: Iff.mpr, ENat.one_le_iff_ne_zero_withTop, ContDiffOn.of_le, ContDiffOn.locallyLipschitzOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hn : n ≠ 0
hs : Convex ℝ s
hs' : IsCompact s
⊢ LocallyLipschitzOn s f

Tactic:
exact (hf.of_le <| ENat.one_le_iff_ne_zero_withTop.2 hn).locallyLipschitzOn hs

Premises used: Iff.mpr, ENat.one_le_iff_ne_zero_withTop, ContDiffOn.of_le, ContDiffOn.locallyLipschitzOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
obtain : ∀ (C : ℝ) (hC : ∀ (x : E'), norm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ C), ∃ (C : ℝ≥0), LipschitzWith C f
⊢ ∃ (C : ℝ≥0), LipschitzWith C f

Tactic:
obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)

Premises used: HasCompactSupport.fderiv, ContDiff.continuous_fderiv, HasCompactSupport.exists_bound_of_continuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
C : ℝ
hC : ∀ (x : E'), norm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ C
⊢ ∃ (C : ℝ≥0), LipschitzWith C f

Tactic:
⟨.mk (max C 0) (le_max_right _ _), ?_⟩

Premises used: le_max_right, NNReal.mk, Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
C : ℝ
hC : ∀ (x : E'), norm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ C
refine : LipschitzWith (NNReal.mk (max C 0) ⋯) f
⊢ ∃ (C : ℝ≥0), LipschitzWith C f

Tactic:
refine ⟨.mk (max C 0) (le_max_right _ _), ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
C : ℝ
hC : ∀ (x : E'), norm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ C
apply : ∀ (x : E'), nnnorm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ NNReal.mk (max C 0) ⋯
⊢ LipschitzWith (NNReal.mk (max C 0) ⋯) f

Tactic:
apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)

Premises used: lipschitzWith_of_nnnorm_fderiv_le, ContDiff.differentiable
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
C : ℝ
hC : ∀ (x : E'), norm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ C
x : E'
⊢ nnnorm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ NNReal.mk (max C 0) ⋯

Tactic:
simp [← NNReal.coe_le_coe, hC x]

Premises used: NNReal.coe_le_coe
-- 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
n : ℕ
s : Set E
φ : E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
simp :
  Eq (α := (a : E) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F)
    (⇑(fderivWithin 𝕜
          ((⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
                  ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F) ∘
            φ)
          s x) :
      (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
      (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
      (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x)) :
        (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F))
⊢ Eq (α := (a : E) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F)
    (⇑(fderivWithin 𝕜 (restrictScalars 𝕜 (M₁ := fun (x : Fin n) ↦ E) ∘ φ) s x) :
      (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) 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 𝕜' φ s x)) :
        (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F))

Tactic:
simp only [← restrictScalarsLinear_apply]

Premises used: ContinuousMultilinearMap.restrictScalarsLinear_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
n : ℕ
s : Set E
φ : E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F)
    (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
          ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
      (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
    (φ x)

Tactic:
fun_prop
-- 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
n : ℕ
s : Set E
φ : E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
rw :
  Eq (α := (a : E) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F)
    (⇑((restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) ∘SL
          (fderivWithin 𝕜 φ s x : E →L[𝕜] ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)) :
      (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
      (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
      (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x)) :
        (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F))
⊢ Eq (α := (a : E) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F)
    (⇑(fderivWithin 𝕜
          ((⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
                  ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F) ∘
            φ)
          s x) :
      (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
      (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
      (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x)) :
        (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F))

Tactic:
rw [fderiv_comp_fderivWithin _ (by fun_prop) (h.restrictScalars 𝕜) hs, ContinuousLinearMap.fderiv]

Premises used: ContinuousLinearMap.fderiv, fderiv_comp_fderivWithin, DifferentiableWithinAt.restrictScalars
-- 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
n : ℕ
s : Set E
φ : E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
a : E
b : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := F)
    (((((restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
                    ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
                      ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) ∘SL
                  (fderivWithin 𝕜 φ s x :
                    E →L[𝕜] ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
              a :
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        b :
      F)
    ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
            (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
                  ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
            (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x)) :
              (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F)
            a :
          (a : (i : Fin n) → E) → F)
        b :
      F)

Tactic:
simp [h.restrictScalars_fderivWithin 𝕜 hs]

Premises used: DifferentiableWithinAt.restrictScalars_fderivWithin
-- 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 : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ContDiffWithinAt 𝕜' (↑0 : WithTop ℕ∞) f s x
zero :
  ∀ (a : E),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin 0) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin 0) ↦ E)) (iteratedFDerivWithin 𝕜' 0 f s) a)
      (iteratedFDerivWithin 𝕜 0 f s a)
⊢ (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin 0) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin 0) ↦ E)) (iteratedFDerivWithin 𝕜' 0 f s))
    (iteratedFDerivWithin 𝕜 0 f s)

Tactic:
filter_upwards with 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 : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ContDiffWithinAt 𝕜' (↑0 : WithTop ℕ∞) f s x
a : E
zero :
  ∀ (m : (i : Fin 0) → E),
    Eq.{u_4 + 1} (α := F)
      ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin 0) ↦ E) F)
              (restrictScalars 𝕜 (M₁ := fun (i : Fin 0) ↦ E)) (iteratedFDerivWithin 𝕜' 0 f s) a :
            (a : (i : Fin 0) → E) → F)
          m :
        F)
      ((iteratedFDerivWithin 𝕜 0 f s a : (a : (i : Fin 0) → E) → F) m : F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin 0) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin 0) ↦ E)) (iteratedFDerivWithin 𝕜' 0 f s) a)
    (iteratedFDerivWithin 𝕜 0 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 : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ContDiffWithinAt 𝕜' (↑0 : WithTop ℕ∞) f s x
a : E
m : (i : Fin 0) → E
⊢ Eq.{u_4 + 1} (α := F)
    ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin 0) ↦ E) F)
            (restrictScalars 𝕜 (M₁ := fun (i : Fin 0) ↦ E)) (iteratedFDerivWithin 𝕜' 0 f s) a :
          (a : (i : Fin 0) → E) → F)
        m :
      F)
    ((iteratedFDerivWithin 𝕜 0 f s a : (a : (i : Fin 0) → E) → F) 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
⊢ ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x

Tactic:
have t₀ := h.of_le (Nat.cast_le.mpr (n.le_add_right 1))
-- 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
nth_rw : ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y
⊢ ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y

Tactic:
nth_rw 2 [← s.insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- 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
⊢ Ne (α := WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

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
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y

Tactic:
apply h.eventually (by simp)

Premises used: ContDiffWithinAt.eventually
-- 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
⊢ ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y

Tactic:
have t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1)) f s y := by
      nth_rw 2 [← s.insert_eq_of_mem hx]
      apply h.eventually (by simp)