awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (hasFPowerSeriesOnBall_exp_of_radius_pos h).analyticAt_of_mem hx

Premises used: NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos, HasFPowerSeriesOnBall.analyticAt_of_mem
-- 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 y : 𝔸
hxy : Commute 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
rw :
  Eq.{u_2 + 1} (α := 𝔸)
    ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) (x + y))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))
⊢ exp (x + y) = exp x * exp y

Tactic:
rw [exp_eq_tsum 𝕂,
    tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
      (norm_expSeries_summable_of_mem_ball' x hx) (norm_expSeries_summable_of_mem_ball' y hy)]

Premises used: NormedSpace.exp_eq_tsum, NormedSpace.norm_expSeries_summable_of_mem_ball', tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
-- 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 y : 𝔸
hxy : Commute 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
f : fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
L : SummationFilter.unconditional ℕ
| ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)

Tactic:
congr
-- 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 y : 𝔸
hxy : Commute 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
f : ∀ (x_1 : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ ((x + y) ^ x_1)
| fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)

Tactic:
ext
-- 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 y : 𝔸
hxy : Commute 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
x_1 : ℕ
f :
  ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2))
| HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ ((x + y) ^ x_1)

Tactic:
rw [hxy.add_pow' _, Finset.smul_sum]

Premises used: Commute.add_pow', Finset.smul_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 y : 𝔸
hxy : Commute 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
f :
  ∀ (x_1 : ℕ),
    ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2))
L : SummationFilter.unconditional ℕ
| ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)

Tactic:
congr
    ext
    rw [hxy.add_pow' _, Finset.smul_sum]

Premises used: Commute.add_pow', Finset.smul_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 y : 𝔸
hxy : Commute 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
conv_lhs :
  Eq.{u_2 + 1} (α := 𝔸)
    (∑' (x_1 : ℕ),
      ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2)))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))
⊢ Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))

Tactic:
conv_lhs =>
    congr
    ext
    rw [hxy.add_pow' _, Finset.smul_sum]

Premises used: Commute.add_pow', Finset.smul_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 y : 𝔸
hxy : Commute 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
⊢ Eq.{u_2 + 1} (α := 𝔸)
    (∑' (x_1 : ℕ),
      ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2)))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))

Tactic:
tsum_congr fun n => Finset.sum_congr rfl fun kl hkl => ?_

Premises used: tsum_congr, Finset.sum_congr, rfl
-- 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 y : 𝔸
hxy : Commute 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
refine :
  ∀ (n : ℕ) (kl : ℕ × ℕ) (hkl : kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (n.choose kl.1 • (x ^ kl.1 * y ^ kl.2)) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2)
⊢ Eq.{u_2 + 1} (α := 𝔸)
    (∑' (x_1 : ℕ),
      ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2)))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))

Tactic:
refine tsum_congr fun n => Finset.sum_congr rfl fun kl hkl => ?_

Premises used: tsum_congr, Finset.sum_congr, rfl
-- 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 y : 𝔸
hxy : Commute 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
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
rw :
  ((↑n ! : 𝕂)⁻¹ * ((↑n ! : 𝕂) / HMul.hMul (α := 𝕂) (↑kl.1! : 𝕂) (↑kl.2! : 𝕂))) • (x ^ kl.1 * y ^ kl.2) =
    HMul.hMul (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (↑kl.2! : 𝕂)⁻¹ • (x ^ kl.1 * y ^ kl.2)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (n.choose kl.1 • (x ^ kl.1 * y ^ kl.2)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2)

Tactic:
rw [← Nat.cast_smul_eq_nsmul 𝕂, smul_smul, smul_mul_smul_comm, ← Finset.mem_antidiagonal.mp hkl,
    Nat.cast_add_choose, Finset.mem_antidiagonal.mp hkl]

Premises used: smul_smul, Nat.cast_add_choose, smul_mul_smul_comm, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, Nat.cast_smul_eq_nsmul
-- 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 y : 𝔸
hxy : Commute 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
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
⊢ ((↑n ! : 𝕂)⁻¹ * ((↑n ! : 𝕂) / HMul.hMul (α := 𝕂) (↑kl.1! : 𝕂) (↑kl.2! : 𝕂))) • (x ^ kl.1 * y ^ kl.2) =
    HMul.hMul (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (↑kl.2! : 𝕂)⁻¹ • (x ^ kl.1 * y ^ kl.2)

Tactic:
field_simp [n.factorial_ne_zero]

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

Tactic:
rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]

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

Tactic:
hx

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

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

Tactic:
have hnx : -x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := by
      rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
      exact hx
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
rw : exp (-x + x) = 1
rw₁ : Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := 𝔸) 1 1
⊢ exp (-x) * exp x = 1

Tactic:
rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,
      neg_add_cancel, exp_zero]

Premises used: Commute.neg_left, NormedSpace.exp_add_of_commute_of_mem_ball, NormedSpace.exp_zero, Commute.refl, neg_add_cancel
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
rw : exp (x + -x) = 1
rw₁ : Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := 𝔸) 1 1
⊢ exp x * exp (-x) = 1

Tactic:
rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx,
      add_neg_cancel, exp_zero]

