[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (↑1 / cos x ^ 2) x
[PROOFSTEP]
exact_mod_cast (Complex.hasStrictDerivAt_tan (by exact_mod_cast h)).real_of_complex
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt tan (↑1 / cos x ^ 2) x
[PROOFSTEP]
exact_mod_cast (Complex.hasDerivAt_tan (by exact_mod_cast h)).real_of_complex
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x : ℝ
hx : cos x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
have hx : Complex.cos x = 0 := by exact_mod_cast hx
[GOAL]
x : ℝ
hx : cos x = 0
⊢ Complex.cos ↑x = 0
[PROOFSTEP]
exact_mod_cast hx
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
simp only [← Complex.abs_ofReal, Complex.ofReal_tan]
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑Complex.abs (Complex.tan ↑x)) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
refine' (Complex.tendsto_abs_tan_of_cos_eq_zero hx).comp _
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓝[{x}ᶜ] x) (𝓝[{↑x}ᶜ] ↑x)
[PROOFSTEP]
refine' Tendsto.inf Complex.continuous_ofReal.continuousAt _
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓟 {x}ᶜ) (𝓟 {↑x}ᶜ)
[PROOFSTEP]
exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1
[GOAL]
x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0
[PROOFSTEP]
refine' ⟨fun hc h₀ => _, fun h => (hasDerivAt_tan h).continuousAt⟩
[GOAL]
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
[PROOFSTEP]
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _ (hc.norm.tendsto.mono_left inf_le_left)
[GOAL]
x : ℝ
h : cos x = 0
⊢ deriv tan x = ↑1 / cos x ^ 2
[PROOFSTEP]
have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
[GOAL]
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = ↑1 / cos x ^ 2
[PROOFSTEP]
simp [deriv_zero_of_not_differentiableAt this, h, sq]
[GOAL]
n : ℕ∞
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x : ℝ
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
[PROOFSTEP]
have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
[GOAL]
x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
[PROOFSTEP]
simpa [cos_sq_arctan] using tanLocalHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)
[GOAL]
x : ℝ
A : cos (arctan x) ≠ 0
⊢ ↑1 / cos (↑(LocalHomeomorph.symm tanLocalHomeomorph) x) ^ 2 ≠ 0
[PROOFSTEP]
simpa
[GOAL]
n : ℕ∞
x : ℝ
this : cos (arctan x) ≠ 0
⊢ ↑1 / cos (↑(LocalHomeomorph.symm tanLocalHomeomorph) x) ^ 2 ≠ 0
[PROOFSTEP]
simpa


