feat(analysis/special_functions/trigonometric): Added lemmas for deri…

…v of tan (#3746)

I added lemmas for the derivative of the tangent function in both the complex and real namespaces. I also corrected two typos in comment lines.
<!-- put comments you want to keep out of the PR commit here -->

src/analysis/special_functions/trigonometric.lean

@@ -80,11 +80,7 @@ funext $ λ x, deriv_cos
 lemma continuous_cos : continuous cos :=
 differentiable_cos.continuous
 
-lemma continuous_tan : continuous (λ x : {x // cos x ≠ 0}, tan x) :=
-(continuous_sin.comp continuous_subtype_val).mul
-  (continuous.inv subtype.property (continuous_cos.comp continuous_subtype_val))
-
-/-- The complex hyperbolic sine function is everywhere differentiable, with the derivative `sinh x`. -/
+/-- The complex hyperbolic sine function is everywhere differentiable, with the derivative `cosh x`. -/
 lemma has_deriv_at_sinh (x : ℂ) : has_deriv_at sinh (cosh x) x :=
 begin
   simp only [cosh, div_eq_mul_inv],
@@ -104,7 +100,7 @@ funext $ λ x, (has_deriv_at_sinh x).deriv
 lemma continuous_sinh : continuous sinh :=
 differentiable_sinh.continuous
 
-/-- The complex hyperbolic cosine function is everywhere differentiable, with the derivative `cosh x`. -/
+/-- The complex hyperbolic cosine function is everywhere differentiable, with the derivative `sinh x`. -/
 lemma has_deriv_at_cosh (x : ℂ) : has_deriv_at cosh (sinh x) x :=
 begin
   simp only [sinh, div_eq_mul_inv],
@@ -312,12 +308,6 @@ funext $ λ _, deriv_cos
 lemma continuous_cos : continuous cos :=
 differentiable_cos.continuous
 
-lemma continuous_tan : continuous (λ x : {x // cos x ≠ 0}, tan x) :=
-by simp only [tan_eq_sin_div_cos]; exact
-  (continuous_sin.comp continuous_subtype_val).mul
-  (continuous.inv subtype.property
-    (continuous_cos.comp continuous_subtype_val))
-
 lemma has_deriv_at_sinh (x : ℝ) : has_deriv_at sinh (cosh x) x :=
 has_deriv_at_real_of_complex (complex.has_deriv_at_sinh x)
 
@@ -627,25 +617,25 @@ by simp [sub_eq_add_neg, cos_add]
 lemma cos_pi_div_two_sub (x : ℝ) : cos (π / 2 - x) = sin x :=
 by rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
 
-lemma cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two
+lemma cos_pos_of_mem_Ioo
   {x : ℝ} (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) : 0 < cos x :=
 sin_add_pi_div_two x ▸ sin_pos_of_pos_of_lt_pi (by linarith) (by linarith)
 
-lemma cos_nonneg_of_neg_pi_div_two_le_of_le_pi_div_two
+lemma cos_nonneg_of_mem_Icc
   {x : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) : 0 ≤ cos x :=
 match lt_or_eq_of_le hx₁, lt_or_eq_of_le hx₂ with
-| or.inl hx₁, or.inl hx₂ := le_of_lt (cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two hx₁ hx₂)
+| or.inl hx₁, or.inl hx₂ := le_of_lt (cos_pos_of_mem_Ioo hx₁ hx₂)
 | or.inl hx₁, or.inr hx₂ := by simp [hx₂]
 | or.inr hx₁, _          := by simp [hx₁.symm]
 end
 
 lemma cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) : cos x < 0 :=
 neg_pos.1 $ cos_pi_sub x ▸
-  cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) (by linarith)
+  cos_pos_of_mem_Ioo (by linarith) (by linarith)
 
 lemma cos_nonpos_of_pi_div_two_le_of_le {x : ℝ} (hx₁ : π / 2 ≤ x) (hx₂ : x ≤ π + π / 2) : cos x ≤ 0 :=
 neg_nonneg.1 $ cos_pi_sub x ▸
-  cos_nonneg_of_neg_pi_div_two_le_of_le_pi_div_two (by linarith) (by linarith)
+  cos_nonneg_of_mem_Icc (by linarith) (by linarith)
 
 lemma sin_nat_mul_pi (n : ℕ) : sin (n * π) = 0 :=
 by induction n; simp [add_mul, sin_add, *]
@@ -706,21 +696,6 @@ lemma cos_eq_one_iff (x : ℝ) : cos x = 1 ↔ ∃ n : ℤ, (n : ℝ) * (2 * π)
         exact absurd h (by norm_num))⟩,
   λ ⟨n, hn⟩, hn ▸ cos_int_mul_two_pi _⟩
 
-theorem cos_eq_zero_iff {θ : ℝ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * pi / 2 :=
-begin
-  rw [←real.sin_pi_div_two_sub, sin_eq_zero_iff],
-  split,
-  { rintro ⟨n, hn⟩, existsi -n,
-    rw [int.cast_neg, add_mul, add_div, mul_assoc, mul_div_cancel_left _ (@two_ne_zero ℝ _),
-        one_mul, ←neg_mul_eq_neg_mul, hn, neg_sub, sub_add_cancel] },
-  { rintro ⟨n, hn⟩, existsi -n,
-    rw [hn, add_mul, one_mul, add_div, mul_assoc, mul_div_cancel_left _ (@two_ne_zero ℝ _),
-        sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_neg_mul, int.cast_neg] }
-end
-
-theorem cos_ne_zero_iff {θ : ℝ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * pi / 2 :=
-by rw [← not_exists, not_iff_not, cos_eq_zero_iff]
-
 lemma cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * π) < x) (hx₂ : x < 2 * π) : cos x = 1 ↔ x = 0 :=
 ⟨λ h, let ⟨n, hn⟩ := (cos_eq_one_iff x).1 h in
     begin
@@ -744,7 +719,7 @@ calc cos y = cos x * cos (y - x) - sin x * sin (y - x) :
   by rw [← cos_add, add_sub_cancel'_right]
 ... < (cos x * 1) - sin x * sin (y - x) :
   sub_lt_sub_right ((mul_lt_mul_left
-    (cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (lt_of_lt_of_le (neg_neg_of_pos pi_div_two_pos) hx₁)
+    (cos_pos_of_mem_Ioo (lt_of_lt_of_le (neg_neg_of_pos pi_div_two_pos) hx₁)
       (lt_of_lt_of_le hxy hy₂))).2
         (lt_of_le_of_ne (cos_le_one _) (mt (cos_eq_one_iff_of_lt_of_lt
           (show -(2 * π) < y - x, by linarith) (show y - x < 2 * π, by linarith)).1
@@ -759,7 +734,7 @@ match (le_total x (π / 2) : x ≤ π / 2 ∨ π / 2 ≤ x), le_total y (π / 2)
 | or.inl hx, or.inl hy := cos_lt_cos_of_nonneg_of_le_pi_div_two hx₁ hy hxy
 | or.inl hx, or.inr hy := (lt_or_eq_of_le hx).elim
   (λ hx, calc cos y ≤ 0 : cos_nonpos_of_pi_div_two_le_of_le hy (by linarith [pi_pos])
-    ... < cos x : cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) hx)
+    ... < cos x : cos_pos_of_mem_Ioo (by linarith) hx)
   (λ hx, calc cos y < 0 : cos_neg_of_pi_div_two_lt_of_lt (by linarith) (by linarith [pi_pos])
     ... = cos x : by rw [hx, cos_pi_div_two])
 | or.inr hx, or.inl hy := by linarith
@@ -923,7 +898,7 @@ lemma sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) :
         mul_div_cancel_left],
     norm_num, norm_num, norm_num,
     apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num,
-    apply le_of_lt, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
+    apply le_of_lt, apply cos_pos_of_mem_Ioo,
     { transitivity (0 : ℝ), rw neg_lt_zero, apply pi_div_two_pos,
       apply div_pos pi_pos, apply pow_pos, norm_num },
     apply div_lt_div' (le_refl pi) _ pi_pos _,
@@ -1188,7 +1163,7 @@ lemma arccos_neg (x : ℝ) : arccos (-x) = π - arccos x :=
 by rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self]; simp
 
 lemma cos_arcsin_nonneg (x : ℝ) : 0 ≤ cos (arcsin x) :=
-cos_nonneg_of_neg_pi_div_two_le_of_le_pi_div_two
+cos_nonneg_of_mem_Icc
     (neg_pi_div_two_le_arcsin _) (arcsin_le_pi_div_two _)
 
 lemma cos_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : cos (arcsin x) = sqrt (1 - x ^ 2) :=
@@ -1226,7 +1201,7 @@ end
 
 lemma tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < π / 2) : 0 < tan x :=
 by rw tan_eq_sin_div_cos; exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith))
