chore(analysis/normed_space/exponential): Make the 𝔸 argument impli…

…cit (#13986)

`exp 𝕂 𝔸` is now just `exp 𝕂`.

This also renames two lemmas that refer to this argument in their name to no longer do so.

In a few places we have to add type annotations where they weren't needed before, but nowhere do we need to resort to `@`.

src/analysis/normed_space/spectrum.lean

@@ -371,11 +371,11 @@ section exp_mapping
 
 local notation `↑ₐ` := algebra_map 𝕜 A
 
-/-- For `𝕜 = ℝ` or `𝕜 = ℂ`, `exp 𝕜 𝕜` maps the spectrum of `a` into the spectrum of `exp 𝕜 A a`. -/
+/-- For `𝕜 = ℝ` or `𝕜 = ℂ`, `exp 𝕜` maps the spectrum of `a` into the spectrum of `exp 𝕜 a`. -/
 theorem exp_mem_exp [is_R_or_C 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
-  (a : A) {z : 𝕜} (hz : z ∈ spectrum 𝕜 a) : exp 𝕜 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 A a) :=
+  (a : A) {z : 𝕜} (hz : z ∈ spectrum 𝕜 a) : exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a) :=
 begin
-  have hexpmul : exp 𝕜 A a = exp 𝕜 A (a - ↑ₐ z) * ↑ₐ (exp 𝕜 𝕜 z),
+  have hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z),
   { rw [algebra_map_exp_comm z, ←exp_add_of_commute (algebra.commutes z (a - ↑ₐz)).symm,
       sub_add_cancel] },
   let b := ∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐz) ^ n,