[GOAL]
⊢ ∀ ⦃x : ℂ⦄, x ∈ {z | z.im ∈ Ioo (-π) π} → exp x ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨h₁ : -π < y, h₂ : y < π⟩
[GOAL]
case mk.intro
x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ exp { re := x, im := y } ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
[PROOFSTEP]
refine' (not_or_of_imp fun hz => _).symm
[GOAL]
case mk.intro
x y : ℝ
h₁ : -π < y
h₂ : y < π
hz : (exp { re := x, im := y }).im = 0
⊢ exp { re := x, im := y } ∈ {z | 0 < z.re}
[PROOFSTEP]
obtain rfl : y = 0 := by
  rw [exp_im] at hz
  simpa [(Real.exp_pos _).ne', Real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz
[GOAL]
x y : ℝ
h₁ : -π < y
h₂ : y < π
hz : (exp { re := x, im := y }).im = 0
⊢ y = 0
[PROOFSTEP]
rw [exp_im] at hz
[GOAL]
x y : ℝ
h₁ : -π < y
h₂ : y < π
hz : Real.exp { re := x, im := y }.re * Real.sin { re := x, im := y }.im = 0
⊢ y = 0
[PROOFSTEP]
simpa [(Real.exp_pos _).ne', Real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz
[GOAL]
case mk.intro
x : ℝ
h₁ : -π < 0
h₂ : 0 < π
hz : (exp { re := x, im := 0 }).im = 0
⊢ exp { re := x, im := 0 } ∈ {z | 0 < z.re}
[PROOFSTEP]
rw [mem_setOf_eq, ← ofReal_def, exp_ofReal_re]
[GOAL]
case mk.intro
x : ℝ
h₁ : -π < 0
h₂ : 0 < π
hz : (exp { re := x, im := 0 }).im = 0
⊢ 0 < Real.exp x
[PROOFSTEP]
exact Real.exp_pos x
[GOAL]
z : ℂ
h : z ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ log z ∈ {z | z.im ∈ Ioo (-π) π}
[PROOFSTEP]
simp only [mem_setOf, log_im, mem_Ioo, neg_pi_lt_arg, arg_lt_pi_iff, true_and]
[GOAL]
z : ℂ
h : z ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ 0 ≤ z.re ∨ z.im ≠ 0
[PROOFSTEP]
exact h.imp_left le_of_lt
[GOAL]
x : ℂ
hx : x ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
hx : 0 ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ False
[PROOFSTEP]
simp [lt_irrefl] at hx
[GOAL]
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp [lt_irrefl] at h
[GOAL]
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expLocalHomeomorph) x (↑(LocalHomeomorph.symm expLocalHomeomorph) x)
[PROOFSTEP]
simpa [exp_log h0] using hasStrictDerivAt_exp (log x)
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
[PROOFSTEP]
exact (hasStrictDerivAt_log h₂).comp x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).comp_hasStrictDerivAt x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
[PROOFSTEP]
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivAt x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) ((f x)⁻¹ * f') s x
[PROOFSTEP]
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp_hasDerivWithinAt x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
s : Set ℝ
x : ℝ
f' : ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
[PROOFSTEP]
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivWithinAt x h₁


[GOAL]
x : ℂ
⊢ (log x).re = Real.log (↑abs x)
[PROOFSTEP]
simp [log]
[GOAL]
x : ℂ
⊢ (log x).im = arg x
[PROOFSTEP]
simp [log]
[GOAL]
x : ℂ
⊢ -π < (log x).im
[PROOFSTEP]
simp only [log_im, neg_pi_lt_arg]
[GOAL]
x : ℂ
⊢ (log x).im ≤ π
[PROOFSTEP]
simp only [log_im, arg_le_pi]
[GOAL]
x : ℂ
hx : x ≠ 0
⊢ exp (log x) = x
[PROOFSTEP]
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp, Real.exp_log (abs.pos hx),
  mul_add, ofReal_div, ofReal_div, mul_div_cancel' _ (ofReal_ne_zero.2 <| abs.ne_zero hx), ← mul_assoc,
  mul_div_cancel' _ (ofReal_ne_zero.2 <| abs.ne_zero hx), re_add_im]
[GOAL]
x : ℂ
⊢ x ∈ Set.range exp → x ∈ {0}ᶜ
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case intro
x : ℂ
⊢ exp x ∈ {0}ᶜ
[PROOFSTEP]
exact exp_ne_zero x
[GOAL]
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (exp x) = x
[PROOFSTEP]
rw [log, abs_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
  arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
[GOAL]
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : exp x = exp y
⊢ x = y
[PROOFSTEP]
rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]
[GOAL]
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = (log ↑x).re
[PROOFSTEP]
rw [log_re, ofReal_re, abs_of_nonneg hx]
[GOAL]
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).im = (log ↑x).im
[PROOFSTEP]
rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]
[GOAL]
x : ℝ
⊢ (log ↑x).re = Real.log x
[PROOFSTEP]
simp [log_re]
[GOAL]
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
[PROOFSTEP]
replace hx := Complex.abs.ne_zero_iff.mpr hx
[GOAL]
r : ℝ
hr : 0 < r
x : ℂ
hx : ↑abs x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
[PROOFSTEP]
simp_rw [log, map_mul, abs_ofReal, arg_real_mul _ hr, abs_of_pos hr, Real.log_mul hr.ne' hx, ofReal_add, add_assoc]
[GOAL]
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (x * ↑r) = ↑(Real.log r) + log x
[PROOFSTEP]
rw [mul_comm, log_ofReal_mul hr hx, add_comm]
[GOAL]
⊢ log 0 = 0
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log 1 = 0
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log (-1) = ↑π * I
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log I = ↑π / 2 * I
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log (-I) = -(↑π / 2) * I
[PROOFSTEP]
simp [log]
[GOAL]
x : ℂ
⊢ log (↑(starRingEnd ℂ) x) = if arg x = π then log x else ↑(starRingEnd ℂ) (log x)
[PROOFSTEP]
simp_rw [log, abs_conj, arg_conj, map_add, map_mul, conj_ofReal]
[GOAL]
x : ℂ
⊢ ↑(Real.log (↑abs x)) + ↑(if arg x = π then π else -arg x) * I =
    if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
x : ℂ
hx : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑π * I = ↑(Real.log (↑abs x)) + ↑(arg x) * I
[PROOFSTEP]
rw [hx]
[GOAL]
case neg
x : ℂ
hx : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(-arg x) * I = ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
[PROOFSTEP]
simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]
[GOAL]
x : ℂ
h : arg x ≠ π
⊢ log (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (log x)
[PROOFSTEP]
rw [log_conj_eq_ite, if_neg h]
[GOAL]
x : ℂ
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x : ℂ
hx : x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) - ↑(Real.log (↑normSq x)) =
    if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_abs, Real.log_pow, Nat.cast_two, ofReal_mul, neg_add,
  mul_neg, neg_neg]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      ↑2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