-  (cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) hxp)
+  (cos_pos_of_mem_Ioo (by linarith) hxp)
 
 lemma tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ π / 2) : 0 ≤ tan x :=
 match lt_or_eq_of_le h0x, lt_or_eq_of_le hxp with
@@ -1249,7 +1224,7 @@ begin
     (sin_lt_sin_of_le_of_le_pi_div_two (by linarith) (le_of_lt hy₂) hxy)
     (cos_le_cos_of_nonneg_of_le_pi hx₁ (by linarith) (le_of_lt hxy))
     (sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith))
-    (cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) hy₂)
+    (cos_pos_of_mem_Ioo (by linarith) hy₂)
 end
 
 lemma tan_lt_tan_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) < x)
@@ -1446,7 +1421,7 @@ lemma arg_cos_add_sin_mul_I {x : ℝ} (hx₁ : -π < x) (hx₂ : x ≤ π) :
 if hx₃ : -(π / 2) ≤ x ∧ x ≤ π / 2
 then
   have hx₄ : 0 ≤ (cos x + sin x * I).re,
-    by simp; exact real.cos_nonneg_of_neg_pi_div_two_le_of_le_pi_div_two hx₃.1 hx₃.2,
+    by simp; exact real.cos_nonneg_of_mem_Icc hx₃.1 hx₃.2,
   by rw [arg, if_pos hx₄];
     simp [abs_cos_add_sin_mul_I, sin_of_real_re, real.arcsin_sin hx₃.1 hx₃.2]
 else if hx₄ : x < -(π / 2)
