awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) Set.univ e ↔
    ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e

Tactic:
exact analyticWithinAt_pi_iff

Premises used: analyticWithinAt_pi_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
hf : ∀ (i : ι), AnalyticOn 𝕜 (f i) s
⊢ AnalyticOn 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s

Tactic:
fun x hx ↦ AnalyticWithinAt.pi (fun i ↦ hf i x hx)

Premises used: AnalyticOn, AnalyticWithinAt.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
⊢ AnalyticOn 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s ↔ ∀ (i : ι), AnalyticOn 𝕜 (f i) s

Tactic:
⟨fun h i x hx ↦ analyticWithinAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩

Premises used: analyticWithinAt_pi_iff, AnalyticOn.pi, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
hf : ∀ (i : ι), AnalyticOnNhd 𝕜 (f i) s
⊢ AnalyticOnNhd 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s

Tactic:
fun x hx ↦ AnalyticAt.pi (fun i ↦ hf i x hx)

Premises used: AnalyticOnNhd, AnalyticAt.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
⊢ AnalyticOnNhd 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s ↔ ∀ (i : ι), AnalyticOnNhd 𝕜 (f i) s

Tactic:
⟨fun h i x hx ↦ analyticAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩

Premises used: Iff.intro, Iff.mp, AnalyticOnNhd.pi, analyticAt_pi_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : Module A E
inst_6 : IsBoundedSMul A E
inst_7 : IsScalarTower 𝕜 A E
z : A × E
⊢ AnalyticAt 𝕜 (F := E) (fun (x : A × E) ↦ x.1 • x.2) z

Tactic:
(ContinuousLinearMap.lsmul 𝕜 A).analyticAt_bilinear z

Premises used: ContinuousLinearMap.lsmul, ContinuousLinearMap.analyticAt_bilinear
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
z : A × A
⊢ AnalyticAt 𝕜 (F := A) (fun (x : A × A) ↦ x.1 * x.2) z

Tactic:
analyticAt_smul z

Premises used: analyticAt_smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
A : Type u_7
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsBoundedSMul A F
inst_9 : IsScalarTower 𝕜 A F
f : E → A
g : E → F
s : Set E
z : E
hf : AnalyticWithinAt 𝕜 f s z
hg : AnalyticWithinAt 𝕜 g s z
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ f x • g x) s z

Tactic:
(analyticAt_smul _).comp₂_analyticWithinAt hf hg

Premises used: analyticAt_smul, AnalyticAt.comp₂_analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
A : Type u_7
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsBoundedSMul A F
inst_9 : IsScalarTower 𝕜 A F
f : E → A
g : E → F
z : E
hf : AnalyticAt 𝕜 f z
hg : AnalyticAt 𝕜 g z
⊢ AnalyticAt 𝕜 (f • g) z

Tactic:
(analyticAt_smul _).comp₂ hf hg

Premises used: analyticAt_smul, AnalyticAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
A : Type u_7
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsBoundedSMul A F
inst_9 : IsScalarTower 𝕜 A F
f : E → A
g : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
hg : AnalyticOn 𝕜 g s
⊢ AnalyticOn.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ f x • g x) s

Tactic:
fun _ m ↦ (hf _ m).smul (hg _ m)

Premises used: AnalyticOn, AnalyticWithinAt.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
A : Type u_7
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsBoundedSMul A F
inst_9 : IsScalarTower 𝕜 A F
f : E → A
g : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
hg : AnalyticOnNhd 𝕜 g s
⊢ AnalyticOnNhd.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ f x • g x) s

Tactic:
fun _ m ↦ (hf _ m).smul (hg _ m)

Premises used: AnalyticOnNhd, AnalyticAt.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
s : Set E
z : E
hf : AnalyticWithinAt 𝕜 f s z
hg : AnalyticWithinAt 𝕜 g s z
⊢ AnalyticWithinAt.{u_2, u_3, u_7} 𝕜 (F := A) (fun (x : E) ↦ f x * g x) s z

Tactic:
(analyticAt_mul _).comp₂_analyticWithinAt hf hg

Premises used: AnalyticAt.comp₂_analyticWithinAt, analyticAt_mul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
z : E
hf : AnalyticAt 𝕜 f z
hg : AnalyticAt 𝕜 g z
⊢ AnalyticAt 𝕜 (f * g) z

Tactic:
hf.smul hg

Premises used: AnalyticAt.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
s : Set E
hf : AnalyticOn 𝕜 f s
hg : AnalyticOn 𝕜 g s
⊢ AnalyticOn.{u_2, u_3, u_7} 𝕜 (F := A) (fun (x : E) ↦ f x * g x) s

Tactic:
hf.smul hg

Premises used: AnalyticOn.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
s : Set E
hf : AnalyticOnNhd 𝕜 f s
hg : AnalyticOnNhd 𝕜 g s
⊢ AnalyticOnNhd.{u_2, u_3, u_7} 𝕜 (F := A) (fun (x : E) ↦ f x * g x) s

Tactic:
hf.smul hg

Premises used: AnalyticOnNhd.smul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
zero : AnalyticWithinAt.{u_2, u_3, u_7} 𝕜 (F := A) 1 s z
⊢ AnalyticWithinAt 𝕜 (HPow.hPow (β := ℕ) f 0) s z