norm_num
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
rw [two_mul]
  -- Porting note: added to simplify `↑2`
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℂ
hx : ¬x = 0
h✝ : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(arg x) * I - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + ↑(arg x) * I
[PROOFSTEP]
rw [add_sub_right_comm, sub_add_cancel']
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
h✝ : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + -(↑(arg x) * I) - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
rw [add_sub_right_comm, sub_add_cancel']
[GOAL]
case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (↑normSq x)⁻¹
[PROOFSTEP]
rwa [inv_pos, Complex.normSq_pos]
[GOAL]
case neg.hx
x : ℂ
hx : ¬x = 0
⊢ ↑(starRingEnd ℂ) x ≠ 0
[PROOFSTEP]
rwa [map_ne_zero]
[GOAL]
x : ℂ
hx : arg x ≠ π
⊢ log x⁻¹ = -log x
[PROOFSTEP]
rw [log_inv_eq_ite, if_neg hx]
[GOAL]
⊢ 2 * ↑π * I ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
⊢ ¬(π = 0 ∨ I = 0)
[PROOFSTEP]
simp [Real.pi_ne_zero, I_ne_zero]
[GOAL]
x : ℂ
⊢ exp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
constructor
[GOAL]
case mp
x : ℂ
⊢ exp x = 1 → ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
intro h
[GOAL]
case mp
x : ℂ
h : exp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩
[GOAL]
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
use-n
[GOAL]
case h
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)
[PROOFSTEP]
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]
[GOAL]
case h
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0
[PROOFSTEP]
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn
[GOAL]
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
[PROOFSTEP]
simpa [two_mul, mul_add] using hn
[GOAL]
case h
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0
[PROOFSTEP]
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
[GOAL]
case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → exp x = 1
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mpr.intro
n : ℤ
⊢ exp (↑n * (2 * ↑π * I)) = 1
[PROOFSTEP]
exact (exp_periodic.int_mul n).eq.trans exp_zero
[GOAL]
x y : ℂ
⊢ exp x = exp y ↔ exp (x - y) = 1
[PROOFSTEP]
rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
[GOAL]
x y : ℂ
⊢ exp x = exp y ↔ ∃ n, x = y + ↑n * (2 * ↑π * I)
[PROOFSTEP]
simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']
[GOAL]
s : Set ℂ
⊢ Set.Countable (exp ⁻¹' s) ↔ Set.Countable s
[PROOFSTEP]
refine' ⟨fun hs => _, fun hs => _⟩
[GOAL]
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ Set.Countable s
[PROOFSTEP]
refine' ((hs.image exp).insert 0).mono _
[GOAL]
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ insert 0 (exp '' (exp ⁻¹' s))
[PROOFSTEP]
rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.diff_eq, ← Set.union_singleton, Set.diff_union_self]
[GOAL]
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ s ∪ {0}
[PROOFSTEP]
exact Set.subset_union_left _ _
[GOAL]
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (exp ⁻¹' s)
[PROOFSTEP]
rw [← Set.biUnion_preimage_singleton]
[GOAL]
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (⋃ (y : ℂ) (_ : y ∈ s), exp ⁻¹' {y})
[PROOFSTEP]
refine' hs.biUnion fun z hz => _
[GOAL]
case refine'_2
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
⊢ Set.Countable (exp ⁻¹' {z})
[PROOFSTEP]
rcases em (∃ w, exp w = z) with (⟨w, rfl⟩ | hne)
[GOAL]
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (exp ⁻¹' {exp w})
[PROOFSTEP]
simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]
[GOAL]
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (⋃ (i : ℤ), {x | x = w + ↑i * (2 * ↑π * I)})
[PROOFSTEP]
exact Set.countable_iUnion fun m => Set.countable_singleton _
[GOAL]
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ¬∃ w, exp w = z
⊢ Set.Countable (exp ⁻¹' {z})
[PROOFSTEP]
push_neg at hne
[GOAL]
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ∀ (w : ℂ), exp w ≠ z
⊢ Set.Countable (exp ⁻¹' {z})
[PROOFSTEP]
simp [Set.preimage, hne]
[GOAL]
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log (↑abs z)) - ↑π * I))
[PROOFSTEP]
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt (continuous_abs.continuousWithinAt.log _)).tendsto.add
    (((continuous_ofReal.tendsto _).comp <| tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using
  1
[GOAL]
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log (↑abs z)) - ↑π * I) = 𝓝 ((ofReal' ∘ fun x => Real.log (↑abs x)) z + ↑(-π) * I)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
[PROOFSTEP]
lift z to ℝ using him
[GOAL]
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
[PROOFSTEP]
simpa using hre.ne
[GOAL]
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z | 0 ≤ z.im} z
[PROOFSTEP]
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt (continuous_abs.continuousWithinAt.log _)).tendsto.add
    ((continuous_ofReal.continuousAt.comp_continuousWithinAt <| continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using
  1
[GOAL]
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
[PROOFSTEP]
lift z to ℝ using him
[GOAL]
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
[PROOFSTEP]
simpa using hre.ne
[GOAL]
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log (↑abs z)) + ↑π * I))
[PROOFSTEP]
simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto
[GOAL]
⊢ map exp (comap re atBot) = 𝓝[{0}ᶜ] 0
[PROOFSTEP]
rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
[GOAL]
⊢ map exp (comap re atTop) = comap (↑abs) atTop
[PROOFSTEP]
rw [← comap_exp_comap_abs_atTop, map_comap, range_exp, inf_eq_left, le_principal_iff]
[GOAL]
⊢ {0}ᶜ ∈ comap (↑abs) atTop
[PROOFSTEP]
exact eventually_ne_of_tendsto_norm_atTop tendsto_comap 0
[GOAL]
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt log x
[PROOFSTEP]
refine' ContinuousAt.add _ _
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (fun x => ↑(Real.log (↑Complex.abs x))) x
[PROOFSTEP]
refine' continuous_ofReal.continuousAt.comp _
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (fun x => Real.log (↑Complex.abs x)) x
[PROOFSTEP]
refine' (Real.continuousAt_log _).comp Complex.continuous_abs.continuousAt
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ↑Complex.abs x ≠ 0
[PROOFSTEP]
rw [Complex.abs.ne_zero_iff]
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
α : Type u_1
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
case refine'_2
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (fun x => ↑(arg x) * I) x
[PROOFSTEP]
have h_cont_mul : Continuous fun x : ℂ => x * I := continuous_id'.mul continuous_const
[GOAL]
case refine'_2
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt (fun x => ↑(arg x) * I) x
[PROOFSTEP]
refine' h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp _)
[GOAL]
case refine'_2
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt (fun x => arg x) x
[PROOFSTEP]
exact continuousAt_arg h


[GOAL]
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div, Complex.ofReal_mul,
  Complex.ofReal_tan] using @Complex.tan_add (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)
[GOAL]
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ ((∀ (k : ℤ), ↑x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑y = (2 * ↑l + 1) * ↑π / 2
[PROOFSTEP]
convert h
[GOAL]
case h.e'_1.h.e'_1.h.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
a✝ : ℤ
⊢ ↑x = (2 * ↑a✝ + 1) * ↑π / 2 ↔ x = (2 * ↑a✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_1.h.e'_2.h.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
a✝ : ℤ
⊢ ↑y = (2 * ↑a✝ + 1) * ↑π / 2 ↔ y = (2 * ↑a✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_2.h.e'_1.h.e'_2.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
x✝ : ℤ
⊢ ↑x = (2 * ↑x✝ + 1) * ↑π / 2 ↔ x = (2 * ↑x✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_2.h.e'_2.h.e'_2.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
x✝ : ℤ
⊢ ↑y = (2 * ↑x✝ + 1) * ↑π / 2 ↔ y = (2 * ↑x✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
x : ℝ
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
[PROOFSTEP]
have := @Complex.tan_two_mul x
[GOAL]
x : ℝ
this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
[PROOFSTEP]
norm_cast at *
[GOAL]
θ : ℝ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * π / 2
[PROOFSTEP]
rw [← Complex.ofReal_ne_zero, Complex.ofReal_tan, Complex.tan_ne_zero_iff]
[GOAL]
θ : ℝ
⊢ (∀ (k : ℤ), ↑θ ≠ ↑k * ↑π / 2) ↔ ∀ (k : ℤ), θ ≠ ↑k * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
θ : ℝ
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * π / 2
[PROOFSTEP]
rw [← not_iff_not, not_exists, ← Ne, tan_ne_zero_iff]
[GOAL]
n : ℤ
⊢ ∃ k, ↑n * π / 2 = ↑k * π / 2
[PROOFSTEP]
use n
[GOAL]
⊢ ContinuousOn tan {x | cos x ≠ 0}
[PROOFSTEP]
suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
  by
  have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
  rwa [h_eq] at this
[GOAL]
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ ContinuousOn tan {x | cos x ≠ 0}
[PROOFSTEP]
have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
[GOAL]
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ (fun x => sin x / cos x) = tan
[PROOFSTEP]
ext1 x
[GOAL]
case h
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
[PROOFSTEP]
rw [tan_eq_sin_div_cos]
[GOAL]
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
h_eq : (fun x => sin x / cos x) = tan
⊢ ContinuousOn tan {x | cos x ≠ 0}
[PROOFSTEP]
rwa [h_eq] at this
[GOAL]
⊢ ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
[PROOFSTEP]
exact continuousOn_sin.div continuousOn_cos fun x => id
[GOAL]
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))
[PROOFSTEP]
refine' ContinuousOn.mono continuousOn_tan fun x => _
[GOAL]
x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}
[PROOFSTEP]
simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne.def]
[GOAL]
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0
[PROOFSTEP]
rw [cos_eq_zero_iff]
[GOAL]
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2
[PROOFSTEP]
rintro hx_gt hx_lt ⟨r, hxr_eq⟩
[GOAL]
case intro
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False
[PROOFSTEP]
cases' le_or_lt 0 r with h h
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
[PROOFSTEP]
rw [lt_iff_not_ge] at hx_lt
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
[PROOFSTEP]
refine' hx_lt _
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ x ≥ π / 2
[PROOFSTEP]
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, mul_le_mul_right (half_pos pi_pos)]
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 ≤ 2 * ↑r + 1
[PROOFSTEP]
simp [h]
[GOAL]
case intro.inr
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
[PROOFSTEP]
rw [lt_iff_not_ge] at hx_gt
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
[PROOFSTEP]
refine' hx_gt _
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ -(π / 2) ≥ x
[PROOFSTEP]
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, neg_mul_eq_neg_mul, mul_le_mul_right (half_pos pi_pos)]
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ 2 * ↑r + 1 ≤ -1
[PROOFSTEP]
have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
[GOAL]
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ r ≤ -1
[PROOFSTEP]
rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 2 * ↑r + 1 ≤ -1
[PROOFSTEP]
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff]
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ (-1 - 1) / 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ -1
[PROOFSTEP]
rw [← Int.cast_one, ← Int.cast_neg]
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ ↑(-1)
[PROOFSTEP]
norm_cast
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atBot atBot
[PROOFSTEP]
rw [tendsto_comp_coe_Ioo_atBot this]
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Ioi (-(π / 2))] (-(π / 2))) atBot
[PROOFSTEP]
exact tendsto_tan_neg_pi_div_two
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atTop atTop
[PROOFSTEP]
rw [tendsto_comp_coe_Ioo_atTop this]
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Iio (π / 2)] (π / 2)) atTop
[PROOFSTEP]
exact tendsto_tan_pi_div_two
[GOAL]
x : ℝ
⊢ cos (arctan x) ^ 2 = ↑1 / (↑1 + x ^ 2)
[PROOFSTEP]
rw_mod_cast [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
[GOAL]
x : ℝ
⊢ sin (arctan x) = x / sqrt (↑1 + x ^ 2)
[PROOFSTEP]
rw_mod_cast [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
[GOAL]
x : ℝ
⊢ cos (arctan x) = ↑1 / sqrt (↑1 + x ^ 2)
[PROOFSTEP]
rw_mod_cast [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
[GOAL]
x : ℝ
h : x ∈ Ioo (-1) 1
⊢ arcsin x = arctan (x / sqrt (↑1 - x ^ 2))
[PROOFSTEP]
rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul, mul_div_cancel', sub_add_cancel,
  sqrt_one, div_one]
[GOAL]
case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
simp at h
[GOAL]
case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
simp at h
[GOAL]
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
simp at h
[GOAL]
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
simp at h
[GOAL]
case hb
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
case hx
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
⊢ arctan 0 = 0
[PROOFSTEP]
simp [arctan_eq_arcsin]
[GOAL]
x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ tan (arctan y) = tan x
[PROOFSTEP]
rw [tan_arctan, h]
[GOAL]
⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ -(π / 2) < π / 4
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case right
⊢ π / 4 < π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x : ℝ
⊢ arctan (-x) = -arctan x
[PROOFSTEP]
simp [arctan_eq_arcsin, neg_div]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (sqrt (↑1 + x ^ 2))⁻¹
[PROOFSTEP]
rw [arctan_eq_arcsin, arccos_eq_arcsin]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))
x : ℝ h : 0 ≤ x ⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
[PROOFSTEP]
swap
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
[PROOFSTEP]
exact inv_nonneg.2 (sqrt_nonneg _)
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
x : ℝ
h : 0 ≤ x
⊢ x / sqrt (↑1 + x ^ 2) = sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2)
[PROOFSTEP]
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel', sqrt_div, sqrt_sq h]
[GOAL]
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2
case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0
case e_a x : ℝ h : 0 ≤ x ⊢ 0 ≤ (1 + x ^ 2)⁻¹
[PROOFSTEP]
all_goals positivity
[GOAL]
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2
[PROOFSTEP]
positivity
[GOAL]
case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹
[PROOFSTEP]
positivity
[GOAL]
x : ℝ
h : 0 < x
⊢ arccos x = arctan (sqrt (↑1 - x ^ 2) / x)
[PROOFSTEP]
rw [arccos, eq_comm]
[GOAL]
x : ℝ
h : 0 < x
⊢ arctan (sqrt (↑1 - x ^ 2) / x) = π / 2 - arcsin x
[PROOFSTEP]
refine' arctan_eq_of_tan_eq _ ⟨_, _⟩
[GOAL]
case refine'_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = sqrt (↑1 - x ^ 2) / x
[PROOFSTEP]
rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
[GOAL]
case refine'_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x
[PROOFSTEP]
linarith only [arcsin_le_pi_div_two x, pi_pos]
[GOAL]
case refine'_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
[PROOFSTEP]
linarith only [arcsin_pos.2 h]


