awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ
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)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
h_deriv₂ : ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (inverse ∘ f' ∘ (↑f.symm : F → E)) a

Tactic:
(h_deriv₁.comp _ hf').comp _ h_deriv₂

Premises used: dite, ContDiffAt.comp, ContinuousLinearMap.inverse
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ
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)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
h_deriv₂ : ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (inverse ∘ f' ∘ (↑f.symm : F → E)) a

Tactic:
exact (h_deriv₁.comp _ hf').comp _ h_deriv₂

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ∞ω
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)
Itop :
  ∀ (n : ℕ) (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 ∞ (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 ∞ (↑f.symm : F → E) a

Tactic:
contDiffAt_infty.mpr fun n ↦ Itop n (contDiffAt_infty.mp hf n)

Premises used: Iff.mpr, contDiffAt_infty, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ∞ω
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)
Itop :
  ∀ (n : ℕ) (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 ∞ (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 ∞ (↑f.symm : F → E) a

Tactic:
exact contDiffAt_infty.mpr fun n ↦ Itop n (contDiffAt_infty.mp hf n)

Premises used: Iff.mpr, contDiffAt_infty, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ∞ω
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)
hf : ContDiffAt 𝕜 n (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 n (↑f.symm : F → E) a

Tactic:
match n with
  | ω =>
    apply AnalyticAt.contDiffAt
    exact f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv
  | (n : ℕ∞) =>
    -- We prove this by induction on `n`
    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)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ∞ω
inst_5 : CompleteSpace E
f : E ≃ₜ F
f₀' : E → E ≃L[𝕜] F
hf₀' : ∀ (a : E), HasFDerivAt (⇑f : (a : E) → F) (↑(f₀' a) : E →L[𝕜] F) a
hf : ContDiff.{u_1, uE, uF} 𝕜 (E := E) (F := F) n (⇑f : (a : E) → F)
⊢ ContDiff.{u_1, uF, uE} 𝕜 (E := F) (F := E) n (⇑f.symm : (a : F) → E)

Tactic:
contDiff_iff_contDiffAt.2 fun x =>
    f.toOpenPartialHomeomorph.contDiffAt_symm (mem_univ x) (hf₀' _) hf.contDiffAt

Premises used: Iff.mpr, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.contDiffAt_symm, Set.mem_univ, contDiff_iff_contDiffAt, OpenPartialHomeomorph.symm, Homeomorph.toOpenPartialHomeomorph, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
inst_1 : CompleteSpace 𝕜
f : OpenPartialHomeomorph 𝕜 𝕜
f₀' a : 𝕜
h₀ : f₀' ≠ 0
ha : a ∈ f.target
hf₀' : HasDerivAt (↑f : 𝕜 → 𝕜) f₀' ((↑f.symm : 𝕜 → 𝕜) a)
hf : ContDiffAt 𝕜 n (↑f : 𝕜 → 𝕜) ((↑f.symm : 𝕜 → 𝕜) a)
⊢ ContDiffAt 𝕜 n (↑f.symm : 𝕜 → 𝕜) a

Tactic:
f.contDiffAt_symm ha (hf₀'.hasFDerivAt_equiv h₀) hf

Premises used: OpenPartialHomeomorph.contDiffAt_symm, HasDerivAt.hasFDerivAt_equiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
inst_1 : CompleteSpace 𝕜
f : 𝕜 ≃ₜ 𝕜
f' : 𝕜 → 𝕜
h₀ : ∀ (x : 𝕜), f' x ≠ 0
hf' : ∀ (x : 𝕜), HasDerivAt (⇑f : (a : 𝕜) → 𝕜) (f' x) x
hf : ContDiff 𝕜 (E := 𝕜) (F := 𝕜) n (⇑f : (a : 𝕜) → 𝕜)
⊢ ContDiff 𝕜 (E := 𝕜) (F := 𝕜) n (⇑f.symm : (a : 𝕜) → 𝕜)

Tactic:
contDiff_iff_contDiffAt.2 fun x =>
    f.toOpenPartialHomeomorph.contDiffAt_symm_deriv (h₀ _) (mem_univ x) (hf' _) hf.contDiffAt

Premises used: Iff.mpr, OpenPartialHomeomorph.contDiffAt_symm_deriv, OpenPartialHomeomorph.toFun', Set.mem_univ, contDiff_iff_contDiffAt, OpenPartialHomeomorph.symm, Homeomorph.toOpenPartialHomeomorph, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_2
inst_7 : NormedAddCommGroup X
inst_8 : NormedSpace 𝕜 X
s t : Set E
f_1 : E → F
g : F → G
x_1 x₀ : E
b : E × F → G
m n_1 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
i : ℕ
f : OpenPartialHomeomorph E F
n : ℕ∞ω
hn : n ≠ ∞
x : E
hx : x ∈ f.source
⊢ Membership.mem (γ := Set F)
      {y : F | ContDiffAt 𝕜 n (↑f.symm : F → E) y ∧ ContDiffAt 𝕜 n (↑f : E → F) ((↑f.symm : F → E) y)}
      ((↑f : E → F) x) ↔
    Membership.mem (γ := Set E)
      {x : E | ContDiffAt 𝕜 n (↑f : E → F) x ∧ ContDiffAt 𝕜 n (↑f.symm : F → E) ((↑f : E → F) x)} x

Tactic:
simp [hx, and_comm]

Premises used: and_comm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : OpenPartialHomeomorph E F
n : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffOn 𝕜 n (↑f : E → F) (restrContDiff 𝕜 f n hn).source

Tactic:
fun _x hx ↦ hx.2.1.contDiffWithinAt

Premises used: ContDiffOn, And.right, And.left, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : OpenPartialHomeomorph E F
n : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffOn 𝕜 n (↑f.symm : F → E) (restrContDiff 𝕜 f n hn).target

Tactic:
fun _x hx ↦ hx.2.1.contDiffWithinAt

Premises used: ContDiffOn, And.right, And.left, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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

Tactic:
⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩

Premises used: And.intro, Exists.intro, ContDiffWithinAt, HasFTaylorSeriesUpToOn.restrictScalars
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ
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
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ FormalMultilinearSeries.restrictScalars 𝕜 (p' x) i) u

Tactic:
change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u

Premises used: AnalyticOn, ContinuousMultilinearMap.restrictScalarsLinear, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ
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
⊢ 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:
apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, AnalyticOnNhd.comp_analyticOn, AnalyticOn.restrictScalars
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ
⊢ 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:
ContinuousLinearMap.analyticOnNhd _ _

Premises used: ContinuousLinearMap.analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ
⊢ 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:
exact ContinuousLinearMap.analyticOnNhd _ _

Premises used: ContinuousLinearMap.analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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
⊢ ∃ 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'⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : 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:
⟨u, u_mem, _, hp'.restrictScalars _⟩

Premises used: And.intro, Exists.intro, HasFTaylorSeriesUpToOn.restrictScalars
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : 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:
exact ⟨u, u_mem, _, hp'.restrictScalars _⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 𝕜' n f s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
match n with
  | ω =>
    obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
    refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
    change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u
    apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)
    exact ContinuousLinearMap.analyticOnNhd _ _
  | (n : ℕ∞) =>
    intro m hm
    rcases h m hm with ⟨u, u_mem, p', hp'⟩
    exact ⟨u, u_mem, _, hp'.restrictScalars _⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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 : ContDiffOn 𝕜' n f s
⊢ ContDiffOn 𝕜 n f s

Tactic:
fun x hx =>
  (h x hx).restrict_scalars _

Premises used: ContDiffOn, ContDiffWithinAt.restrict_scalars