awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedDivisionRing 𝔸
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 : ℕ) ↦ x ^ n / (↑n ! : 𝔸))

Tactic:
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]

Premises used: NormedSpace.expSeries_apply_eq_div'
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedDivisionRing 𝔸
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 : NormedDivisionRing 𝔸
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 : NormedDivisionRing 𝔸
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 : ℕ) ↦ x ^ n / (↑n ! : 𝔸)

Tactic:
(norm_expSeries_div_summable_of_mem_ball 𝕂 x hx).of_norm

Premises used: Summable.of_norm, NormedSpace.norm_expSeries_div_summable_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CharZero 𝕂
inst_4 : CompleteSpace 𝔸
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 : ℕ) ↦ x ^ n / (↑n ! : 𝔸)) (exp x)

Tactic:
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]

Premises used: NormedSpace.expSeries_apply_eq_div'
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CharZero 𝕂
inst_4 : CompleteSpace 𝔸
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 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CharZero 𝕂
inst_4 : CompleteSpace 𝔸
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 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CharZero 𝕂
inst_4 : CompleteSpace 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ exp (-x) = (exp x)⁻¹

Tactic:
letI := invertibleExpOfMemBall hx
  invOf_eq_inv (exp x)

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

Tactic:
exp_add_of_commute_of_mem_ball (Commute.all x y) hx hy

Premises used: NormedSpace.exp_add_of_commute_of_mem_ball, Commute.all
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
⊢ ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0

Tactic:
have {n : ℕ} : (Nat.factorial n : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
apply :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑n.succ ! : 𝕂)⁻¹ / norm.{u_1} (E := 𝕂) (↑n ! : 𝕂)⁻¹) atTop (𝓝 0)
apply₁ : ∀ (n : ℕ), Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂)⁻¹ 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = ∞

Tactic:
apply expSeries_eq_ofScalars 𝕂 𝔸 ▸
    ofScalars_radius_eq_top_of_tendsto 𝔸 _ (Eventually.of_forall fun n => ?_)
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
simp_rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑(n + 1) : 𝕂)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑n.succ ! : 𝕂)⁻¹ / norm.{u_1} (E := 𝕂) (↑n ! : 𝕂)⁻¹) atTop (𝓝 0)

Tactic:
simp_rw [← norm_div, Nat.factorial_succ, Nat.cast_mul, mul_inv_rev, mul_div_right_comm,
      inv_div_inv, norm_mul, div_self this, norm_one, one_mul]

Premises used: Nat.factorial_succ, NormOneClass.norm_one, norm_mul, mul_div_right_comm, Nat.cast_mul, norm_div, mul_inv_rev, inv_div_inv, one_mul, div_self
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
apply : Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (↑(x + 1) : 𝕂)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑(n + 1) : 𝕂)⁻¹) atTop (𝓝 0)

Tactic:
apply norm_zero (E := 𝕂) ▸ Filter.Tendsto.norm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
apply : Tendsto.{0, u_1} (β := 𝕂) (fun (n : ℕ) ↦ (↑n : 𝕂)⁻¹) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (↑(x + 1) : 𝕂)⁻¹) atTop (𝓝 0)

Tactic:
apply (Filter.tendsto_add_atTop_iff_nat (f := fun n => (n : 𝕂)⁻¹) 1).mpr

Premises used: Iff.mpr, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (n : ℕ) ↦ (↑n : 𝕂)⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (n : ℕ) ↦ (↑n : 𝕂)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atTop_nhds_zero_nat

Premises used: tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
n : ℕ
⊢ Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂)⁻¹ 0

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
rw : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)

Tactic:
rw [expSeries_radius_eq_top]

Premises used: NormedSpace.expSeries_radius_eq_top
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
WithTop.top_pos

Premises used: ENNReal.ofNNReal, WithTop.top_pos
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
exact WithTop.top_pos

Premises used: WithTop.top_pos
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
x : 𝔸
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)

