awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
h :
  ∀ (x : E),
    (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))) =
      HMul.hMul (α := B)
        ((aeval (f x) : (a : A[X]) → B)
            (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
          B)
        (f x)
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))))
    s z

Tactic:
convert! hp.mul hf

Premises used: AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
x : E
h :
  (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p * X)) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)
h₁ :
  HMul.hMul (α := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
      (HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B)
        ((aeval (f x) : (a : A[X]) → B) X : B)) =
    HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
        ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B) *
      f x
h₂ :
  HMul.hMul (β := B)
      (HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
        ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B))
      ((aeval (f x) : (a : A[X]) → B) X : B) =
    HMul.hMul (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) i : A[X]) : B)
        ((aeval (f x) : (a : A[X]) → B) (HPow.hPow (α := A[X]) X p) : B) *
      f x
⊢ (aeval (f x) : (a : A[X]) → B)
      (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))) =
    HMul.hMul (α := B)
      ((aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
        B)
      (f x)

Tactic:
simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X]

Premises used: pow_succ, mul_assoc, Polynomial.aeval_mul, Polynomial.aeval_X
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticAt 𝕜 f z
p : A[X]
rw :
  ∀ (hf : AnalyticWithinAt 𝕜 f Set.univ z) (p : A[X]),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) Set.univ z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f Set.univ z
p : A[X]
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) Set.univ z

Tactic:
hf.aeval_polynomial p

Premises used: AnalyticWithinAt.aeval_polynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f Set.univ z
p : A[X]
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) Set.univ z

Tactic:
exact hf.aeval_polynomial p

Premises used: AnalyticWithinAt.aeval_polynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticOnNhd 𝕜 f s
p : A[X]
⊢ AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s

Tactic:
fun x hx ↦ (hf x hx).aeval_polynomial p

Premises used: AnalyticOnNhd, AnalyticAt.aeval_polynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticOn 𝕜 f s
p : A[X]
⊢ AnalyticOn.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s

Tactic:
fun x hx ↦ (hf x hx).aeval_polynomial p

Premises used: AnalyticOn, AnalyticWithinAt.aeval_polynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
A : Type u_5
inst_1 : NormedCommRing A
inst_2 : NormedAlgebra 𝕜 A
p : A[X]
⊢ AnalyticOnNhd 𝕜 (F := A) (fun (x : A) ↦ eval x p) Set.univ

Tactic:
analyticOnNhd_id.aeval_polynomial p

Premises used: Polynomial.eval, MonoidHomClass.toMonoidHom, analyticOnNhd_id, RingHomClass.toRingHom, AnalyticOnNhd.aeval_polynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
A : Type u_5
inst_1 : NormedCommRing A
inst_2 : NormedAlgebra 𝕜 A
p : A[X]
⊢ AnalyticOn 𝕜 (F := A) (fun (x : A) ↦ eval x p) Set.univ

Tactic:
analyticOn_id.aeval_polynomial p

Premises used: AnalyticOn.aeval_polynomial, Polynomial.eval, MonoidHomClass.toMonoidHom, analyticOn_id, RingHomClass.toRingHom
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
apply :
  ∀ (k : A),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) ((C : (a : A) → MvPolynomial σ A) k : MvPolynomial σ A))
      z
apply₁ :
  ∀ (p q : MvPolynomial σ A)
    (hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z)
    (hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p + q)) z
apply₂ :
  ∀ (p : MvPolynomial σ A) (i : σ)
    (hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p * X i)) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z

Tactic:
apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
k : A
simp_rw : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (algebraMap A B : (a : A) → B) k) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) ((C : (a : A) → MvPolynomial σ A) k : MvPolynomial σ A)) z

Tactic:
simp_rw [aeval_C]

Premises used: MvPolynomial.aeval_C
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p : MvPolynomial σ A
k : A
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (algebraMap A B : (a : A) → B) k) z

Tactic:
apply analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p q : MvPolynomial σ A
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z
simp_rw :
  AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B)
        ((aeval (f x) : (a : MvPolynomial σ A) → B) q : B))
    z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p + q)) z

Tactic:
simp_rw [map_add]

Premises used: map_add
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p q : MvPolynomial σ A
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B)
        ((aeval (f x) : (a : MvPolynomial σ A) → B) q : B))
    z

Tactic:
hp.add hq

Premises used: AnalyticAt.add
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p q : MvPolynomial σ A
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
hq : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) q) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B)
        ((aeval (f x) : (a : MvPolynomial σ A) → B) q : B))
    z

Tactic:
exact hp.add hq

Premises used: AnalyticAt.add
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p : MvPolynomial σ A
i : σ
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
simp_rw :
  AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ HMul.hMul (α := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B) (f x i)) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p * X i)) z

Tactic:
simp_rw [map_mul, aeval_X]

Premises used: MvPolynomial.aeval_X, map_mul
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p : MvPolynomial σ A
i : σ
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ HMul.hMul (α := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B) (f x i)) z

Tactic:
hp.mul (hf i)

Premises used: AnalyticAt.mul
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p : MvPolynomial σ A
i : σ
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ HMul.hMul (α := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B) (f x i)) z

Tactic:
exact hp.mul (hf i)