[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
      (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈ Ioi 0 ×ˢ Ioo (-π) π
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case mk
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y) ∈ Ioi 0 ×ˢ Ioo (-π) π
[PROOFSTEP]
simp only [prod_mk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg, true_and_iff,
  Complex.arg_lt_pi_iff]
[GOAL]
case mk
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2 ∧ (0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0)
[PROOFSTEP]
constructor
[GOAL]
case mk.left
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
cases' hxy with hxy hxy
[GOAL]
case mk.left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst}
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
dsimp at hxy
[GOAL]
case mk.left.inl
x y : ℝ
hxy : 0 < x
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
linarith [sq_pos_of_ne_zero _ hxy.ne', sq_nonneg y]
[GOAL]
case mk.left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.snd ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
[PROOFSTEP]
linarith [sq_nonneg x, sq_pos_of_ne_zero _ hxy]
[GOAL]
case mk.right
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ 0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0
[PROOFSTEP]
cases' hxy with hxy hxy
[GOAL]
case mk.right.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst}
⊢ 0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0
[PROOFSTEP]
exact Or.inl (le_of_lt hxy)
[GOAL]
case mk.right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.snd ≠ 0}
⊢ 0 ≤ (↑Complex.equivRealProd.symm (x, y)).re ∨ (↑Complex.equivRealProd.symm (x, y)).im ≠ 0
[PROOFSTEP]
exact Or.inr hxy
[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ Ioi 0 ×ˢ Ioo (-π) π → (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
rintro ⟨r, θ⟩ ⟨hr, hθ⟩
[GOAL]
case mk.intro
r θ : ℝ
hr : (r, θ).fst ∈ Ioi 0
hθ : (r, θ).snd ∈ Ioo (-π) π
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
dsimp at hr hθ
[GOAL]
case mk.intro
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
rcases eq_or_ne θ 0 with (rfl | h'θ)
[GOAL]
case mk.intro.inl
r : ℝ
hr : r ∈ Ioi 0
hθ : 0 ∈ Ioo (-π) π
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, 0) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
simpa using hr
[GOAL]
case mk.intro.inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
[PROOFSTEP]
right
[GOAL]
case mk.intro.inr.h
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | q.snd ≠ 0}
[PROOFSTEP]
simp at hr
[GOAL]
case mk.intro.inr.h
r θ : ℝ
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
hr : 0 < r
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ) ∈ {q | q.snd ≠ 0}
[PROOFSTEP]
simpa only [ne_of_gt hr, Ne.def, mem_setOf_eq, mul_eq_zero, false_or_iff, sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2] using
  h'θ