Tactic:
norm_expSeries_summable_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

Premises used: Eq.rec, NormedSpace.norm_expSeries_summable_of_mem_ball, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
x : 𝔸
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)‖

Tactic:
norm_expSeries_summable_of_mem_ball' x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

Premises used: NormedSpace.norm_expSeries_summable_of_mem_ball', Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝕂
x : 𝕂
⊢ Eq.{u_2 + 1} (α := 𝔸) ((algebraMap 𝕂 𝔸 : (a : 𝕂) → 𝔸) (exp x) : 𝔸) (exp ((algebraMap 𝕂 𝔸 : (a : 𝕂) → 𝔸) x) : 𝔸)

Tactic:
algebraMap_exp_comm_of_mem_ball x <| (expSeries_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, NormedSpace.algebraMap_exp_comm_of_mem_ball, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
x : 𝔸
⊢ Summable.{u_2, 0} (α := 𝔸) fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x

Tactic:
(norm_expSeries_summable x).of_norm

Premises used: Summable.of_norm, NormedSpace.norm_expSeries_summable
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
x : 𝔸
⊢ Summable.{u_2, 0} (α := 𝔸) fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
(norm_expSeries_summable' x).of_norm

Premises used: Summable.of_norm, NormedSpace.norm_expSeries_summable'
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
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 ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm, NormedSpace.expSeries_hasSum_exp_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
x : 𝔸
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)) (exp x)

Tactic:
expSeries_hasSum_exp_of_mem_ball' x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, NormedSpace.expSeries_hasSum_exp_of_mem_ball', Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
⊢ HasFPowerSeriesOnBall.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp (expSeries 𝕂 𝔸) 0 ∞

Tactic:
expSeries_radius_eq_top 𝕂 𝔸 ▸ hasFPowerSeriesOnBall_exp_of_radius_pos (expSeries_radius_pos _ _)

Premises used: Eq.rec, NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos, NormedSpace.expSeries_radius_eq_top, NormedSpace.expSeries_radius_pos
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
⊢ HasFPowerSeriesAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp (expSeries 𝕂 𝔸) 0

Tactic:
exp_hasFPowerSeriesOnBall.hasFPowerSeriesAt

Premises used: NormedSpace.exp_hasFPowerSeriesOnBall, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
inst_5 : CompleteSpace 𝔸
x : 𝔸
⊢ AnalyticAt 𝕂 exp x

Tactic:
analyticAt_exp_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

Premises used: NormedSpace.analyticAt_exp_of_mem_ball, Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
rw :
  ContinuousOn.{u_1, u_1} (X := 𝔸) exp
    (Metric.eball 0 (radius.{0, u_1, u_1} (𝕜 := ℚ) (E := 𝔸) (F := 𝔸) (expSeries ℚ 𝔸)))
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    exp

Tactic:
rw [← continuousOn_univ, ← Metric.eball_top_eq_univ (0 : 𝔸), ←
    expSeries_radius_eq_top ℚ 𝔸]

Premises used: Metric.eball_top_eq_univ, Rat, NormedSpace.expSeries_radius_eq_top, continuousOn_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
⊢ ContinuousOn.{u_1, u_1} (X := 𝔸) exp
    (Metric.eball 0 (radius.{0, u_1, u_1} (𝕜 := ℚ) (E := 𝔸) (F := 𝔸) (expSeries ℚ 𝔸)))

Tactic:
continuousOn_exp

Premises used: NormedSpace.continuousOn_exp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
⊢ ContinuousOn.{u_1, u_1} (X := 𝔸) exp
    (Metric.eball 0 (radius.{0, u_1, u_1} (𝕜 := ℚ) (E := 𝔸) (F := 𝔸) (expSeries ℚ 𝔸)))

Tactic:
exact continuousOn_exp

Premises used: NormedSpace.continuousOn_exp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
α : Type u_3
l : Filter α
f : α → 𝔸
a : 𝔸
hf : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ exp (f x)) l (𝓝 (exp a))

