awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (goal)
Goal:
𝕂 : 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_1 : ContDiff 𝕂 1 f
x : E'
K : ℝ≥0
t : Set E'
ht : t ∈ 𝓝 x
hf : LipschitzOnWith K f t
w : ℝ≥0
w₁ : Set E'
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
have h : t ∈ 𝓝 x ∧ LipschitzOnWith K f t
Tactic: use K, t
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (goal)
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
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have apply : LocallyLipschitzOn s f
Tactic: apply LocallyLipschitzOn.exists_lipschitzOnWith_of_compact hs'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (goal)
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 : ℝ≥0), LipschitzWith C f
have obtain : ∀ (C : ℝ) (hC : ∀ (x : E'), norm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ C), ∃ (C : ℝ≥0), LipschitzWith C f
Tactic: obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (goal)
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
have refine : LipschitzWith (NNReal.mk (max C 0) sorry) f
Tactic: refine ⟨.mk (max C 0) (le_max_right _ _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (goal)
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
⊢ LipschitzWith (NNReal.mk (max C 0) ⋯) f
have apply : ∀ (x : E'), nnnorm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) ≤ NNReal.mk (max C 0) sorry
Tactic: apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
⊢ 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))
have 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))
Tactic: simp only [← restrictScalarsLinear_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
⊢ 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))
have 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))
Tactic: rw [fderiv_comp_fderivWithin _ (by fun_prop) (h.restrictScalars 𝕜) hs, ContinuousLinearMap.fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
⊢ 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))
have h₁ : ∀ (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: ext a b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
⊢ (𝓝[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)
have 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)
Tactic: filter_upwards with a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
⊢ 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)
have 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)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (hypothesis)
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
⊢ (𝓝[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)
have t₀ : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x
Tactic: have t₀ := h.of_le (Nat.cast_le.mpr (n.le_add_right 1))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
have nth_rw : ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y
Tactic: nth_rw 2 [← s.insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (hypothesis)
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
⊢ (𝓝[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)
have t₁ : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
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
⊢ (𝓝[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)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (hypothesis)
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
⊢ 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)
have 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)
Tactic: rw [← Filter.EventuallyEq] at h₁a
Cleared hypotheses: h₁a, h₃a, h₄a