[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
      (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
          ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
        x
[PROOFSTEP]
rintro ⟨x, y⟩ _
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
have A : sqrt (x ^ 2 + y ^ 2) = Complex.abs (x + y * Complex.I) := by
  simp [Complex.abs_def, Complex.normSq, pow_two, MonoidWithZeroHom.coe_mk, Complex.add_re, Complex.ofReal_re,
    Complex.mul_re, Complex.I_re, mul_zero, Complex.ofReal_im, Complex.I_im, sub_self, add_zero, Complex.add_im,
    Complex.mul_im, mul_one, zero_add]
[GOAL]
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
[PROOFSTEP]
simp [Complex.abs_def, Complex.normSq, pow_two, MonoidWithZeroHom.coe_mk, Complex.add_re, Complex.ofReal_re,
  Complex.mul_re, Complex.I_re, mul_zero, Complex.ofReal_im, Complex.I_im, sub_self, add_zero, Complex.add_im,
  Complex.mul_im, mul_one, zero_add]
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
A : sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
have Z := Complex.abs_mul_cos_add_sin_mul_I (x + y * Complex.I)
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
A : sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
Z :
  ↑(↑Complex.abs (↑x + ↑y * Complex.I)) *
      (Complex.cos ↑(Complex.arg (↑x + ↑y * Complex.I)) +
        Complex.sin ↑(Complex.arg (↑x + ↑y * Complex.I)) * Complex.I) =
    ↑x + ↑y * Complex.I
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
simp only [← Complex.ofReal_cos, ← Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc] at Z
[GOAL]
case mk
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
A : sqrt (x ^ 2 + y ^ 2) = ↑Complex.abs (↑x + ↑y * Complex.I)
Z :
  ↑(↑Complex.abs (↑x + ↑y * Complex.I) * cos (Complex.arg (↑x + ↑y * Complex.I))) +
      ↑(↑Complex.abs (↑x + ↑y * Complex.I) * sin (Complex.arg (↑x + ↑y * Complex.I))) * Complex.I =
    ↑x + ↑y * Complex.I
⊢ (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
      ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) (x, y)) =
    (x, y)
[PROOFSTEP]
simpa [A, -Complex.ofReal_cos, -Complex.ofReal_sin] using Complex.ext_iff.1 Z
[GOAL]
⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ Ioi 0 ×ˢ Ioo (-π) π →
      (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
          ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
        x
[PROOFSTEP]
rintro ⟨r, θ⟩ ⟨hr, hθ⟩
[GOAL]
case mk.intro
r θ : ℝ
hr : (r, θ).fst ∈ Ioi 0
hθ : (r, θ).snd ∈ Ioo (-π) π
⊢ (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
      ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ)) =
    (r, θ)
[PROOFSTEP]
dsimp at hr hθ
[GOAL]
case mk.intro
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
      ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) (r, θ)) =
    (r, θ)