Tactic:
(exp_continuous.tendsto _).comp hf

Premises used: NormedSpace.exp_continuous, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x y : 𝔸
hxy : Commute x y
⊢ exp (x + y) = exp x * exp y

Tactic:
exp_add_of_commute_of_mem_ball hxy ((expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _)
    ((expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _)

Premises used: NormedSpace.exp_add_of_commute_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
⊢ IsUnit (exp x)

Tactic:
isUnit_exp_of_mem_ball <| (expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _

Premises used: NormedSpace.isUnit_exp_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
inst_3 : Invertible (exp x)
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (exp x) _ = exp (-x)

Tactic:
invOf_exp_of_mem_ball <| (expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _

Premises used: NormedSpace.invOf_exp_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
⊢ (exp x)⁻¹ʳ = exp (-x)

Tactic:
letI := invertibleExp x
  Ring.inverse_invertible _

Premises used: Ring.inverse_invertible, NormedSpace.exp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
rw₄ : exp (-x + x) = 1 ∧ exp (x + -x) = 1
rw₅ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ exp (x + -x) = 1
rw₆ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
rw₇ : Eq.{u_1 + 1} (α := 𝔸) 1 1 ∧ Eq.{u_1 + 1} (α := 𝔸) 1 1
rw₈ rw₉ : Eq.{u_1 + 1} (α := 𝔸) 1 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)

Tactic:
rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]

Premises used: add_neg_cancel, skewAdjoint.mem_iff, Commute.neg_left, NormedSpace.star_exp, NormedSpace.exp_zero, Commute.refl, neg_add_cancel, Commute.neg_right, Iff.mp, Unitary.mem_iff, and_self_iff, NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
rw :
  SemiconjBy x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) a)
    ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) b)
⊢ SemiconjBy x (exp a) (exp b)

Tactic:
rw [exp_eq_tsum ℚ]

Premises used: NormedSpace.exp_eq_tsum, Rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
apply : ∀ (i : ℕ), SemiconjBy x (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
⊢ SemiconjBy x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) a)
    ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) b)

Tactic:
apply SemiconjBy.tsum_right x (expSeries_summable' _) (expSeries_summable' _)

Premises used: NormedSpace.expSeries_summable', SemiconjBy.tsum_right
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ ∀ (i : ℕ), SemiconjBy x (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))

Tactic:
fun _ ↦ h.pow_right _ |>.smul_right _

Premises used: Nat.cast, SemiconjBy.pow_right, Inv.inv, Nat.factorial, SemiconjBy.smul_right
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ ∀ (i : ℕ), SemiconjBy x (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))

Tactic:
exact fun _ ↦ h.pow_right _ |>.smul_right _

Premises used: SemiconjBy.pow_right, SemiconjBy.smul_right
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
this : Invertible (exp b) := invertibleExp b
⊢ exp (-b) * x * exp a = x

Tactic:
simpa [← invOf_exp, mul_assoc, invOf_mul_eq_iff_eq_mul_left] using h.exp_right

Premises used: mul_assoc, invOf_mul_eq_iff_eq_mul_left, SemiconjBy.exp_right, NormedSpace.invOf_exp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
h : (↑∅ : Set ι).Pairwise (Commute on f)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) ⋯)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
h : (↑(Insert.insert a s) : Set ι).Pairwise (Commute on f)
insert : Commute (f a) (∑ x ∈ s, f x)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ Insert.insert a s, f i))
    ((Insert.insert a s).noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]

Premises used: Set.Pairwise.mono, Finset.subset_insert, NormedSpace.exp_add_of_commute, Finset.sum_insert, Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
h : (↑(insert a s) : Set ι).Pairwise (Commute on f)
⊢ Commute (f a) (∑ x ∈ s, f x)

Tactic:
Commute.sum_right _ _ _ fun i hi => ?_

Premises used: Commute.sum_right