awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
inl : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸) → star (exp x) = exp (star x)
inr : ∀ (val : Algebra ℚ 𝔸), star (exp x) = exp (star x)
⊢ star (exp x) = exp (star x)

Tactic:
obtain _ | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)

Premises used: Rat, Algebra, isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
⊢ star (exp x) = exp (star x)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr :
  Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star x ^ n))
inr₁ :
  Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star (x ^ n)))
inr₂ :
  Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (∑' (n : ℕ), star (HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
⊢ star (exp x) = exp (star x)

Tactic:
simp_rw [exp_eq_tsum ℚ, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]

Premises used: NormedSpace.exp_eq_tsum, Rat, star_inv_natCast_smul, tsum_star, star_pow
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst_3 : Monoid R
inst_4 : SMul ℚ R
inst_5 : MulAction R 𝔸
inst_6 : Algebra ℚ 𝔸
inst_7 : IsScalarTower ℚ R 𝔸
inst_8 : SetLike S 𝔸
inst_9 : SubsemiringClass S 𝔸
inst_10 : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst_1] (↑s : Set 𝔸)
x : 𝔸
h : x ∈ s
⊢ SMulMemClass S ℚ 𝔸

Tactic:
have := SMulMemClass.ofIsScalarTower S ℚ R 𝔸
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst_3 : Monoid R
inst_4 : SMul ℚ R
inst_5 : MulAction R 𝔸
inst_6 : Algebra ℚ 𝔸
inst_7 : IsScalarTower ℚ R 𝔸
inst_8 : SetLike S 𝔸
inst_9 : SubsemiringClass S 𝔸
inst_10 : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst_1] (↑s : Set 𝔸)
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
rw : (fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x ∈ s
⊢ exp x ∈ s

Tactic:
rw [exp_eq_tsum ℚ]

Premises used: NormedSpace.exp_eq_tsum, Rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst_3 : Monoid R
inst_4 : SMul ℚ R
inst_5 : MulAction R 𝔸
inst_6 : Algebra ℚ 𝔸
inst_7 : IsScalarTower ℚ R 𝔸
inst_8 : SetLike S 𝔸
inst_9 : SubsemiringClass S 𝔸
inst_10 : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst_1] (↑s : Set 𝔸)
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ (fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x ∈ s

Tactic:
tsum_mem h_closed fun i => SMulMemClass.smul_mem _ <| pow_mem h _

Premises used: SMulMemClass.smul_mem, Set.Mem, tsum_mem, Nat.cast, Inv.inv, Nat.factorial, pow_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst_3 : Monoid R
inst_4 : SMul ℚ R
inst_5 : MulAction R 𝔸
inst_6 : Algebra ℚ 𝔸
inst_7 : IsScalarTower ℚ R 𝔸
inst_8 : SetLike S 𝔸
inst_9 : SubsemiringClass S 𝔸
inst_10 : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst_1] (↑s : Set 𝔸)
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ (fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x ∈ s

Tactic:
exact tsum_mem h_closed fun i => SMulMemClass.smul_mem _ <| pow_mem h _

Premises used: SMulMemClass.smul_mem, tsum_mem, pow_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
h : IsSelfAdjoint x
⊢ IsSelfAdjoint (exp x)

Tactic:
(star_exp x).trans <| h.symm ▸ rfl

Premises used: IsSelfAdjoint, Eq.rec, NormedSpace.star_exp, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
inl : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸) → Commute x (exp y)
inr : ∀ (val : Algebra ℚ 𝔸), Commute x (exp y)
⊢ Commute x (exp y)

Tactic:
obtain _ | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)

Premises used: Rat, Algebra, isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
h_1 : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
⊢ Commute x (exp y)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
val : Algebra ℚ 𝔸
inr : Commute x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) y)
⊢ Commute x (exp y)

Tactic:
rw [exp_eq_tsum ℚ]

Premises used: NormedSpace.exp_eq_tsum, Rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
val : Algebra ℚ 𝔸
⊢ Commute x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) y)

Tactic:
Commute.tsum_right x fun n => (h.pow_right n).smul_right _

Premises used: Commute.pow_right, Commute.tsum_right, Nat.cast, Commute.smul_right, Inv.inv, Nat.factorial
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
val : Algebra ℚ 𝔸
⊢ Commute x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) y)

Tactic:
exact Commute.tsum_right x fun n => (h.pow_right n).smul_right _

Premises used: Commute.pow_right, Commute.tsum_right, Commute.smul_right
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute (exp x) y

Tactic:
h.symm.exp_right.symm

Premises used: Commute.exp_right, Commute.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute (exp x) (exp y)

Tactic:
h.exp_left.exp_right

Premises used: Commute.exp_right, Commute.exp_left
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
rw : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n * (↑n ! : 𝔸)⁻¹
rw₁ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = (↑n ! : 𝔸)⁻¹ * x ^ n
rw₂ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
rw₄ rw₅ : HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n / (↑n ! : 𝔸)

Tactic:
rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]

Premises used: inv_natCast_smul_eq, NormedSpace.expSeries_apply_eq, div_eq_mul_inv, HPow.hPow, Nat.factorial, smul_eq_mul, Commute.eq, Commute.inv_left₀, Nat.cast_commute
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
⊢ Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸) (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦ x ^ n / (↑n ! : 𝔸)

Tactic:
funext (expSeries_apply_eq_div x)

Premises used: NormedSpace.expSeries_apply_eq_div, funext
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x = ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)

Tactic:
tsum_congr (expSeries_apply_eq_div x)

Premises used: tsum_congr, NormedSpace.expSeries_apply_eq_div, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : DivisionRing 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : CharZero 𝔸
rw :
  FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) = fun (x : 𝔸) ↦
    ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp fun (x : 𝔸) ↦ ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)