@@ -391,13 +391,13 @@ begin
     { simpa only [mul_smul_comm, pow_succ] using hb.tsum_mul_left (a - ↑ₐz) },
   have h₁ : ∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐz) ^ (n + 1) = b * (a - ↑ₐz),
     { simpa only [pow_succ', algebra.smul_mul_assoc] using hb.tsum_mul_right (a - ↑ₐz) },
-  have h₃ : exp 𝕜 A (a - ↑ₐz) = 1 + (a - ↑ₐz) * b,
+  have h₃ : exp 𝕜 (a - ↑ₐz) = 1 + (a - ↑ₐz) * b,
   { rw exp_eq_tsum,
     convert tsum_eq_zero_add (exp_series_summable' (a - ↑ₐz)),
     simp only [nat.factorial_zero, nat.cast_one, inv_one, pow_zero, one_smul],
     exact h₀.symm },
-  rw [spectrum.mem_iff, is_unit.sub_iff, ←one_mul (↑ₐ(exp 𝕜 𝕜 z)), hexpmul, ←_root_.sub_mul,
-    commute.is_unit_mul_iff (algebra.commutes (exp 𝕜 𝕜 z) (exp 𝕜 A (a - ↑ₐz) - 1)).symm,
+  rw [spectrum.mem_iff, is_unit.sub_iff, ←one_mul (↑ₐ(exp 𝕜 z)), hexpmul, ←_root_.sub_mul,
+    commute.is_unit_mul_iff (algebra.commutes (exp 𝕜 z) (exp 𝕜 (a - ↑ₐz) - 1)).symm,
     sub_eq_iff_eq_add'.mpr h₃, commute.is_unit_mul_iff (h₀ ▸ h₁ : (a - ↑ₐz) * b = b * (a - ↑ₐz))],
   exact not_and_of_not_left _ (not_and_of_not_left _ ((not_iff_not.mpr is_unit.sub_iff).mp hz)),
 end

src/analysis/normed_space/star/exponential.lean

@@ -29,20 +29,20 @@ variables {A : Type*}
 open complex
 
 lemma self_adjoint.exp_i_smul_unitary {a : A} (ha : a ∈ self_adjoint A) :
-  exp ℂ A (I • a) ∈ unitary A :=
+  exp ℂ (I • a) ∈ unitary A :=
 begin
   rw [unitary.mem_iff, star_exp],
   simp only [star_smul, is_R_or_C.star_def, self_adjoint.mem_iff.mp ha, conj_I, neg_smul],
   rw ←@exp_add_of_commute ℂ A _ _ _ _ _ _ ((commute.refl (I • a)).neg_left),
   rw ←@exp_add_of_commute ℂ A _ _ _ _ _ _ ((commute.refl (I • a)).neg_right),
-  simpa only [add_right_neg, add_left_neg, and_self] using (exp_zero : exp ℂ A 0 = 1),
+  simpa only [add_right_neg, add_left_neg, and_self] using (exp_zero : exp ℂ (0 : A) = 1),
 end
 
 /-- The map from the selfadjoint real subspace to the unitary group. This map only makes sense
 over ℂ. -/
 @[simps]
 noncomputable def self_adjoint.exp_unitary (a : self_adjoint A) : unitary A :=
-⟨exp ℂ A (I • a), self_adjoint.exp_i_smul_unitary (a.property)⟩
+⟨exp ℂ (I • a), self_adjoint.exp_i_smul_unitary (a.property)⟩
 
 open self_adjoint
 

src/analysis/normed_space/star/spectrum.lean

@@ -88,11 +88,11 @@ theorem self_adjoint.mem_spectrum_eq_re [star_module ℂ A] [nontrivial A] {a :
   (ha : a ∈ self_adjoint A) {z : ℂ} (hz : z ∈ spectrum ℂ a) : z = z.re :=
 begin
   let Iu := units.mk0 I I_ne_zero,
-  have : exp ℂ ℂ (I • z) ∈ spectrum ℂ (exp ℂ A (I • a)),
+  have : exp ℂ (I • z) ∈ spectrum ℂ (exp ℂ (I • a)),
     by simpa only [units.smul_def, units.coe_mk0]
       using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz),
   exact complex.ext (of_real_re _)
-    (by simpa only [←complex.exp_eq_exp_ℂ_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp,
+    (by simpa only [←complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp,
       real.exp_eq_one_iff, smul_eq_mul, I_mul, neg_eq_zero]
       using spectrum.subset_circle_of_unitary (self_adjoint.exp_i_smul_unitary ha) this),
 end

src/analysis/special_functions/exponential.lean

@@ -11,7 +11,7 @@ import topology.metric_space.cau_seq_filter
 /-!
 # Calculus results on exponential in a Banach algebra
 
-In this file, we prove basic properties about the derivative of the exponential map `exp 𝕂 𝔸`
+In this file, we prove basic properties about the derivative of the exponential map `exp 𝕂`
 in a Banach algebra `𝔸` over a field `𝕂`. We keep them separate from the main file
 `analysis/normed_space/exponential` in order to minimize dependencies.
 
@@ -21,26 +21,26 @@ We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂
 
 ### General case
 
-- `has_strict_fderiv_at_exp_zero_of_radius_pos` : `exp 𝕂 𝔸` has strict Fréchet-derivative
+- `has_strict_fderiv_at_exp_zero_of_radius_pos` : `exp 𝕂` has strict Fréchet-derivative
   `1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero
   (see also `has_strict_deriv_at_exp_zero_of_radius_pos` for the case `𝔸 = 𝕂`)
 - `has_strict_fderiv_at_exp_of_lt_radius` : if `𝕂` has characteristic zero and `𝔸` is commutative,
-  then given a point `x` in the disk of convergence, `exp 𝕂 𝔸` as strict Fréchet-derivative
-  `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp_of_lt_radius` for the case
+  then given a point `x` in the disk of convergence, `exp 𝕂` as strict Fréchet-derivative
+  `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp_of_lt_radius` for the case
   `𝔸 = 𝕂`)
 
 ### `𝕂 = ℝ` or `𝕂 = ℂ`
 
-- `has_strict_fderiv_at_exp_zero` : `exp 𝕂 𝔸` has strict Fréchet-derivative `1 : 𝔸 →L[𝕂] 𝔸` at zero
+- `has_strict_fderiv_at_exp_zero` : `exp 𝕂` has strict Fréchet-derivative `1 : 𝔸 →L[𝕂] 𝔸` at zero
   (see also `has_strict_deriv_at_exp_zero` for the case `𝔸 = 𝕂`)
-- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂 𝔸` as strict
-  Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp` for the
+- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂` as strict
+  Fréchet-derivative `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp` for the
   case `𝔸 = 𝕂`)
 
 ### Compatibilty with `real.exp` and `complex.exp`
 
-- `complex.exp_eq_exp_ℂ_ℂ` : `complex.exp = exp ℂ ℂ`
-- `real.exp_eq_exp_ℝ_ℝ` : `real.exp = exp ℝ ℝ`
+- `complex.exp_eq_exp_ℂ` : `complex.exp = exp ℂ ℂ`
+- `real.exp_eq_exp_ℝ` : `real.exp = exp ℝ ℝ`
 
 -/
 
@@ -55,7 +55,7 @@ variables {𝕂 𝔸 : Type*} [nondiscrete_normed_field 𝕂] [normed_ring 𝔸]
 /-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has strict Fréchet-derivative
 `1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/
 lemma has_strict_fderiv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
+  has_strict_fderiv_at (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
 begin
   convert (has_fpower_series_at_exp_zero_of_radius_pos h).has_strict_fderiv_at,
   ext x,
@@ -66,7 +66,7 @@ end
 /-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has Fréchet-derivative
 `1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/
 lemma has_fderiv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
-  has_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
+  has_fderiv_at (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
 (has_strict_fderiv_at_exp_zero_of_radius_pos h).has_fderiv_at
 
 end any_field_any_algebra
@@ -77,16 +77,16 @@ variables {𝕂 𝔸 : Type*} [nondiscrete_normed_field 𝕂] [normed_comm_ring
   [complete_space 𝔸]
 
 /-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of
-characteristic zero has Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x` in the
+characteristic zero has Fréchet-derivative `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x` in the
 disk of convergence. -/
 lemma has_fderiv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  has_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
+  has_fderiv_at (exp 𝕂) (exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
 begin
   have hpos : 0 < (exp_series 𝕂 𝔸).radius := (zero_le _).trans_lt hx,
   rw has_fderiv_at_iff_is_o_nhds_zero,
-  suffices : (λ h, exp 𝕂 𝔸 x * (exp 𝕂 𝔸 (0 + h) - exp 𝕂 𝔸 0 - continuous_linear_map.id 𝕂 𝔸 h))
-    =ᶠ[𝓝 0] (λ h, exp 𝕂 𝔸 (x + h) - exp 𝕂 𝔸 x - exp 𝕂 𝔸 x • continuous_linear_map.id 𝕂 𝔸 h),
+  suffices : (λ h, exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - continuous_linear_map.id 𝕂 𝔸 h))
+    =ᶠ[𝓝 0] (λ h, exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • continuous_linear_map.id 𝕂 𝔸 h),
   { refine (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _),
     rw ← has_fderiv_at_iff_is_o_nhds_zero,
     exact has_fderiv_at_exp_zero_of_radius_pos hpos },
@@ -98,11 +98,11 @@ begin
 end
 
 /-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of
-characteristic zero has strict Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x` in
+characteristic zero has strict Fréchet-derivative `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x` in
 the disk of convergence. -/
 lemma has_strict_fderiv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
+  has_strict_fderiv_at (exp 𝕂) (exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
 let ⟨p, hp⟩ := analytic_at_exp_of_mem_ball x hx in
 hp.has_fderiv_at.unique (has_fderiv_at_exp_of_mem_ball hx) ▸ hp.has_strict_fderiv_at
 
@@ -113,29 +113,29 @@ section deriv
 variables {𝕂 : Type*} [nondiscrete_normed_field 𝕂] [complete_space 𝕂]
 
 /-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
-`exp 𝕂 𝕂 x` at any point `x` in the disk of convergence. -/
+`exp 𝕂 x` at any point `x` in the disk of convergence. -/
 lemma has_strict_deriv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝕂}
   (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
-  has_strict_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
+  has_strict_deriv_at (exp 𝕂) (exp 𝕂 x) x :=
 by simpa using (has_strict_fderiv_at_exp_of_mem_ball hx).has_strict_deriv_at
 
 /-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
-`exp 𝕂 𝕂 x` at any point `x` in the disk of convergence. -/
+`exp 𝕂 x` at any point `x` in the disk of convergence. -/
 lemma has_deriv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝕂}
   (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
-  has_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
+  has_deriv_at (exp 𝕂) (exp 𝕂 x) x :=
 (has_strict_deriv_at_exp_of_mem_ball hx).has_deriv_at
 
 /-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
 `1` at zero, as long as it converges on a neighborhood of zero. -/
 lemma has_strict_deriv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝕂).radius) :
-  has_strict_deriv_at (exp 𝕂 𝕂) 1 0 :=
+  has_strict_deriv_at (exp 𝕂) (1 : 𝕂) 0 :=
 (has_strict_fderiv_at_exp_zero_of_radius_pos h).has_strict_deriv_at
 
 /-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
 `1` at zero, as long as it converges on a neighborhood of zero. -/
 lemma has_deriv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝕂).radius) :
-  has_deriv_at (exp 𝕂 𝕂) 1 0 :=
+  has_deriv_at (exp 𝕂) (1 : 𝕂) 0 :=
 (has_strict_deriv_at_exp_zero_of_radius_pos h).has_deriv_at
 
 end deriv
@@ -148,13 +148,13 @@ variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebr
 /-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict Fréchet-derivative
 `1 : 𝔸 →L[𝕂] 𝔸` at zero. -/
 lemma has_strict_fderiv_at_exp_zero :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
+  has_strict_fderiv_at (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
 has_strict_fderiv_at_exp_zero_of_radius_pos (exp_series_radius_pos 𝕂 𝔸)
 
 /-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has Fréchet-derivative
 `1 : 𝔸 →L[𝕂] 𝔸` at zero. -/
 lemma has_fderiv_at_exp_zero :
-  has_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
+  has_fderiv_at (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
 has_strict_fderiv_at_exp_zero.has_fderiv_at
 
 end is_R_or_C_any_algebra
@@ -165,15 +165,15 @@ variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_comm_ring 𝔸] [normed_a
   [complete_space 𝔸]
 
 /-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict
-Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
+Fréchet-derivative `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
 lemma has_strict_fderiv_at_exp {x : 𝔸} :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
+  has_strict_fderiv_at (exp 𝕂) (exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
 has_strict_fderiv_at_exp_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 /-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has
-Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
+Fréchet-derivative `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
 lemma has_fderiv_at_exp {x : 𝔸} :
-  has_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
+  has_fderiv_at (exp 𝕂) (exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
 has_strict_fderiv_at_exp.has_fderiv_at
 
 end is_R_or_C_comm_algebra
@@ -182,29 +182,29 @@ section deriv_R_or_C
 
 variables {𝕂 : Type*} [is_R_or_C 𝕂]
 
-/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `exp 𝕂 𝕂 x` at any point
+/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `exp 𝕂 x` at any point
 `x`. -/
-lemma has_strict_deriv_at_exp {x : 𝕂} : has_strict_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
+lemma has_strict_deriv_at_exp {x : 𝕂} : has_strict_deriv_at (exp 𝕂) (exp 𝕂 x) x :=
 has_strict_deriv_at_exp_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _)
 
-/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `exp 𝕂 𝕂 x` at any point `x`. -/
-lemma has_deriv_at_exp {x : 𝕂} : has_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
+/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `exp 𝕂 x` at any point `x`. -/
+lemma has_deriv_at_exp {x : 𝕂} : has_deriv_at (exp 𝕂) (exp 𝕂 x) x :=
 has_strict_deriv_at_exp.has_deriv_at
 
 /-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `1` at zero. -/
-lemma has_strict_deriv_at_exp_zero : has_strict_deriv_at (exp 𝕂 𝕂) 1 0 :=
+lemma has_strict_deriv_at_exp_zero : has_strict_deriv_at (exp 𝕂) (1 : 𝕂) 0 :=
 has_strict_deriv_at_exp_zero_of_radius_pos (exp_series_radius_pos 𝕂 𝕂)
 
 /-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `1` at zero. -/
 lemma has_deriv_at_exp_zero :
-  has_deriv_at (exp 𝕂 𝕂) 1 0 :=
+  has_deriv_at (exp 𝕂) (1 : 𝕂) 0 :=
 has_strict_deriv_at_exp_zero.has_deriv_at
 
 end deriv_R_or_C
 
 section complex
 
-lemma complex.exp_eq_exp_ℂ_ℂ : complex.exp = exp ℂ ℂ :=
+lemma complex.exp_eq_exp_ℂ : complex.exp = exp ℂ :=
 begin
   refine funext (λ x, _),
   rw [complex.exp, exp_eq_tsum_field],
@@ -216,10 +216,10 @@ end complex
 
 section real
 
-lemma real.exp_eq_exp_ℝ_ℝ : real.exp = exp ℝ ℝ :=
+lemma real.exp_eq_exp_ℝ : real.exp = exp ℝ :=
 begin
   refine funext (λ x, _),
-  rw [real.exp, complex.exp_eq_exp_ℂ_ℂ, ← exp_ℝ_ℂ_eq_exp_ℂ_ℂ, exp_eq_tsum, exp_eq_tsum_field,
+  rw [real.exp, complex.exp_eq_exp_ℂ, ← exp_ℝ_ℂ_eq_exp_ℂ_ℂ, exp_eq_tsum, exp_eq_tsum_field,
       ← re_to_complex, ← re_clm_apply, re_clm.map_tsum (exp_series_summable' (x : ℂ))],
   refine tsum_congr (λ n, _),
   rw [re_clm.map_smul, ← complex.of_real_pow, re_clm_apply, re_to_complex, complex.of_real_re,

src/combinatorics/derangements/exponential.lean

@@ -34,7 +34,7 @@ begin
     apply has_sum.tendsto_sum_nat,
     -- there's no specific lemma for ℝ that ∑ x^k/k! sums to exp(x), but it's
     -- true in more general fields, so use that lemma
-    rw real.exp_eq_exp_ℝ_ℝ,
+    rw real.exp_eq_exp_ℝ,
     exact exp_series_field_has_sum_exp (-1 : ℝ) },
   intro n,
   rw [← int.cast_coe_nat, num_derangements_sum],