[PROOFSTEP]
simp only [Prod.mk.inj_iff]
[GOAL]
case mk.intro
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ sqrt ((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r ∧ Complex.arg (↑Complex.equivRealProd.symm (r * cos θ, r * sin θ)) = θ
[PROOFSTEP]
constructor
[GOAL]
case mk.intro.left
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ sqrt ((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r
[PROOFSTEP]
conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r
[PROOFSTEP]
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r
[PROOFSTEP]
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r
[PROOFSTEP]
rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
[GOAL]
case mk.intro.left
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ sqrt ((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = sqrt ((sin θ ^ 2 + cos θ ^ 2) * r ^ 2)
[PROOFSTEP]
congr 1
[GOAL]
case mk.intro.left.e_x
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (r * cos θ) ^ 2 + (r * sin θ) ^ 2 = (sin θ ^ 2 + cos θ ^ 2) * r ^ 2
[PROOFSTEP]
ring
[GOAL]
case mk.intro.right
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ Complex.arg (↑Complex.equivRealProd.symm (r * cos θ, r * sin θ)) = θ
[PROOFSTEP]
convert Complex.arg_mul_cos_add_sin_mul_I hr ⟨hθ.1, hθ.2.le⟩
[GOAL]
case h.e'_2.h.e'_1
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ ↑Complex.equivRealProd.symm (r * cos θ, r * sin θ) = ↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)
[PROOFSTEP]
simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos, Complex.ofReal_sin]
[GOAL]
case h.e'_2.h.e'_1
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ ↑r * Complex.cos ↑θ + ↑r * Complex.sin ↑θ * Complex.I = ↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)
[PROOFSTEP]
ring
[GOAL]
⊢ ContinuousOn
    ↑{ toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
apply ((continuous_fst.pow 2).add (continuous_snd.pow 2)).sqrt.continuousOn.prod
[GOAL]
⊢ ContinuousOn (fun x => Complex.arg (↑Complex.equivRealProd.symm x))
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0} :=
  by rintro ⟨x, y⟩ hxy; simpa only using hxy
[GOAL]
⊢ MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case mk
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}
⊢ ↑Complex.equivRealProd.symm (x, y) ∈ {z | 0 < z.re ∨ z.im ≠ 0}
[PROOFSTEP]
simpa only using hxy
[GOAL]
A : MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
⊢ ContinuousOn (fun x => Complex.arg (↑Complex.equivRealProd.symm x))
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
refine' ContinuousOn.comp (f := Complex.equivRealProd.symm) (g := Complex.arg) (fun z hz => _) _ A
[GOAL]
case refine'_1
A : MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
z : ℂ
hz : z ∈ {z | 0 < z.re ∨ z.im ≠ 0}
⊢ ContinuousWithinAt Complex.arg {z | 0 < z.re ∨ z.im ≠ 0} z
[PROOFSTEP]
exact (Complex.continuousAt_arg hz).continuousWithinAt
[GOAL]
case refine'_2
A : MapsTo (↑Complex.equivRealProd.symm) ({q | 0 < q.fst} ∪ {q | q.snd ≠ 0}) {z | 0 < z.re ∨ z.im ≠ 0}
⊢ ContinuousOn ↑Complex.equivRealProd.symm
    { toFun := fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)),
        invFun := fun p => (p.fst * cos p.snd, p.fst * sin p.snd), source := {q | 0 < q.fst} ∪ {q | q.snd ≠ 0},
        target := Ioi 0 ×ˢ Ioo (-π) π,
        map_source' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x ∈
                  Ioi 0 ×ˢ Ioo (-π) π),
        map_target' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}),
        left_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ {q | 0 < q.fst} ∪ {q | q.snd ≠ 0} →
                (fun p => (p.fst * cos p.snd, p.fst * sin p.snd))
                    ((fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : ℝ × ℝ⦄,
              x ∈ Ioi 0 ×ˢ Ioo (-π) π →
                (fun q => (sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q)))
                    ((fun p => (p.fst * cos p.snd, p.fst * sin p.snd)) x) =
                  x) }.source
[PROOFSTEP]
exact Complex.equivRealProdClm.symm.continuous.continuousOn
[GOAL]
p : ℝ × ℝ
⊢ HasFDerivAt (↑(LocalHomeomorph.symm polarCoord))
    (↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]])))
    p