Premises used: AnalyticAt.mul
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
s : Set E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) s
p : MvPolynomial σ A
⊢ AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) s

Tactic:
fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p

Premises used: AnalyticOnNhd, AnalyticAt.aeval_mvPolynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedCommRing B
inst_4 : NormedAlgebra 𝕜 B
σ : Type u_5
f : E →L[𝕜] σ → B
p : MvPolynomial σ B
⊢ AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (eval ((f : (a : E) → σ → B) x) : (a : MvPolynomial σ B) → B) p) Set.univ

Tactic:
fun x _ ↦ .aeval_mvPolynomial (fun i ↦ ((ContinuousLinearMap.proj i).comp f).analyticAt x) p

Premises used: ContinuousLinearMap.comp, AnalyticOnNhd, ContinuousLinearMap.analyticAt, ContinuousLinearMap.proj, AnalyticAt.aeval_mvPolynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedCommRing B
inst_4 : NormedAlgebra 𝕜 B
σ : Type u_5
f : σ → E →L[𝕜] B
p : MvPolynomial σ B
⊢ AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (eval fun (x_1 : σ) ↦ (f x_1 : (a : E) → B) x : (a : MvPolynomial σ B) → B) p) Set.univ

Tactic:
fun x _ ↦ .aeval_mvPolynomial (fun i ↦ (f i).analyticAt x) p

Premises used: AnalyticOnNhd, ContinuousLinearMap.analyticAt, AnalyticAt.aeval_mvPolynomial
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedCommRing B
inst_4 : NormedAlgebra 𝕜 B
σ : Type u_5
inst_5 : CompleteSpace 𝕜
inst_6 : T2Space E
inst_7 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] σ → B
p : MvPolynomial σ B
⊢ AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (eval ((f : (a : E) → σ → B) x) : (a : MvPolynomial σ B) → B) p) Set.univ

Tactic:
AnalyticOnNhd.eval_continuousLinearMap { f with cont := f.continuous_of_finiteDimensional } p

Premises used: ContinuousLinearMap.mk, LinearMap.continuous_of_finiteDimensional, AnalyticOnNhd.eval_continuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedCommRing B
inst_4 : NormedAlgebra 𝕜 B
σ : Type u_5
inst_5 : CompleteSpace 𝕜
inst_6 : T2Space E
inst_7 : FiniteDimensional 𝕜 E
f : σ → E →ₗ[𝕜] B
p : MvPolynomial σ B
⊢ AnalyticOnNhd.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (eval fun (x_1 : σ) ↦ (f x_1 : (a : E) → B) x : (a : MvPolynomial σ B) → B) p) Set.univ

Tactic:
AnalyticOnNhd.eval_linearMap (.pi f) p

Premises used: AnalyticOnNhd.eval_linearMap, LinearMap.pi
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
σ : Type u_5
inst_1 : CompleteSpace 𝕜
inst_2 : Fintype σ
p : MvPolynomial σ 𝕜
⊢ AnalyticOnNhd 𝕜 (F := 𝕜) (fun (x : σ → 𝕜) ↦ (eval x : (a : MvPolynomial σ 𝕜) → 𝕜) p) Set.univ

Tactic:
AnalyticOnNhd.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p

Premises used: LinearMap.id, AnalyticOnNhd.eval_linearMap
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have : 0 < (n : ℝ) := Nat.cast_pos.2 hn
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : ‖p n‖₊ * r ^ n ≤ 1
| (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)

Tactic:
rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]

Premises used: Iff.mpr, NNReal.rpow_natCast, mul_inv_cancel₀, NNReal.rpow_mul, inv_pos, ENNReal.coe_le_one_iff, Nat.cast, LT.lt.ne', ENNReal.coe_mul, Inv.inv, one_div, mul_comm, NNReal.one_rpow, NNReal.rpow_one, ENNReal.le_inv_iff_mul_le, NNReal.mul_rpow, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : LT.lt (α := ℝ) 0 (↑n : ℝ)
conv_lhs : (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1
conv_lhs₁ : ‖p n‖₊ * r ^ n ≤ 1 ↔ ‖p n‖₊ * r ^ n ≤ 1
⊢ (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1

Tactic:
conv_lhs =>
      rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]

Premises used: Iff.mpr, NNReal.rpow_natCast, mul_inv_cancel₀, NNReal.rpow_mul, inv_pos, ENNReal.coe_le_one_iff, Nat.cast, LT.lt.ne', ENNReal.coe_mul, Inv.inv, one_div, mul_comm, NNReal.one_rpow, NNReal.rpow_one, ENNReal.le_inv_iff_mul_le, NNReal.mul_rpow, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)

Tactic:
have :
    ∀ (r : ℝ≥0) {n},
      0 < n → ((r : ℝ≥0∞) ≤ 1 / ↑(‖p n‖₊ ^ (1 / (n : ℝ))) ↔ ‖p n‖₊ * r ^ n ≤ 1) := by
    intro r n hn
    have : 0 < (n : ℝ) := Nat.cast_pos.2 hn
    conv_lhs =>
      rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
a : p.radius ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
a₁ : liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop ≤ p.radius
⊢ p.radius = liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ p.radius ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop

Tactic:
ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
a :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius),
    (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
⊢ p.radius ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt