awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (i : ι) (hi : i ∈ s), Commute (f a) (f i)
⊢ Commute (f a) (∑ x ∈ s, f x)

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

Premises used: Commute.sum_right
-- 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)
i : ι
hi : i ∈ s
⊢ Commute (f a) (f i)

Tactic:
h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_self, Set.Pairwise.of_refl, Finset.mem_insert_of_mem
-- 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)
i : ι
hi : i ∈ s
⊢ Commute (f a) (f i)

Tactic:
exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_self, Set.Pairwise.of_refl, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) ⋯)
insert :
  ∀ (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)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ Insert.insert a s, f i))
      ((Insert.insert a s).noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)

Premises used: Insert.insert, Commute.sum_right, NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) ⋯)
insert :
  ∀ (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)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ Insert.insert a s, f i))
      ((Insert.insert a s).noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)

Premises used: Insert.insert, Commute.sum_right, NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
zero : exp 0 = HPow.hPow (β := ℕ) (exp x) 0
zero₁ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
zero₂ zero₃ : Eq.{u_1 + 1} (α := 𝔸) 1 1
⊢ exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0

Tactic:
rw [zero_smul, pow_zero, exp_zero]

Premises used: pow_zero, NormedSpace.exp_zero, zero_smul
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
succ : exp (n • x + x) = exp x ^ (n + 1)
succ₁ : exp (n • x + x) = exp x ^ n * exp x
succ₂ : exp (n • x) * exp x = exp x ^ n * exp x
succ₃ succ₄ : exp x ^ n * exp x = exp x ^ n * exp x
⊢ exp ((n + 1) • x) = exp x ^ (n + 1)

Tactic:
rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]

Premises used: pow_succ, Commute.smul_left, Commute.refl, NormedSpace.exp_add_of_commute, succ_nsmul
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
n : ℕ
x : 𝔸
zero : exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0
succ : ∀ (n : ℕ) (ih : exp (n • x) = exp x ^ n), exp ((n + 1) • x) = exp x ^ (n + 1)
⊢ exp (n • x) = exp x ^ n

Tactic:
induction n with
  | zero => rw [zero_smul, pow_zero, exp_zero]
  | succ n ih => rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]

Premises used: pow_succ, Commute.smul_left, pow_zero, NormedSpace.exp_zero, zero_smul, Commute.refl, NormedSpace.exp_add_of_commute, succ_nsmul
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
𝔹 : Type u_2
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : NormedRing 𝔹
inst_4 : Algebra ℚ 𝔹
F : Type u_3
inst_5 : FunLike F 𝔸 𝔹
inst_6 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
⊢ Eq.{u_2 + 1} (α := 𝔹) ((f : (a : 𝔸) → 𝔹) (exp x) : 𝔹) (exp ((f : (a : 𝔸) → 𝔹) x) : 𝔹)

Tactic:
map_exp_of_mem_ball f hf x <| (expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _

Premises used: NormedSpace.map_exp_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
G : Type u_3
inst_3 : Monoid G
inst_4 : MulSemiringAction G 𝔸
inst_5 : ContinuousConstSMul G 𝔸
g : G
x : 𝔸
⊢ exp (g • x) = g • exp x

Tactic:
(map_exp (MulSemiringAction.toRingHom G 𝔸 g) (continuous_const_smul g) x).symm

Premises used: ContinuousConstSMul.continuous_const_smul, NormedSpace.map_exp, MulSemiringAction.toRingHom, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
y : 𝔸ˣ
x : 𝔸
⊢ exp ((↑y : 𝔸) * x * (↑y⁻¹ : 𝔸)) = (↑y : 𝔸) * exp x * (↑y⁻¹ : 𝔸)

Tactic:
exp_smul (ConjAct.toConjAct y) x

Premises used: ConjAct.toConjAct, NormedSpace.exp_smul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
y : 𝔸ˣ
x : 𝔸
⊢ exp ((↑y⁻¹ : 𝔸) * x * (↑y : 𝔸)) = (↑y⁻¹ : 𝔸) * exp x * (↑y : 𝔸)

Tactic:
exp_units_conj _ _

Premises used: NormedSpace.exp_units_conj
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
𝔹 : Type u_2
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : NormedRing 𝔹
inst_4 : NormedAlgebra ℚ 𝔹
inst_5 : CompleteSpace 𝔹
x : 𝔸 × 𝔹
⊢ (exp x).1 = exp x.1

Tactic:
map_exp (RingHom.fst 𝔸 𝔹) continuous_fst x

Premises used: NormedSpace.map_exp, setOf, continuous_fst, RingHom.fst
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
𝔹 : Type u_2
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : NormedRing 𝔹
inst_4 : NormedAlgebra ℚ 𝔹
inst_5 : CompleteSpace 𝔹
x : 𝔸 × 𝔹
⊢ (exp x).2 = exp x.2

Tactic:
map_exp (RingHom.snd 𝔸 𝔹) continuous_snd x

Premises used: NormedSpace.map_exp, setOf, continuous_snd, RingHom.snd
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : (i : ι) → NormedRing (𝔸 i)
inst_2 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
i : ι
⊢ exp x i = exp (x i)

Tactic:
let ⟨_⟩ := nonempty_fintype ι
  map_exp (Pi.evalRingHom 𝔸 i) (continuous_apply _) x

Premises used: _private.0.Pi.coe_exp.match_1, NormedSpace.map_exp, NormedSpace.exp, nonempty_fintype, Pi.evalRingHom, continuous_apply, Eq
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : (i : ι) → NormedRing (𝔸 i)
inst_2 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
⊢ exp x = fun (i : ι) ↦ exp (x i)

Tactic:
funext <| Pi.coe_exp x

Premises used: funext, Pi.coe_exp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedRing (𝔸 i)
inst_3 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
h : ∀ (i : ι), Function.update (β := 𝔸) (exp x) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj) i
⊢ Function.update (β := 𝔸) (exp x) j (exp xj) = exp (Function.update (β := 𝔸) x j xj)