Tactic:
rw [exp_eq_expSeries_sum ℚ]

Premises used: Rat, NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : DivisionRing 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : CharZero 𝔸
h :
  ∀ (x : 𝔸),
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x = ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) = fun (x : 𝔸) ↦
    ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : DivisionRing 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : CharZero 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x = ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)

Tactic:
expSeries_sum_eq_div x

Premises used: NormedSpace.expSeries_sum_eq_div
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : DivisionRing 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : CharZero 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x = ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)

Tactic:
exact expSeries_sum_eq_div x

Premises used: NormedSpace.expSeries_sum_eq_div
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)

Tactic:
(expSeries 𝕂 𝔸).summable_norm_apply hx

Premises used: NormedSpace.expSeries, FormalMultilinearSeries.summable_norm_apply
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
change :
  Summable
    (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)‖

Tactic:
change Summable (norm ∘ _)

Premises used: Norm.norm, Function.comp, Summable, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
rw :
  Summable
    (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
      (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
⊢ Summable
    (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))

Tactic:
rw [← expSeries_apply_eq']

Premises used: NormedSpace.expSeries_apply_eq'
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable
    (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
      (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)

Tactic:
norm_expSeries_summable_of_mem_ball x hx

Premises used: NormedSpace.norm_expSeries_summable_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable
    (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
      (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)

Tactic:
exact norm_expSeries_summable_of_mem_ball x hx

Premises used: NormedSpace.norm_expSeries_summable_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable.{u_2, 0} (α := 𝔸) fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x

Tactic:
(norm_expSeries_summable_of_mem_ball x hx).of_norm

Premises used: Summable.of_norm, NormedSpace.norm_expSeries_summable_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable.{u_2, 0} (α := 𝔸) fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
(norm_expSeries_summable_of_mem_ball' x hx).of_norm

Premises used: Summable.of_norm, NormedSpace.norm_expSeries_summable_of_mem_ball'
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ HasSum (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) (exp x)

Tactic:
simpa only [exp_eq_expSeries_sum 𝕂, expSeries_sum_eq_rat] using
    FormalMultilinearSeries.hasSum (expSeries 𝕂 𝔸) hx

Premises used: FormalMultilinearSeries.hasSum, NormedSpace.expSeries_sum_eq_rat, NormedSpace.expSeries, NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
rw : HasSum (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) (exp x)
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)) (exp x)

Tactic:
rw [← expSeries_apply_eq']

Premises used: NormedSpace.expSeries_apply_eq'
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ HasSum (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) (exp x)

Tactic:
expSeries_hasSum_exp_of_mem_ball x hx

Premises used: NormedSpace.expSeries_hasSum_exp_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ HasSum (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) (exp x)

Tactic:
exact expSeries_hasSum_exp_of_mem_ball x hx

Premises used: NormedSpace.expSeries_hasSum_exp_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
h : 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
⊢ HasFPowerSeriesOnBall.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp (expSeries 𝕂 𝔸) 0
    (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))

Tactic:
simpa only [exp_eq_expSeries_sum 𝕂, expSeries_sum_eq_rat] using
    (expSeries 𝕂 𝔸).hasFPowerSeriesOnBall h

Premises used: NormedSpace.expSeries_sum_eq_rat, NormedSpace.expSeries, FormalMultilinearSeries.hasFPowerSeriesOnBall, NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
h : 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
⊢ HasFPowerSeriesAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp (expSeries 𝕂 𝔸) 0

Tactic:
simpa only [exp, expSeries_sum_eq_rat] using
    (hasFPowerSeriesOnBall_exp_of_radius_pos h).hasFPowerSeriesAt

Premises used: NormedSpace.exp, NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos, NormedSpace.expSeries_sum_eq_rat, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
⊢ ContinuousOn (FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸))
    (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))

Tactic:
have := FormalMultilinearSeries.continuousOn (p := expSeries 𝕂 𝔸)
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
this :
  ContinuousOn (FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸))
    (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
⊢ ContinuousOn.{u_2, u_2} (X := 𝔸) exp
    (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))

Tactic:
simpa only [exp_eq_expSeries_sum 𝕂, expSeries_sum_eq_rat] using this

Premises used: NormedSpace.expSeries_sum_eq_rat, NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
pos : ∀ (h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0), AnalyticAt 𝕂 exp x
neg : ∀ (h : ¬radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0), AnalyticAt 𝕂 exp x
⊢ AnalyticAt 𝕂 exp x

Tactic:
by_cases h : (expSeries 𝕂 𝔸).radius = 0

Premises used: FormalMultilinearSeries.radius, NormedSpace.expSeries
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
⊢ Membership.mem (γ := Set 𝔸) (Metric.eball 0 0) x

Tactic:
rw [h] at hx
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
hx₁ : Membership.mem (γ := Set 𝔸) (Metric.eball 0 0) x
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0

Tactic:
rw [h] at hx
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 0) x
h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 exp x

Tactic:
(ENNReal.not_lt_zero hx).elim

Premises used: False.elim, ENNReal.not_lt_zero
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 0) x
h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 exp x

Tactic:
exact (ENNReal.not_lt_zero hx).elim

Premises used: False.elim, ENNReal.not_lt_zero
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h : ¬radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
⊢ 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)

Tactic:
have h := pos_iff_ne_zero.mpr h
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h_1 : ¬radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
h : 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
⊢ AnalyticAt 𝕂 exp x

Tactic:
(hasFPowerSeriesOnBall_exp_of_radius_pos h).analyticAt_of_mem hx

Premises used: NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos, HasFPowerSeriesOnBall.analyticAt_of_mem