Tactic:
simp only [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
⊢ AnalyticWithinAt.{u_2, u_3, u_7} 𝕜 (F := A) 1 s z

Tactic:
apply analyticWithinAt_const

Premises used: analyticWithinAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
succ : AnalyticWithinAt 𝕜 (f ^ m * f) s z
⊢ AnalyticWithinAt 𝕜 (f ^ (m + 1)) s z

Tactic:
simp only [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
⊢ AnalyticWithinAt 𝕜 (f ^ m * f) s z

Tactic:
hm.mul hf

Premises used: AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
⊢ AnalyticWithinAt 𝕜 (f ^ m * f) s z

Tactic:
exact hm.mul hf

Premises used: AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
n : ℕ
zero : AnalyticWithinAt 𝕜 (HPow.hPow (β := ℕ) f 0) s z
succ : ∀ (m : ℕ) (hm : AnalyticWithinAt 𝕜 (f ^ m) s z), AnalyticWithinAt 𝕜 (f ^ (m + 1)) s z
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
induction n with
  | zero =>
    simp only [pow_zero]
    apply analyticWithinAt_const
  | succ m hm =>
    simp only [pow_succ]
    exact hm.mul hf

Premises used: analyticWithinAt_const, pow_succ, pow_zero
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticAt 𝕜 f z
n : ℕ
rw : ∀ (hf : AnalyticWithinAt 𝕜 f Set.univ z) (n : ℕ), AnalyticWithinAt 𝕜 (f ^ n) Set.univ z
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) Set.univ z

Tactic:
hf.pow n

Premises used: AnalyticWithinAt.pow
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) Set.univ z

Tactic:
exact hf.pow n

Premises used: AnalyticWithinAt.pow
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
s : Set E
hf : AnalyticOn 𝕜 f s
n : ℕ
⊢ AnalyticOn 𝕜 (f ^ n) s

Tactic:
fun _ m ↦ (hf _ m).pow n

Premises used: AnalyticOn, AnalyticWithinAt.pow
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
s : Set E
hf : AnalyticOnNhd 𝕜 f s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (f ^ n) s

Tactic:
fun _ m ↦ (hf _ m).pow n

Premises used: AnalyticOnNhd, AnalyticAt.pow
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
hf : AnalyticWithinAt 𝕜 f s z
hn : 0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
simpa [← zpow_natCast, hn] using hf.pow n.toNat

Premises used: zpow_natCast, AnalyticWithinAt.pow, Int.toNat
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
hf : AnalyticAt 𝕜 f z
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
simpa [← zpow_natCast, hn] using hf.pow n.toNat

Premises used: zpow_natCast, Int.toNat, AnalyticAt.pow
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
s : Set E
n : ℤ
hf : AnalyticOn 𝕜 f s
hn : 0 ≤ n
⊢ AnalyticOn 𝕜 (f ^ n) s

Tactic:
simpa [← zpow_natCast, hn] using hf.pow n.toNat

Premises used: zpow_natCast, AnalyticOn.pow, Int.toNat
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
s : Set E
n : ℤ
hf : AnalyticOnNhd 𝕜 f s
hn : 0 ≤ n
simp_rw : AnalyticOnNhd 𝕜 (HPow.hPow (β := ℕ) f (OfNat.ofNat n.toNat)) s
⊢ AnalyticOnNhd 𝕜 (f ^ n) s

Tactic:
simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]

Premises used: Int.toNat_of_nonneg, zpow_ofNat, Eq.symm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
s : Set E
n : ℤ
hf : AnalyticOnNhd 𝕜 f s
hn : 0 ≤ n
⊢ AnalyticOnNhd 𝕜 (HPow.hPow (β := ℕ) f (OfNat.ofNat n.toNat)) s

Tactic:
apply pow hf

Premises used: AnalyticOnNhd.pow
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
n : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (FormalMultilinearSeries.restrictScalars 𝕜 p n) ≤
    ‖p n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
n : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (FormalMultilinearSeries.restrictScalars 𝕜 p n) ≤
    ‖p n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
hf : HasFPowerSeriesWithinAt f p s x
rcases :
  ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r),
    HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Tactic:
rcases hf with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Tactic:
⟨r, hr.restrictScalars⟩

Premises used: HasFPowerSeriesWithinOnBall.restrictScalars, HasFPowerSeriesWithinAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Tactic:
exact ⟨r, hr.restrictScalars⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
hf : HasFPowerSeriesAt f p x
rcases :
  ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesOnBall f p x r), HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x

Tactic:
rcases hf with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x

Tactic:
⟨r, hr.restrictScalars⟩

Premises used: HasFPowerSeriesOnBall.restrictScalars, Exists.intro, HasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x

Tactic:
exact ⟨r, hr.restrictScalars⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
hf : AnalyticWithinAt 𝕜' f s x
rcases : ∀ (p : FormalMultilinearSeries 𝕜' E F) (hp : HasFPowerSeriesWithinAt f p s x), AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases hf with ⟨p, hp⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

Premises used: AnalyticWithinAt, FormalMultilinearSeries.restrictScalars, HasFPowerSeriesWithinAt.restrictScalars, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : AnalyticAt 𝕜' f x
rcases : ∀ (p : FormalMultilinearSeries 𝕜' E F) (hp : HasFPowerSeriesAt f p x), AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases hf with ⟨p, hp⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesAt f p x
⊢ AnalyticAt 𝕜 f x

Tactic:
⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

Premises used: HasFPowerSeriesAt.restrictScalars, FormalMultilinearSeries.restrictScalars, AnalyticAt, Exists.intro