awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
s : Set (G × ((i : ι) → Em i))
⊢ CPolynomialOn 𝕜 (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    s

Tactic:
fun _ _ ↦ f.cpolynomialAt_uncurry_of_multilinear

Premises used: ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
s : Set (G × ((i : ι) → Em i))
⊢ AnalyticOnNhd 𝕜 (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    s

Tactic:
f.cpolynomialOn_uncurry_of_multilinear.analyticOnNhd

Premises used: ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, CPolynomialOn.analyticOnNhd
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
s : Set (G × ((i : ι) → Em i))
⊢ AnalyticOn 𝕜 (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    s

Tactic:
f.analyticOnNhd_uncurry_of_multilinear.analyticOn

Premises used: AnalyticOnNhd.analyticOn, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
x : G × ((i : ι) → Em i)
⊢ AnalyticAt 𝕜 (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    x

Tactic:
f.cpolynomialAt_uncurry_of_multilinear.analyticAt

Premises used: ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, CPolynomialAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
s : Set (G × ((i : ι) → Em i))
x : G × ((i : ι) → Em i)
⊢ AnalyticWithinAt 𝕜 (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    s x

Tactic:
f.analyticAt_uncurry_of_multilinear.analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, ContinuousLinearMap.analyticAt_uncurry_of_multilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
x : ((i : ι) → Em i) × G
⊢ CPolynomialAt 𝕜 (F := G × ((i : ι) → Em i))
    (⇑(↑(ContinuousLinearEquiv.prodComm 𝕜 ((i : ι) → Em i) G) : ((i : ι) → Em i) × G →L[𝕜] G × ((i : ι) → Em i)) :
      (a : ((i : ι) → Em i) × G) → G × ((i : ι) → Em i))
    x

Tactic:
have : CPolynomialAt 𝕜 (ContinuousLinearEquiv.prodComm 𝕜 (Π i, Em i) G).toContinuousLinearMap x :=
    ContinuousLinearMap.cpolynomialAt _ _
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
x : ((i : ι) → Em i) × G
this :
  CPolynomialAt 𝕜 (F := G × ((i : ι) → Em i))
    (⇑(↑(ContinuousLinearEquiv.prodComm 𝕜 ((i : ι) → Em i) G) : ((i : ι) → Em i) × G →L[𝕜] G × ((i : ι) → Em i)) :
      (a : ((i : ι) → Em i) × G) → G × ((i : ι) → Em i))
    x
⊢ CPolynomialAt 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) x

Tactic:
f.flipLinear.cpolynomialAt_uncurry_of_multilinear.comp this

Premises used: ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, CPolynomialAt.comp, ContinuousMultilinearMap.flipLinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
x : ((i : ι) → Em i) × G
this :
  CPolynomialAt 𝕜 (F := G × ((i : ι) → Em i))
    (⇑(↑(ContinuousLinearEquiv.prodComm 𝕜 ((i : ι) → Em i) G) : ((i : ι) → Em i) × G →L[𝕜] G × ((i : ι) → Em i)) :
      (a : ((i : ι) → Em i) × G) → G × ((i : ι) → Em i))
    x
⊢ CPolynomialAt 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) x

Tactic:
exact f.flipLinear.cpolynomialAt_uncurry_of_multilinear.comp this

Premises used: ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, CPolynomialAt.comp, ContinuousMultilinearMap.flipLinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
s : Set (((i : ι) → Em i) × G)
⊢ CPolynomialOn 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) s

Tactic:
fun _ _ ↦ f.cpolynomialAt_uncurry_of_linear

Premises used: ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
s : Set (((i : ι) → Em i) × G)
⊢ AnalyticOnNhd 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) s

Tactic:
f.cpolyomialOn_uncurry_of_linear.analyticOnNhd

Premises used: CPolynomialOn.analyticOnNhd, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
s : Set (((i : ι) → Em i) × G)
⊢ AnalyticOn 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) s

Tactic:
f.analyticOnNhd_uncurry_of_linear.analyticOn

Premises used: AnalyticOnNhd.analyticOn, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
x : ((i : ι) → Em i) × G
⊢ AnalyticAt 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) x

Tactic:
f.cpolynomialAt_uncurry_of_linear.analyticAt

Premises used: ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, CPolynomialAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
s : Set (((i : ι) → Em i) × G)
x : ((i : ι) → Em i) × G
⊢ AnalyticWithinAt 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) s x

Tactic:
f.analyticAt_uncurry_of_linear.analyticWithinAt