Premises used: add_neg_cancel, NormedSpace.exp_add_of_commute_of_mem_ball, NormedSpace.exp_zero, Commute.refl, Commute.neg_right
-- 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
⊢ IsUnit (exp x)

Tactic:
@isUnit_of_invertible _ _ _ (invertibleExpOfMemBall hx)

Premises used: isUnit_of_invertible
-- 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
inst_5 : Invertible (exp x)
this : Invertible (exp x) := invertibleExpOfMemBall hx
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (exp x) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (exp x) _

Tactic:
(rfl : ⅟(exp x) = _)

Premises used: rfl
-- 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
inst_5 : Invertible (exp x)
this : Invertible (exp x) := invertibleExpOfMemBall hx
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (exp x) _ = exp (-x)

Tactic:
convert! (rfl : ⅟(exp x) = _)

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
rw :
  Eq.{u_3 + 1} (α := 𝔹)
    ((f : (a : 𝔸) → 𝔹) ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) x) :
      𝔹)
    ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x) :
      𝔹)
⊢ Eq.{u_3 + 1} (α := 𝔹) ((f : (a : 𝔸) → 𝔹) (exp x) : 𝔹) (exp ((f : (a : 𝔸) → 𝔹) x) : 𝔹)

Tactic:
rw [exp_eq_tsum 𝕂, exp_eq_tsum 𝕂]

Premises used: NormedSpace.exp_eq_tsum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Eq.{u_3 + 1} (α := 𝔹)
    ((f : (a : 𝔸) → 𝔹) ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) x) :
      𝔹)
    ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x) :
      𝔹)

Tactic:
((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans ?_

Premises used: HasSum.map, HasSum.tsum_eq, Summable.hasSum, Eq.symm, NormedSpace.expSeries_summable_of_mem_ball', Eq.trans
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
refine :
  Eq.{u_3 + 1} (α := 𝔹)
    (∑' (b : ℕ),
      Function.comp.{1, u_2 + 1, u_3 + 1} (β := 𝔸) (⇑f : (a : 𝔸) → 𝔹)
        (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)) b)
    ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x))
⊢ Eq.{u_3 + 1} (α := 𝔹)
    ((f : (a : 𝔸) → 𝔹) ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) x) :
      𝔹)
    ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x) :
      𝔹)

Tactic:
refine ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans ?_

Premises used: HasSum.map, HasSum.tsum_eq, Summable.hasSum, Eq.symm, NormedSpace.expSeries_summable_of_mem_ball', Eq.trans
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
dsimp :
  Eq.{u_3 + 1} (α := 𝔹) (∑' (b : ℕ), (f : (a : 𝔸) → 𝔹) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑b ! : 𝕂)⁻¹ (x ^ b)))
    (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔹) ((f : (a : 𝔸) → 𝔹) x : 𝔹) n))
⊢ Eq.{u_3 + 1} (α := 𝔹)
    (∑' (b : ℕ),
      Function.comp.{1, u_2 + 1, u_3 + 1} (β := 𝔸) (⇑f : (a : 𝔸) → 𝔹)
        (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)) b)
    ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x))

Tactic:
dsimp only [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
simp_rw :
  Eq.{u_3 + 1} (α := 𝔹)
    (∑' (b : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (β := 𝔹) (↑b ! : 𝕂)⁻¹ ((f : (a : 𝔸) → 𝔹) (x ^ b) : 𝔹))
    (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔹) ((f : (a : 𝔸) → 𝔹) x : 𝔹) n))
⊢ Eq.{u_3 + 1} (α := 𝔹) (∑' (b : ℕ), (f : (a : 𝔸) → 𝔹) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑b ! : 𝕂)⁻¹ (x ^ b)))
    (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔹) ((f : (a : 𝔸) → 𝔹) x : 𝔹) n))

Tactic:
simp_rw [map_inv_natCast_smul f 𝕂 𝕂, map_pow]

Premises used: map_pow, map_inv_natCast_smul
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CharZero 𝕂
inst_4 : CompleteSpace 𝕂
x : 𝕂
hx : Membership.mem (γ := Set 𝕂) (Metric.eball 0 (radius.{u_1, u_1, u_1} (𝕜 := 𝕂) (E := 𝕂) (F := 𝕂) (expSeries 𝕂 𝕂))) x
⊢ Eq.{u_2 + 1} (α := 𝔸) ((algebraMap 𝕂 𝔸 : (a : 𝕂) → 𝔸) (exp x) : 𝔸) (exp ((algebraMap 𝕂 𝔸 : (a : 𝕂) → 𝔸) x) : 𝔸)

Tactic:
map_exp_of_mem_ball (algebraMap _ _) (algebraMapCLM _ _).continuous _ hx

Premises used: Algebra.algebraMap, algebraMapCLM, NormedSpace.map_exp_of_mem_ball, ContinuousLinearMap.continuous
-- 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
change : Summable (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦ x ^ n / (↑n ! : 𝔸))
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x ^ n / (↑n ! : 𝔸)‖

Tactic:
change Summable (norm ∘ _)

Premises used: Norm.norm, Function.comp, Summable, SummationFilter.unconditional