Tactic:
ext i
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedRing (𝔸 i)
inst_3 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
h : Function.update (β := 𝔸) (fun (i : ι) ↦ exp (x i)) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj i)
⊢ Function.update (β := 𝔸) (exp x) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj) i

Tactic:
simp_rw [Pi.exp_def]

Premises used: Pi.exp_def
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedRing (𝔸 i)
inst_3 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (β := 𝔸) (fun (i : ι) ↦ exp (x i)) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj i)

Tactic:
(Function.apply_update (fun i => exp) x j xj i).symm

Premises used: Function.apply_update, NormedSpace.exp, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedRing (𝔸 i)
inst_3 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (β := 𝔸) (fun (i : ι) ↦ exp (x i)) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj i)

Tactic:
exact (Function.apply_update (fun i => exp) x j xj i).symm

Premises used: Function.apply_update, NormedSpace.exp, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
x : 𝔸
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x ^ n / (↑n ! : 𝔸)‖

Tactic:
norm_expSeries_div_summable_of_mem_ball ℚ x
    ((expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _)

Premises used: Rat, Eq.rec, NormedSpace.expSeries_radius_eq_top, NormedSpace.norm_expSeries_div_summable_of_mem_ball, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
⊢ Summable.{u_1, 0} (α := 𝔸) fun (n : ℕ) ↦ x ^ n / (↑n ! : 𝔸)

Tactic:
(norm_expSeries_div_summable x).of_norm

Premises used: Summable.of_norm, NormedSpace.norm_expSeries_div_summable
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
⊢ HasSum (fun (n : ℕ) ↦ x ^ n / (↑n ! : 𝔸)) (exp x)

Tactic:
expSeries_div_hasSum_exp_of_mem_ball ℚ x ((expSeries_radius_eq_top ℚ 𝔸).symm ▸ edist_lt_top _ _)

Premises used: Rat, Eq.rec, NormedSpace.expSeries_div_hasSum_exp_of_mem_ball, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
⊢ exp (-x) = (exp x)⁻¹

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

Premises used: NormedSpace.exp_neg_of_mem_ball, Rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
z : ℤ
x : 𝔸
inl : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)
inr : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
⊢ exp (z • x) = exp x ^ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inl : exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = exp x ^ n
inl₁ : exp (n • x) = exp x ^ n
inl₂ inl₃ : exp x ^ n = exp x ^ n
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)

Tactic:
rw [zpow_natCast, natCast_zsmul, exp_nsmul]

Premises used: zpow_natCast, NormedSpace.exp_nsmul, natCast_zsmul
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (exp x ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = (exp x ^ n)⁻¹
inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x))⁻¹ = (exp x ^ n)⁻¹
inr₄ : (exp (n • x))⁻¹ = (exp x ^ n)⁻¹
inr₅ inr₆ : (exp x ^ n)⁻¹ = (exp x ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))

