Theorem: Complex.hasDerivAt_exp_real_smul_I (ForML/Trigonometric.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => cexp (x • I)) (I * cexp (x • I)) x
Tactic:
rw [mul_comm I]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => cexp (x • I)) (cexp (x • I) * I) x

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => cexp (x • I)) (cexp (x • I) * I) x
Tactic:
refine HasDerivAt.cexp ?_
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) I x

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) I x
Tactic:
suffices : HasDerivAt (fun x => x • I) ((1 : ℝ) • I) x
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
this : HasDerivAt (fun x => x • I) (1 • I) x
⊢ HasDerivAt (fun x => x • I) I x

case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
this : HasDerivAt (fun x => x • I) (1 • I) x
⊢ HasDerivAt (fun x => x • I) I x

case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x
Tactic:
. simpa using this
State after:
case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x

State before:
case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x
Tactic:
exact HasDerivAt.smul_const (hasDerivAt_id' x) I
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
this : HasDerivAt (fun x => x • I) (1 • I) x
⊢ HasDerivAt (fun x => x • I) I x
Tactic:
simpa using this
State after:
no goals