Premises used: ContinuousMultilinearMap.analyticAt_uncurry_of_linear, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
Fm : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : (i : ι) → NormedAddCommGroup (Fm i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (Fm i)
inst_7 : Fintype ι
q : ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) × ContinuousMultilinearMap 𝕜 Em G
⊢ CPolynomialAt 𝕜 (F := ContinuousMultilinearMap 𝕜 Fm G)
    (fun
        (p :
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
            ContinuousMultilinearMap 𝕜 Em G) ↦
      p.2.compContinuousLinearMap (M₁ := Fm) (M₁' := Em) p.1)
    q

Tactic:
cpolynomialAt_uncurry_of_linear
    (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

Premises used: ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
Fm : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : (i : ι) → NormedAddCommGroup (Fm i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (Fm i)
inst_7 : Fintype ι
t :
  Set
    (((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
      ContinuousMultilinearMap 𝕜 Em G)
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap 𝕜 Fm G)
    (fun
        (p :
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
            ContinuousMultilinearMap 𝕜 Em G) ↦
      p.2.compContinuousLinearMap (M₁ := Fm) (M₁' := Em) p.1)
    t

Tactic:
cpolyomialOn_uncurry_of_linear
    (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

Premises used: ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
Fm : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : (i : ι) → NormedAddCommGroup (Fm i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (Fm i)
inst_7 : Fintype ι
t :
  Set
    (((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
      ContinuousMultilinearMap 𝕜 Em G)
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap 𝕜 Fm G)
    (fun
        (p :
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
            ContinuousMultilinearMap 𝕜 Em G) ↦
      p.2.compContinuousLinearMap (M₁ := Fm) (M₁' := Em) p.1)
    t

Tactic:
analyticOnNhd_uncurry_of_linear
    (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

Premises used: ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
Fm : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : (i : ι) → NormedAddCommGroup (Fm i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (Fm i)
inst_7 : Fintype ι
t :
  Set
    (((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
      ContinuousMultilinearMap 𝕜 Em G)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 Fm G)
    (fun
        (p :
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
            ContinuousMultilinearMap 𝕜 Em G) ↦
      p.2.compContinuousLinearMap (M₁ := Fm) (M₁' := Em) p.1)
    t

Tactic:
analyticOn_uncurry_of_linear
    (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

Premises used: ContinuousMultilinearMap.analyticOn_uncurry_of_linear, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
Fm : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : (i : ι) → NormedAddCommGroup (Fm i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (Fm i)
inst_7 : Fintype ι
q : ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) × ContinuousMultilinearMap 𝕜 Em G
⊢ AnalyticAt 𝕜 (F := ContinuousMultilinearMap 𝕜 Fm G)
    (fun
        (p :
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
            ContinuousMultilinearMap 𝕜 Em G) ↦
      p.2.compContinuousLinearMap (M₁ := Fm) (M₁' := Em) p.1)
    q

Tactic:
analyticAt_uncurry_of_linear
    (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

Premises used: ContinuousMultilinearMap.analyticAt_uncurry_of_linear, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
Fm : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : (i : ι) → NormedAddCommGroup (Fm i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (Fm i)
inst_7 : Fintype ι
t :
  Set
    (((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
      ContinuousMultilinearMap 𝕜 Em G)
q : ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) × ContinuousMultilinearMap 𝕜 Em G
⊢ AnalyticWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 Fm G)
    (fun
        (p :
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_7, u_6} (RingHom.id 𝕜) (Fm i) (Em i)) ×
            ContinuousMultilinearMap 𝕜 Em G) ↦
      p.2.compContinuousLinearMap (M₁ := Fm) (M₁' := Em) p.1)
    t q

Tactic:
analyticWithinAt_uncurry_of_linear
    (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

Premises used: ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = f (x + y)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : m ∉ Finset.range n
⊢ n ≤ m

Tactic:
rw [Finset.mem_range, not_lt] at hm

Premises used: Finset.mem_range, not_lt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = f (x + y)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : n ≤ m
rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)

Tactic:
rw [finite m hm]
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = f (x + y)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : n ≤ m
⊢ Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
hf : HasFiniteFPowerSeriesAt f p x n
⊢ HasFPowerSeriesAt f p x

Tactic:
let ⟨r, hf⟩ := hf
  ⟨r, hf.toHasFPowerSeriesOnBall⟩

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, Exists.intro, HasFPowerSeriesAt, _private.0.HasFiniteFPowerSeriesAt.hasFPowerSeriesAt.match_1
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
hf : HasFiniteFPowerSeriesAt f p x n
⊢ ∀ (m : ℕ), n ≤ m → p m = 0

Tactic:
let ⟨_, hf⟩ := hf; hf.finite

Premises used: HasFiniteFPowerSeriesOnBall.finite, _private.0.HasFiniteFPowerSeriesAt.hasFPowerSeriesAt.match_1
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
⊢ HasFiniteFPowerSeriesAt f p x n

Tactic:
⟨r, hf⟩

Premises used: HasFiniteFPowerSeriesAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
hf : HasFiniteFPowerSeriesAt f p x n
⊢ CPolynomialAt 𝕜 f x

Tactic:
⟨p, n, hf⟩

Premises used: Exists.intro, CPolynomialAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
⊢ CPolynomialAt 𝕜 f x

Tactic:
hf.hasFiniteFPowerSeriesAt.cpolynomialAt

Premises used: HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt, HasFiniteFPowerSeriesAt.cpolynomialAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : CPolynomialAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
let ⟨p, _, hp⟩ := hf
  ⟨p, hp.hasFPowerSeriesAt⟩

Premises used: HasFiniteFPowerSeriesAt.hasFPowerSeriesAt, AnalyticAt, Exists.intro, _private.0.CPolynomialAt.analyticAt.match_1
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hf : CPolynomialAt 𝕜 f x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
hf.analyticAt.analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, CPolynomialAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : CPolynomialOn 𝕜 f s
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
fun x hx ↦ (hf x hx).analyticAt

Premises used: AnalyticOnNhd, CPolynomialAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : CPolynomialOn 𝕜 f s
⊢ AnalyticOn 𝕜 f s

Tactic:
hf.analyticOnNhd.analyticOn

Premises used: CPolynomialOn.analyticOnNhd, AnalyticOnNhd.analyticOn