awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ∞
hf : ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a
have zero : ∀ (hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)), ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f.symm : F → E) a
Tactic: induction n using ENat.nat_induction with
    | zero =>
      apply contDiffAt_zero.2
      exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
    | succ n IH =>
      obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
      apply contDiffAt_succ_iff_hasFDerivAt.2
      -- For showing `n.succ` times continuous differentiability (the main inductive step), it
      -- suffices to produce the derivative and show that it is `n` times continuously
      -- differentiable
      have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
      -- This follows by a bootstrapping formula expressing the derivative as a
      -- function of `f` itself
      refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
      · -- We first check that the derivative of `f` is that formula
        have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
          have hf₀' := f₀'.nhds
          rw [← eq_f₀'] at hf₀'
          exact hf'.continuousAt.preimage_mem_nhds hf₀'
        obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
        use f.target ∩ f.symm ⁻¹' t
        refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
        · exact f.isOpen_inter_preimage_symm ht
        · exact mem_inter ha (mem_preimage.mpr htf)
        intro x hx
        obtain ⟨hxu, e, he⟩ := htu hx.2
        have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
          rw [he]
          exact hff' (f.symm x) hxu
        convert! f.hasFDerivAt_symm hx.1 h_deriv
        simp [← he]
      · -- Then we check that the formula, being a composition of `ContDiff` pieces, is
        -- itself `ContDiff`
        have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
          rw [eq_f₀']
          exact contDiffAt_map_inverse _
        have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
          refine IH (hf.of_le ?_)
          norm_cast
          exact Nat.le_succ n
        exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
    | top Itop => exact contDiffAt_infty.mpr fun n ↦ Itop n (contDiffAt_infty.mp hf n)
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ∞
hf : ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
zero : ∀ (hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)), ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f.symm : F → E) a
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
      ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a)
  (hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
  ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
Tactic: induction n using ENat.nat_induction with
    | zero =>
      apply contDiffAt_zero.2
      exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
    | succ n IH =>
      obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
      apply contDiffAt_succ_iff_hasFDerivAt.2
      -- For showing `n.succ` times continuous differentiability (the main inductive step), it
      -- suffices to produce the derivative and show that it is `n` times continuously
      -- differentiable
      have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
      -- This follows by a bootstrapping formula expressing the derivative as a
      -- function of `f` itself
      refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
      · -- We first check that the derivative of `f` is that formula
        have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
          have hf₀' := f₀'.nhds
          rw [← eq_f₀'] at hf₀'
          exact hf'.continuousAt.preimage_mem_nhds hf₀'
        obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
        use f.target ∩ f.symm ⁻¹' t
        refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
        · exact f.isOpen_inter_preimage_symm ht
        · exact mem_inter ha (mem_preimage.mpr htf)
        intro x hx
        obtain ⟨hxu, e, he⟩ := htu hx.2
        have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
          rw [he]
          exact hff' (f.symm x) hxu
        convert! f.hasFDerivAt_symm hx.1 h_deriv
        simp [← he]
      · -- Then we check that the formula, being a composition of `ContDiff` pieces, is
        -- itself `ContDiff`
        have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
          rw [eq_f₀']
          exact contDiffAt_map_inverse _
        have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
          refine IH (hf.of_le ?_)
          norm_cast
          exact Nat.le_succ n
        exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
    | top Itop => exact contDiffAt_infty.mpr fun n ↦ Itop n (contDiffAt_infty.mp hf n)
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
h : ContDiffWithinAt 𝕜' ω f s x
⊢ ContDiffWithinAt 𝕜 ω f s x
have obtain : ∀ (u : Set E) (u_mem : u ∈ 𝓝[insert x s] x) (p' : E → FormalMultilinearSeries 𝕜' E F)
  (hp' : HasFTaylorSeriesUpToOn ω f p' u)
  (Hp' :
    ∀ (i : ℕ),
      AnalyticOn 𝕜' (F := ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p' x i)
        u),
  ContDiffWithinAt 𝕜 ω f s x
Tactic: obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn ω f p' u
Hp' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜' (F := ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p' x i) u
⊢ ContDiffWithinAt 𝕜 ω f s x
have refine : ∀ (i : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ FormalMultilinearSeries.restrictScalars 𝕜 (p' x) i) u
Tactic: refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn ω f p' u
Hp' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜' (F := ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p' x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ FormalMultilinearSeries.restrictScalars 𝕜 (p' x) i) u
have change : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
  (fun (x : E) ↦
    ((ContinuousMultilinearMap.restrictScalarsLinear (E := fun (i : Fin i) ↦ E) 𝕜 :
          ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜' (fun (i : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
      (p' x i))
  u
Tactic: change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn ω f p' u
Hp' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜' (F := ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p' x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦
      ((ContinuousMultilinearMap.restrictScalarsLinear (E := fun (i : Fin i) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : ContinuousMultilinearMap 𝕜' (fun (i : Fin i) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
        (p' x i))
    u
have apply : AnalyticOnNhd 𝕜 (E := ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F) (F :=
  ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
  (⇑(ContinuousMultilinearMap.restrictScalarsLinear (E := fun (i : Fin i) ↦ E) 𝕜 :
        ContinuousMultilinearMap.{u_3, 0, uE, uF} 𝕜' (fun (i : Fin i) ↦ E) F →L[𝕜]
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
    (a : ContinuousMultilinearMap 𝕜' (fun (i : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
  univ
Tactic: apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n_1 : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
n : ℕ∞
h : ContDiffWithinAt 𝕜' (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
have rcases : ∀ (u : Set E) (u_mem : u ∈ 𝓝[insert x s] x) (p' : E → FormalMultilinearSeries 𝕜' E F)
  (hp' : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p' u),
  ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
Tactic: rcases h m hm with ⟨u, u_mem, p', hp'⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Polynomial (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
inst : CommSemiring R
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Algebra R 𝕜
f : R[X]
n : WithTop ℕ∞
⊢ ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f
have add : ∀ (f g : R[X]) (fc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f)
  (gc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) g),
  ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) (f + g)
Tactic: induction f using Polynomial.induction_on' with
  | add f g fc gc => simpa using fc.add gc
  | monomial n a => simpa using contDiff_const.mul (contDiff_id.pow _)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Polynomial (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
inst : CommSemiring R
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Algebra R 𝕜
f : R[X]
n : WithTop ℕ∞
add :
  ∀ (f g : R[X]) (fc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f)
    (gc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) g),
    ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) (f + g)
⊢ ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f
have monomial : ∀ (n_1 : ℕ) (a : R),
  ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) ((monomial n_1 : (a : R) → R[X]) a : R[X])
Tactic: induction f using Polynomial.induction_on' with
  | add f g fc gc => simpa using fc.add gc
  | monomial n a => simpa using contDiff_const.mul (contDiff_id.pow _)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (goal)
Goal:
n : WithTop ℕ∞
𝕂 : 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'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
have rcases : ∀ (u : Set E') (H : u ∈ 𝓝[insert x univ] x) (p : E' → FormalMultilinearSeries 𝕂 E' F')
  (hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u), HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
Tactic: rcases hf.of_le (ENat.one_le_iff_ne_zero_withTop.mpr hn) 1 le_rfl with ⟨u, H, p, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
n : WithTop ℕ∞
𝕂 : 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'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
u : Set E'
H : u ∈ 𝓝[insert x univ] x
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
have H₁ : u ∈ 𝓝 x
Tactic: simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
n : WithTop ℕ∞
𝕂 : 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'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u
H : u ∈ 𝓝 x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
have this : HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f
  ((continuousMultilinearCurryFin1 𝕂 E' F' : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ E') F') → E' →L[𝕂] F')
    (p x 1))
  x
Tactic: have := hp.hasStrictFDerivAt one_ne_zero H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
Tactic: have hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y := fun y hy =>
    (hf.hasFDerivWithinAt one_ne_zero (subset_insert x s hy)).mono (subset_insert x s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hcont : ContinuousWithinAt f' s x
Tactic: have hcont : ContinuousWithinAt f' s x :=
    (continuousMultilinearCurryFin1 ℝ E F).continuousAt.comp_continuousWithinAt
      ((hf.cont _ le_rfl _ (mem_insert _ _)).mono (subset_insert x s))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hK₁ : ‖f' x‖₊ < K
Tactic: replace hK : ‖f' x‖₊ < K := by simpa only [f', LinearIsometryEquiv.nnnorm_map]
Cleared hypotheses: hK
-- 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
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have rcases : ∀ (t : Set E) (hst : t ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries ℝ E F)
  (hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Tactic: rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩
-- 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
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have rcases : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : Metric.ball x ε ∩ insert x s ⊆ t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Tactic: rcases Metric.mem_nhdsWithin_iff.mp hst with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p t
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hp₁ : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
Tactic: replace hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s) := hp.mono hε
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hp₁ : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
Tactic: rw [← insert_eq_of_mem (Metric.mem_ball_self ε0), ← insert_inter_distrib] at hp
Cleared hypotheses: hp
-- 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
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have rcases : ∀ (K : ℝ≥0) (t : Set E) (hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x) (hft : LipschitzOnWith K f t),
  ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Tactic: rcases hp.exists_lipschitzOnWith ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RCLike (hypothesis)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x
hft : LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have hst₁ : t ∈ 𝓝[s] x
Tactic: rw [inter_comm, ← nhdsWithin_restrict' _ (Metric.ball_mem_nhds _ ε0)] at hst
Cleared hypotheses: hst, hft
-- 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
f : E → F
s : Set E
hs : Convex ℝ s
hf : ContDiffOn ℝ 1 f s
x : E
hx : x ∈ s
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have obtain : ∀ (K : ℝ≥0) (t : Set E) (ht : t ∈ 𝓝[s] x) (hf : LipschitzOnWith K f t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Tactic: obtain ⟨K, t, ht, hf⟩ := ContDiffWithinAt.exists_lipschitzOnWith (hf x hx) hs
-- 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
f : E → F
s : Set E
hs : Convex ℝ s
hf_1 : ContDiffOn ℝ 1 f s
x : E
hx : x ∈ s
K : ℝ≥0
t : Set E
ht : t ∈ 𝓝[s] x
hf : LipschitzOnWith K f t
w : ℝ≥0
w₁ : Set E
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have h : t ∈ 𝓝[s] x ∧ LipschitzOnWith K f t
Tactic: use K, t
-- 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 : ContDiff 𝕂 1 f
x : E'
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
have rcases : ∀ (K : ℝ≥0) (t : Set E') (ht : t ∈ 𝓝 x) (hf : LipschitzOnWith K f t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
Tactic: rcases hf.contDiffAt.exists_lipschitzOnWith with ⟨K, t, ht, hf⟩