Tactic:
rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]

Premises used: zpow_natCast, neg_smul, NormedSpace.exp_nsmul, zpow_neg, NormedSpace.exp_neg, natCast_zsmul
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
y x : 𝔸
hy : y ≠ 0
⊢ exp (y * x * y⁻¹) = y * exp x * y⁻¹

Tactic:
exp_units_conj (Units.mk0 y hy) x

Premises used: Units.mk0, NormedSpace.exp_units_conj
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
y x : 𝔸
hy : y ≠ 0
⊢ exp (y⁻¹ * x * y) = y⁻¹ * exp x * y

Tactic:
exp_units_conj' (Units.mk0 y hy) x

Premises used: NormedSpace.exp_units_conj', Units.mk0
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : NormedCommRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x y : 𝔸
⊢ exp (x + y) = exp x * exp y

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

Premises used: NormedSpace.exp_add_of_mem_ball
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : NormedCommRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Function.onFun Commute f)
⊢ Eq.{u_2 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (∏ i ∈ s, exp (f i))

Tactic:
rw [exp_sum_of_commute, Finset.noncommProd_eq_prod]

Premises used: Finset.noncommProd_eq_prod, NormedSpace.exp_sum_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : NormedCommRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ (↑s : Set ι).Pairwise (Function.onFun Commute f)

Tactic:
fun i _hi j _hj _ => Commute.all _ _

Premises used: Set.Pairwise, Commute.all
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : NormedCommRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ (↑s : Set ι).Pairwise (Function.onFun Commute f)

Tactic:
exact fun i _hi j _hj _ => Commute.all _ _

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

Tactic:
rw [expSeries_apply_eq, expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝕂']

Premises used: inv_natCast_smul_eq, NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
r : ℝ
⊢ (↑(exp r) : ℂ) = exp (↑r : ℂ)

Tactic:
map_exp (algebraMap ℝ ℂ) (continuous_algebraMap _ _) r

Premises used: Real, Algebra.algebraMap, NormedSpace.map_exp, continuous_algebraMap, Complex
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)

Tactic:
have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
⊢ HasDerivAt.{u_1, u_2} (F := A) (fun (k : 𝕜) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) 1 k

Tactic:
simpa using (Algebra.linearMap 𝕜 A).hasDerivAt.sub_const a

Premises used: HasDerivAt.sub_const, Algebra.linearMap, LinearMap.hasDerivAt
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
⊢ HasDerivAt.{u_1, u_2} (F := A) (fun (k : 𝕜) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) 1 k

Tactic:
have H₂ : HasDerivAt (fun k => algebraMap 𝕜 A k - a) 1 k := by
    simpa using (Algebra.linearMap 𝕜 A).hasDerivAt.sub_const a
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
H₂ : HasDerivAt.{u_1, u_2} (F := A) (fun (k : 𝕜) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) 1 k
⊢ HasDerivAt (resolvent a) (-HPow.hPow (β := ℕ) (resolvent a k) 2) k

Tactic:
simpa [resolvent, sq, hk.unit_spec, ← Ring.inverse_unit hk.unit] using H₁.comp_hasDerivAt k H₂

Premises used: HasFDerivAt.comp_hasDerivAt, sq, Ring.inverse_unit, resolvent, IsUnit.unit, IsUnit.unit_spec
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
⊢ HasFDerivAt (fun (a : A) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) (-ContinuousLinearMap.id 𝕜 A)
    a

Tactic:
simpa using (hasFDerivAt_const _ a).sub (hasFDerivAt_id a)

Premises used: HasFDerivAt.sub, hasFDerivAt_id, hasFDerivAt_const
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
⊢ HasFDerivAt (fun (a : A) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) (-ContinuousLinearMap.id 𝕜 A)
    a

Tactic:
have H₂ : HasFDerivAt (fun a => algebraMap 𝕜 A k - a) (- .id 𝕜 A) a := by
    simpa using (hasFDerivAt_const _ a).sub (hasFDerivAt_id a)
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
H₂ :
  HasFDerivAt (fun (a : A) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) (-ContinuousLinearMap.id 𝕜 A)
    a
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ resolvent x k)
    ((((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (resolvent a k) : A →L[𝕜] A →L[𝕜] A) :
        (a : A) → A →L[𝕜] A)
      (resolvent a k))
    a

Tactic:
simpa [resolvent_eq hk] using H₁.comp a H₂

Premises used: spectrum.resolvent_eq, HasFDerivAt.comp