[PROOFSTEP]
rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]
[GOAL]
p : ℝ × ℝ
⊢ HasFDerivAt (↑(LocalHomeomorph.symm polarCoord))
    (ContinuousLinearMap.prod
      (cos p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.fst * sin p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ)
      (sin p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.fst * cos p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
[PROOFSTEP]
convert
  HasFDerivAt.prod (𝕜 := ℝ) (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
    (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
  2
[GOAL]
case h.e'_10.h.e'_15.h.h.h
p : ℝ × ℝ
e_4✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = AddCommGroup.toAddCommMonoid
e_8✝ : NonUnitalNonAssocSemiring.toAddCommMonoid = AddCommGroup.toAddCommMonoid
he✝¹ : Prod.instModule = NormedSpace.toModule
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ cos p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.fst * sin p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.fst • -sin p.snd • ContinuousLinearMap.snd ℝ ℝ ℝ + (cos ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
simp [smul_smul, add_comm, neg_mul, neg_smul, smul_neg]
[GOAL]
case h.e'_10.h.e'_16.h.h.h
p : ℝ × ℝ
e_4✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = AddCommGroup.toAddCommMonoid
e_11✝ : NonUnitalNonAssocSemiring.toAddCommMonoid = AddCommGroup.toAddCommMonoid
he✝¹ : Prod.instModule = NormedSpace.toModule
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ sin p.snd • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.fst * cos p.snd) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.fst • cos p.snd • ContinuousLinearMap.snd ℝ ℝ ℝ + (sin ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
simp [smul_smul, add_comm, neg_mul, neg_smul, smul_neg]
[GOAL]
⊢ polarCoord.source =ᵐ[volume] univ
[PROOFSTEP]
have A : polarCoord.sourceᶜ ⊆ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) :=
  by
  intro x hx
  simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt, Classical.not_not] at
    hx
  exact hx.2
[GOAL]
⊢ polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
[PROOFSTEP]
intro x hx
[GOAL]
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
[PROOFSTEP]
simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt, Classical.not_not] at hx
[GOAL]
x : ℝ × ℝ
hx : x.fst ≤ 0 ∧ x.snd = 0
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
[PROOFSTEP]
exact hx.2
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.source =ᵐ[volume] univ
[PROOFSTEP]
have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 :=
  by
  apply Measure.addHaar_submodule
  rw [Ne.def, LinearMap.ker_eq_top]
  intro h
  have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
  simp at this
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
[PROOFSTEP]
apply Measure.addHaar_submodule
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) ≠ ⊤
[PROOFSTEP]
rw [Ne.def, LinearMap.ker_eq_top]
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0
[PROOFSTEP]
intro h
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False
[PROOFSTEP]
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
[PROOFSTEP]
rw [h]
[GOAL]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
this : ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
⊢ False
[PROOFSTEP]
simp at this
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ polarCoord.source =ᵐ[volume] univ
[PROOFSTEP]
simp only [ae_eq_univ]
[GOAL]
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ ↑↑volume polarCoord.sourceᶜ = 0
[PROOFSTEP]
exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
set B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p =>
  LinearMap.toContinuousLinearMap
    (Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
have A : ∀ p ∈ polarCoord.symm.source, HasFDerivAt polarCoord.symm (B p) p := fun p _ => hasFDerivAt_polarCoord_symm p
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
have B_det : ∀ p, (B p).det = p.1 := by
  intro p
  conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
  simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin, Matrix.det_fin_two_of, sub_neg_eq_add]
  ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
⊢ ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
[PROOFSTEP]
intro p
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
⊢ ContinuousLinearMap.det (B p) = p.fst
[PROOFSTEP]
conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
| p.fst
[PROOFSTEP]
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
| p.fst
[PROOFSTEP]
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
| p.fst
[PROOFSTEP]
rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
⊢ ContinuousLinearMap.det (B p) = (cos p.snd ^ 2 + sin p.snd ^ 2) * p.fst
[PROOFSTEP]
simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin, Matrix.det_fin_two_of, sub_neg_eq_add]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
p : ℝ × ℝ
⊢ cos p.snd * (p.fst * cos p.snd) + p.fst * sin p.snd * sin p.snd = (cos p.snd ^ 2 + sin p.snd ^ 2) * p.fst
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p
[PROOFSTEP]
symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p)
[PROOFSTEP]
calc
  ∫ p, f p = ∫ p in polarCoord.source, f p := by
    rw [← integral_univ]
    apply set_integral_congr_set_ae
    exact polarCoord_source_ae_eq_univ.symm
  _ = ∫ p in polarCoord.target, abs (B p).det • f (polarCoord.symm p) := by
    apply integral_target_eq_integral_abs_det_fderiv_smul volume A
  _ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) :=
    by
    apply set_integral_congr polarCoord.open_target.measurableSet fun x hx => ?_
    rw [B_det, abs_of_pos]
    exact hx.1
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.source, f p
[PROOFSTEP]
rw [← integral_univ]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (x : ℝ × ℝ) in univ, f x = ∫ (p : ℝ × ℝ) in polarCoord.source, f p
[PROOFSTEP]
apply set_integral_congr_set_ae
[GOAL]
case hst
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ univ =ᵐ[volume] polarCoord.source
[PROOFSTEP]
exact polarCoord_source_ae_eq_univ.symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ) in polarCoord.source, f p =
    ∫ (p : ℝ × ℝ) in polarCoord.target, |ContinuousLinearMap.det (B p)| • f (↑(LocalHomeomorph.symm polarCoord) p)
[PROOFSTEP]
apply integral_target_eq_integral_abs_det_fderiv_smul volume A
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, |ContinuousLinearMap.det (B p)| • f (↑(LocalHomeomorph.symm polarCoord) p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p)
[PROOFSTEP]
apply set_integral_congr polarCoord.open_target.measurableSet fun x hx => ?_
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ |ContinuousLinearMap.det (B x)| • f (↑(LocalHomeomorph.symm polarCoord) x) =
    x.fst • f (↑(LocalHomeomorph.symm polarCoord) x)
[PROOFSTEP]
rw [B_det, abs_of_pos]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ × ℝ → E
B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  fun p =>
    ↑LinearMap.toContinuousLinearMap
      (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
        (↑Matrix.of ![![cos p.snd, -p.fst * sin p.snd], ![sin p.snd, p.fst * cos p.snd]]))
A :
  ∀ (p : ℝ × ℝ),
    p ∈ (LocalHomeomorph.symm polarCoord).toLocalEquiv.source → HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (B p) p
B_det : ∀ (p : ℝ × ℝ), ContinuousLinearMap.det (B p) = p.fst
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ 0 < x.fst
[PROOFSTEP]
exact hx.1