@@ -1690,4 +1665,98 @@ by cases n; simp only [cos_nat_mul_two_pi, int.of_nat_eq_coe,
 lemma cos_int_mul_two_pi_add_pi (n : ℤ) : cos (n * (2 * π) + π) = -1 :=
 by simp [cos_add, sin_add, cos_int_mul_two_pi]
 
+lemma exp_pi_mul_I : exp (π * I) = -1 := by { rw exp_mul_I, simp, }
+
+theorem cos_eq_zero_iff {θ : ℂ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * π / 2 :=
+begin
+  have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1,
+  { rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 (by norm_num), zero_mul, add_eq_zero_iff_eq_neg,
+        neg_eq_neg_one_mul (exp (-θ * I)), ← div_eq_iff (exp_ne_zero (-θ * I)), ← exp_sub],
+    field_simp, ring },
+  rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int],
+  split; simp; intros; use x,
+  { field_simp, ring at a,
+    rwa [mul_right_comm 2 I θ, mul_right_comm (2*(x:ℂ)+1) I (π:ℂ), mul_left_inj' I_ne_zero,
+        mul_comm 2 θ] at a },
+  { field_simp at a, ring,
+    rw [mul_right_comm 2 I θ, mul_right_comm (2*(x:ℂ)+1) I (π:ℂ), mul_left_inj' I_ne_zero,
+        mul_comm 2 θ, a] },
+end
+
+theorem cos_ne_zero_iff {θ : ℂ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 :=
+by rw [← not_exists, not_iff_not, cos_eq_zero_iff]
+
+lemma has_deriv_at_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
+  has_deriv_at tan (1 / (cos x)^2) x :=
+begin
+  convert has_deriv_at.div (has_deriv_at_sin x) (has_deriv_at_cos x) (cos_ne_zero_iff.mpr h),
+  rw ← sin_sq_add_cos_sq x,
+  ring,
+end
+
+lemma differentiable_at_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : differentiable_at ℂ tan x :=
+(has_deriv_at_tan h).differentiable_at
+
+@[simp] lemma deriv_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : deriv tan x = 1 / (cos x)^2 :=
+(has_deriv_at_tan h).deriv
+
+lemma continuous_tan : continuous (λ x : {x | cos x ≠ 0}, tan x) :=
+(continuous_sin.comp continuous_subtype_val).mul
+  (continuous.inv subtype.property (continuous_cos.comp continuous_subtype_val))
+
+lemma continuous_on_tan : continuous_on tan {x | cos x ≠ 0} :=
+by { rw continuous_on_iff_continuous_restrict, convert continuous_tan }
+
 end complex
+
+
+namespace real
+
+open_locale real
+
+theorem cos_eq_zero_iff {θ : ℝ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * π / 2 :=
+begin
+  rw [← complex.of_real_eq_zero, complex.of_real_cos θ],
+  convert @complex.cos_eq_zero_iff θ,
+  norm_cast,
+end
+
+theorem cos_ne_zero_iff {θ : ℝ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 :=
+by rw [← not_exists, not_iff_not, cos_eq_zero_iff]
+
+
+lemma has_deriv_at_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
+  has_deriv_at tan (1 / (cos x)^2) x :=
+begin
+  convert has_deriv_at_real_of_complex (complex.has_deriv_at_tan (by { convert h, norm_cast } )),
+  rw ← complex.of_real_re (1/((cos x)^2)),
+  simp,
+end
+
+lemma differentiable_at_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : differentiable_at ℝ tan x :=
+(has_deriv_at_tan h).differentiable_at
+
+@[simp] lemma deriv_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : deriv tan x = 1 / (cos x)^2 :=
+(has_deriv_at_tan h).deriv
+
+lemma continuous_tan : continuous (λ x : {x | cos x ≠ 0}, tan x) :=
+by simp only [tan_eq_sin_div_cos]; exact
+  (continuous_sin.comp continuous_subtype_val).mul
+  (continuous.inv subtype.property
+    (continuous_cos.comp continuous_subtype_val))
+
+lemma continuous_on_tan : continuous_on tan {x | cos x ≠ 0} :=
+by { rw continuous_on_iff_continuous_restrict, convert continuous_tan }
+
+lemma has_deriv_at_tan_of_mem_Ioo {x : ℝ} (h : x ∈ set.Ioo (-(π/2):ℝ) (π/2)) :
+  has_deriv_at tan (1 / (cos x)^2) x :=
+has_deriv_at_tan (cos_ne_zero_iff.mp (ne_of_gt (cos_pos_of_mem_Ioo h.1 h.2)))
+
+lemma differentiable_at_tan_of_mem_Ioo {x : ℝ} (h : x ∈ set.Ioo (-(π/2):ℝ) (π/2)) :
+  differentiable_at ℝ tan x :=
+(has_deriv_at_tan_of_mem_Ioo h).differentiable_at
+
+lemma deriv_tan_of_mem_Ioo {x : ℝ} (h : x ∈ set.Ioo (-(π/2):ℝ) (π/2)) : deriv tan x = 1 / (cos x)^2 :=
+(has_deriv_at_tan_of_mem_Ioo h).deriv
+
+end real