[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasStrictFDerivAt (exp 𝕂) 1 0
[PROOFSTEP]
convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt
[GOAL]
case h.e'_10
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ 1 = ↑(continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
x : 𝔸
⊢ ↑1 x = ↑(↑(continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)) x
[PROOFSTEP]
change x = expSeries 𝕂 𝔸 1 fun _ => x
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
x : 𝔸
⊢ x = ↑(expSeries 𝕂 𝔸 1) fun x_1 => x
[PROOFSTEP]
simp [expSeries_apply_eq]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
[PROOFSTEP]
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
[PROOFSTEP]
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - ↑(exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h
[PROOFSTEP]
suffices
  (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ContinuousLinearMap.id 𝕂 𝔸 h
  by
  refine' (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
  rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
  exact hasFDerivAt_exp_zero_of_radius_pos hpos
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) h
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - ↑(exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h
[PROOFSTEP]
refine' (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) h
⊢ (fun x => exp 𝕂 (0 + x) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) x) =o[𝓝 0] fun h => h
[PROOFSTEP]
rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) h
⊢ HasFDerivAt (exp 𝕂) (ContinuousLinearMap.id 𝕂 𝔸) 0
[PROOFSTEP]
exact hasFDerivAt_exp_zero_of_radius_pos hpos
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) h
[PROOFSTEP]
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := EMetric.ball_mem_nhds _ hpos
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) h
[PROOFSTEP]
filter_upwards [this] with _ hh
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * (exp 𝕂 (0 + a✝) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp 𝕂 (x + a✝) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) a✝
[PROOFSTEP]
rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * (exp 𝕂 a✝ - 1 - a✝) = exp 𝕂 x * exp 𝕂 a✝ - exp 𝕂 x - exp 𝕂 x * a✝
[PROOFSTEP]
ring
[GOAL]
𝕂 : Type u_1
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : CompleteSpace 𝕂
inst✝ : CharZero 𝕂
x : 𝕂
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝕂))
⊢ HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x
[PROOFSTEP]
simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt
[GOAL]
⊢ exp = _root_.exp ℂ
[PROOFSTEP]
refine' funext fun x => _
[GOAL]
x : ℂ
⊢ exp x = _root_.exp ℂ x
[PROOFSTEP]
rw [Complex.exp, exp_eq_tsum_div]
[GOAL]
x : ℂ
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
[PROOFSTEP]
have : CauSeq.IsComplete ℂ norm := Complex.instIsComplete
[GOAL]
x : ℂ
this : CauSeq.IsComplete ℂ norm
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
[PROOFSTEP]
exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat
[GOAL]
⊢ exp = _root_.exp ℝ
[PROOFSTEP]
ext x
[GOAL]
case h
x : ℝ
⊢ exp x = _root_.exp ℝ x
[PROOFSTEP]
exact_mod_cast congr_fun Complex.exp_eq_exp_ℂ x
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
[PROOFSTEP]
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt htx
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
[PROOFSTEP]
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0]
    fun h => h
[PROOFSTEP]
suffices
  (fun (h : 𝕊) => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 ((0 : 𝕊) • x) - ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) h
  by
  apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
  rw [← @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u • x)) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x) 0]
  have : HasFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x 0) :=
    by
    rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
    exact hasFDerivAt_exp_zero_of_radius_pos hpos
  exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ (fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0]
    fun h => h
[PROOFSTEP]
apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ (fun x_1 => exp 𝕂 ((0 + x_1) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) x_1) =o[𝓝 0] fun h => h
[PROOFSTEP]
rw [← @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u • x)) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x) 0]
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (ContinuousLinearMap.smulRight 1 x) 0
[PROOFSTEP]
have : HasFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x 0) :=
  by
  rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
  exact hasFDerivAt_exp_zero_of_radius_pos hpos
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (exp 𝕂) 1 (↑(ContinuousLinearMap.smulRight 1 x) 0)
[PROOFSTEP]
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (exp 𝕂) 1 0
[PROOFSTEP]
exact hasFDerivAt_exp_zero_of_radius_pos hpos
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
this : HasFDerivAt (exp 𝕂) 1 (↑(ContinuousLinearMap.smulRight 1 x) 0)
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (ContinuousLinearMap.smulRight 1 x) 0
[PROOFSTEP]
exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
[PROOFSTEP]
have : Tendsto (fun h : 𝕊 => h • x) (𝓝 0) (𝓝 0) :=
  by
  rw [← zero_smul 𝕊 x]
  exact tendsto_id.smul_const x
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
rw [← zero_smul 𝕊 x]
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 (0 • x))
[PROOFSTEP]
exact tendsto_id.smul_const x
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
⊢ (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
[PROOFSTEP]
have : ∀ᶠ h in 𝓝 (0 : 𝕊), h • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  this.eventually (EMetric.ball_mem_nhds _ hpos)
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
[PROOFSTEP]
filter_upwards [this] with h hh
[GOAL]
case h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h) =
    exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
[PROOFSTEP]
have : Commute (t • x) (h • x) := ((Commute.refl x).smul_left t).smul_right h
[GOAL]
case h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝¹ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
this : Commute (t • x) (h • x)
⊢ exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - ↑(ContinuousLinearMap.smulRight 1 x) h) =
    exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
[PROOFSTEP]
rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, ContinuousLinearMap.smul_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib,
  mul_sub_left_distrib, mul_one]
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t
[PROOFSTEP]
convert hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
[GOAL]
case h.e'_10
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x)) =
    exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x
[PROOFSTEP]
ext t'
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
t' : 𝕊
⊢ ↑(ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t' =
    ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t'
[PROOFSTEP]
show Commute (t' • x) (exp 𝕂 (t • x))
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
t' : 𝕊
⊢ Commute (t' • x) (exp 𝕂 (t • x))
[PROOFSTEP]
exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasStrictFDerivAt (fun u => exp 𝕂 (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t
[PROOFSTEP]
let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t • x) htx
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
⊢ HasStrictFDerivAt (fun u => exp 𝕂 (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t
[PROOFSTEP]
convert hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
[GOAL]
case h.e'_10
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x)) =
    exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x
[PROOFSTEP]
ext t'
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
t' : 𝕊
⊢ ↑(ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t' =
    ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t'
[PROOFSTEP]
show Commute (t' • x) (exp 𝕂 (t • x))
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
t' : 𝕊
⊢ Commute (t' • x) (exp 𝕂 (t • x))
[PROOFSTEP]
exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t
[PROOFSTEP]
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt
[GOAL]
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx : t • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t
[PROOFSTEP]
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).hasStrictDerivAt