chore(analysis/special_functions/trigonometric/inverse): move results…

… about derivatives to a new file (#10110)

This is part of a refactor of the `analysis/special_functions` folder, in which I will isolate all lemmas about derivatives. The result will be a definition of Lp spaces that does not import derivatives.



Co-authored-by: RemyDegenne <remydegenne@gmail.com>

src/analysis/special_functions/complex/log.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin
 -/
 import analysis.special_functions.complex.arg
 import analysis.special_functions.log
+import analysis.special_functions.trigonometric.inverse_deriv
 
 /-!
 # The complex `log` function

src/analysis/special_functions/trigonometric/inverse.lean

@@ -3,15 +3,17 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
-import analysis.special_functions.trigonometric.deriv
+import analysis.special_functions.trigonometric.basic
+import topology.algebra.ordered.proj_Icc
+
 
 /-!
 # Inverse trigonometric functions.
 
 See also `analysis.special_functions.trigonometric.arctan` for the inverse tan function.
 (This is delayed as it is easier to set up after developing complex trigonometric functions.)
 
-Basic inequalities and derivatives.
+Basic inequalities on trigonometric functions.
 -/
 
 noncomputable theory
@@ -227,112 +229,6 @@ begin
   rw [this, sin_arcsin hx₁ hx₂],
 end
 
-lemma deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
-  has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ arcsin x :=
-begin
-  cases h₁.lt_or_lt with h₁ h₁,
-  { have : 1 - x ^ 2 < 0, by nlinarith [h₁],
-    rw [sqrt_eq_zero'.2 this.le, div_zero],
-    have : arcsin =ᶠ[𝓝 x] λ _, -(π / 2) :=
-      (gt_mem_nhds h₁).mono (λ y hy, arcsin_of_le_neg_one hy.le),
-    exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm,
-      times_cont_diff_at_const.congr_of_eventually_eq this⟩ },
-  cases h₂.lt_or_lt with h₂ h₂,
-  { have : 0 < sqrt (1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂]),
-    simp only [← cos_arcsin h₁.le h₂.le, one_div] at this ⊢,
-    exact ⟨sin_local_homeomorph.has_strict_deriv_at_symm ⟨h₁, h₂⟩ this.ne'
-      (has_strict_deriv_at_sin _),
-      sin_local_homeomorph.times_cont_diff_at_symm_deriv this.ne' ⟨h₁, h₂⟩
-        (has_deriv_at_sin _) times_cont_diff_sin.times_cont_diff_at⟩ },
-  { have : 1 - x ^ 2 < 0, by nlinarith [h₂],
-    rw [sqrt_eq_zero'.2 this.le, div_zero],
-    have : arcsin =ᶠ[𝓝 x] λ _, π / 2 := (lt_mem_nhds h₂).mono (λ y hy, arcsin_of_one_le hy.le),
-    exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm,
-      times_cont_diff_at_const.congr_of_eventually_eq this⟩ }
-end
-
-lemma has_strict_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
-  has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x :=
-(deriv_arcsin_aux h₁ h₂).1
-
-lemma has_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
-  has_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x :=
-(has_strict_deriv_at_arcsin h₁ h₂).has_deriv_at
-
-lemma times_cont_diff_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} :
-  times_cont_diff_at ℝ n arcsin x :=
-(deriv_arcsin_aux h₁ h₂).2.of_le le_top
-
-lemma has_deriv_within_at_arcsin_Ici {x : ℝ} (h : x ≠ -1) :
-  has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x :=
-begin
-  rcases em (x = 1) with (rfl|h'),
-  { convert (has_deriv_within_at_const _ _ (π / 2)).congr _ _;
-      simp [arcsin_of_one_le] { contextual := tt } },
-  { exact (has_deriv_at_arcsin h h').has_deriv_within_at }
-end
-
-lemma has_deriv_within_at_arcsin_Iic {x : ℝ} (h : x ≠ 1) :
-  has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x :=
-begin
-  rcases em (x = -1) with (rfl|h'),
-  { convert (has_deriv_within_at_const _ _ (-(π / 2))).congr _ _;
-      simp [arcsin_of_le_neg_one] { contextual := tt } },
-  { exact (has_deriv_at_arcsin h' h).has_deriv_within_at }
-end
-
-lemma differentiable_within_at_arcsin_Ici {x : ℝ} :
-  differentiable_within_at ℝ arcsin (Ici x) x ↔ x ≠ -1 :=
-begin
-  refine ⟨_, λ h, (has_deriv_within_at_arcsin_Ici h).differentiable_within_at⟩,
-  rintro h rfl,
-  have : sin ∘ arcsin =ᶠ[𝓝[Ici (-1:ℝ)] (-1)] id,
-  { filter_upwards [Icc_mem_nhds_within_Ici ⟨le_rfl, neg_lt_self (@zero_lt_one ℝ _ _)⟩],
-    exact λ x, sin_arcsin' },
-  have := h.has_deriv_within_at.sin.congr_of_eventually_eq this.symm (by simp),
-  simpa using (unique_diff_on_Ici _ _ left_mem_Ici).eq_deriv _ this (has_deriv_within_at_id _ _)
-end
-
-lemma differentiable_within_at_arcsin_Iic {x : ℝ} :
-  differentiable_within_at ℝ arcsin (Iic x) x ↔ x ≠ 1 :=
-begin
-  refine ⟨λ h, _, λ h, (has_deriv_within_at_arcsin_Iic h).differentiable_within_at⟩,
-  rw [← neg_neg x, ← image_neg_Ici] at h,
-  have := (h.comp (-x) differentiable_within_at_id.neg (maps_to_image _ _)).neg,
-  simpa [(∘), differentiable_within_at_arcsin_Ici] using this
-end
-
-lemma differentiable_at_arcsin {x : ℝ} :
-  differentiable_at ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1 :=
-⟨λ h, ⟨differentiable_within_at_arcsin_Ici.1 h.differentiable_within_at,
-  differentiable_within_at_arcsin_Iic.1 h.differentiable_within_at⟩,
-  λ h, (has_deriv_at_arcsin h.1 h.2).differentiable_at⟩
-
-@[simp] lemma deriv_arcsin : deriv arcsin = λ x, 1 / sqrt (1 - x ^ 2) :=
-begin
-  funext x,
-  by_cases h : x ≠ -1 ∧ x ≠ 1,
-  { exact (has_deriv_at_arcsin h.1 h.2).deriv },
-  { rw [deriv_zero_of_not_differentiable_at (mt differentiable_at_arcsin.1 h)],
-    simp only [not_and_distrib, ne.def, not_not] at h,
-    rcases h with (rfl|rfl); simp }
-end
-
-lemma differentiable_on_arcsin : differentiable_on ℝ arcsin {-1, 1}ᶜ :=
-λ x hx, (differentiable_at_arcsin.2
-  ⟨λ h, hx (or.inl h), λ h, hx (or.inr h)⟩).differentiable_within_at
-
-lemma times_cont_diff_on_arcsin {n : with_top ℕ} :
-  times_cont_diff_on ℝ n arcsin {-1, 1}ᶜ :=
-λ x hx, (times_cont_diff_at_arcsin (mt or.inl hx) (mt or.inr hx)).times_cont_diff_within_at
-
-lemma times_cont_diff_at_arcsin_iff {x : ℝ} {n : with_top ℕ} :
-  times_cont_diff_at ℝ n arcsin x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) :=
-⟨λ h, or_iff_not_imp_left.2 $ λ hn, differentiable_at_arcsin.1 $ h.differentiable_at $
-  with_top.one_le_iff_pos.2 (pos_iff_ne_zero.2 hn),
-  λ h, h.elim (λ hn, hn.symm ▸ (times_cont_diff_zero.2 continuous_arcsin).times_cont_diff_at) $
-    λ hx, times_cont_diff_at_arcsin hx.1 hx.2⟩
-
 /-- Inverse of the `cos` function, returns values in the range `0 ≤ arccos x` and `arccos x ≤ π`.
   If the argument is not between `-1` and `1` it defaults to `π / 2` -/
 @[pp_nodot] noncomputable def arccos (x : ℝ) : ℝ :=
@@ -388,51 +284,4 @@ by rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin hx₁ hx
 @[continuity]
 lemma continuous_arccos : continuous arccos := continuous_const.sub continuous_arcsin
 
-lemma has_strict_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
-  has_strict_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x :=
-(has_strict_deriv_at_arcsin h₁ h₂).const_sub (π / 2)
-
-lemma has_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
-  has_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x :=
-(has_deriv_at_arcsin h₁ h₂).const_sub (π / 2)
-
-lemma times_cont_diff_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} :
-  times_cont_diff_at ℝ n arccos x :=
-times_cont_diff_at_const.sub (times_cont_diff_at_arcsin h₁ h₂)
-
-lemma has_deriv_within_at_arccos_Ici {x : ℝ} (h : x ≠ -1) :
-  has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Ici x) x :=
-(has_deriv_within_at_arcsin_Ici h).const_sub _
-
-lemma has_deriv_within_at_arccos_Iic {x : ℝ} (h : x ≠ 1) :
-  has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Iic x) x :=
-(has_deriv_within_at_arcsin_Iic h).const_sub _
-
-lemma differentiable_within_at_arccos_Ici {x : ℝ} :
-  differentiable_within_at ℝ arccos (Ici x) x ↔ x ≠ -1 :=
-(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Ici
-
-lemma differentiable_within_at_arccos_Iic {x : ℝ} :
-  differentiable_within_at ℝ arccos (Iic x) x ↔ x ≠ 1 :=
-(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Iic
-
-lemma differentiable_at_arccos {x : ℝ} :
-  differentiable_at ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1 :=
-(differentiable_at_const_sub_iff _).trans differentiable_at_arcsin
-
-@[simp] lemma deriv_arccos : deriv arccos = λ x, -(1 / sqrt (1 - x ^ 2)) :=
-funext $ λ x, (deriv_const_sub _).trans $ by simp only [deriv_arcsin]
-
-lemma differentiable_on_arccos : differentiable_on ℝ arccos {-1, 1}ᶜ :=
-differentiable_on_arcsin.const_sub _
-
-lemma times_cont_diff_on_arccos {n : with_top ℕ} :
-  times_cont_diff_on ℝ n arccos {-1, 1}ᶜ :=
-times_cont_diff_on_const.sub times_cont_diff_on_arcsin
-
-lemma times_cont_diff_at_arccos_iff {x : ℝ} {n : with_top ℕ} :
-  times_cont_diff_at ℝ n arccos x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) :=
-by refine iff.trans ⟨λ h, _, λ h, _⟩ times_cont_diff_at_arcsin_iff;
-  simpa [arccos] using (@times_cont_diff_at_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h
-
 end real

src/analysis/special_functions/trigonometric/inverse_deriv.lean

@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
+-/
+import analysis.special_functions.trigonometric.inverse
+import analysis.special_functions.trigonometric.deriv
+
+/-!
+# derivatives of the inverse trigonometric functions
+
+Derivatives of `arcsin` and `arccos`.
+-/
+
+noncomputable theory
+open_locale classical topological_space filter
+open set filter
+
+open_locale real
+
+namespace real
+
+section arcsin
+
+lemma deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
+  has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ arcsin x :=
+begin
+  cases h₁.lt_or_lt with h₁ h₁,
+  { have : 1 - x ^ 2 < 0, by nlinarith [h₁],
+    rw [sqrt_eq_zero'.2 this.le, div_zero],
+    have : arcsin =ᶠ[𝓝 x] λ _, -(π / 2) :=
+      (gt_mem_nhds h₁).mono (λ y hy, arcsin_of_le_neg_one hy.le),
+    exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm,
+      times_cont_diff_at_const.congr_of_eventually_eq this⟩ },
+  cases h₂.lt_or_lt with h₂ h₂,
+  { have : 0 < sqrt (1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂]),
+    simp only [← cos_arcsin h₁.le h₂.le, one_div] at this ⊢,
+    exact ⟨sin_local_homeomorph.has_strict_deriv_at_symm ⟨h₁, h₂⟩ this.ne'
+      (has_strict_deriv_at_sin _),
+      sin_local_homeomorph.times_cont_diff_at_symm_deriv this.ne' ⟨h₁, h₂⟩
+        (has_deriv_at_sin _) times_cont_diff_sin.times_cont_diff_at⟩ },
+  { have : 1 - x ^ 2 < 0, by nlinarith [h₂],
+    rw [sqrt_eq_zero'.2 this.le, div_zero],
+    have : arcsin =ᶠ[𝓝 x] λ _, π / 2 := (lt_mem_nhds h₂).mono (λ y hy, arcsin_of_one_le hy.le),
+    exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm,
+      times_cont_diff_at_const.congr_of_eventually_eq this⟩ }
+end
+
+lemma has_strict_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
+  has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x :=
+(deriv_arcsin_aux h₁ h₂).1
+
+lemma has_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
+  has_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x :=
+(has_strict_deriv_at_arcsin h₁ h₂).has_deriv_at
+
+lemma times_cont_diff_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} :
+  times_cont_diff_at ℝ n arcsin x :=
+(deriv_arcsin_aux h₁ h₂).2.of_le le_top
+
+lemma has_deriv_within_at_arcsin_Ici {x : ℝ} (h : x ≠ -1) :
+  has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x :=
+begin
+  rcases em (x = 1) with (rfl|h'),
+  { convert (has_deriv_within_at_const _ _ (π / 2)).congr _ _;
+      simp [arcsin_of_one_le] { contextual := tt } },
+  { exact (has_deriv_at_arcsin h h').has_deriv_within_at }
+end
+
+lemma has_deriv_within_at_arcsin_Iic {x : ℝ} (h : x ≠ 1) :
+  has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x :=
+begin
+  rcases em (x = -1) with (rfl|h'),
+  { convert (has_deriv_within_at_const _ _ (-(π / 2))).congr _ _;
+      simp [arcsin_of_le_neg_one] { contextual := tt } },
+  { exact (has_deriv_at_arcsin h' h).has_deriv_within_at }
+end
+
+lemma differentiable_within_at_arcsin_Ici {x : ℝ} :
+  differentiable_within_at ℝ arcsin (Ici x) x ↔ x ≠ -1 :=
+begin
+  refine ⟨_, λ h, (has_deriv_within_at_arcsin_Ici h).differentiable_within_at⟩,
+  rintro h rfl,
+  have : sin ∘ arcsin =ᶠ[𝓝[Ici (-1:ℝ)] (-1)] id,
+  { filter_upwards [Icc_mem_nhds_within_Ici ⟨le_rfl, neg_lt_self (@zero_lt_one ℝ _ _)⟩],
+    exact λ x, sin_arcsin' },
+  have := h.has_deriv_within_at.sin.congr_of_eventually_eq this.symm (by simp),
+  simpa using (unique_diff_on_Ici _ _ left_mem_Ici).eq_deriv _ this (has_deriv_within_at_id _ _)
+end
+
+lemma differentiable_within_at_arcsin_Iic {x : ℝ} :
+  differentiable_within_at ℝ arcsin (Iic x) x ↔ x ≠ 1 :=
+begin
+  refine ⟨λ h, _, λ h, (has_deriv_within_at_arcsin_Iic h).differentiable_within_at⟩,
+  rw [← neg_neg x, ← image_neg_Ici] at h,
+  have := (h.comp (-x) differentiable_within_at_id.neg (maps_to_image _ _)).neg,
+  simpa [(∘), differentiable_within_at_arcsin_Ici] using this
+end
+
+lemma differentiable_at_arcsin {x : ℝ} :
+  differentiable_at ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1 :=
+⟨λ h, ⟨differentiable_within_at_arcsin_Ici.1 h.differentiable_within_at,
+  differentiable_within_at_arcsin_Iic.1 h.differentiable_within_at⟩,
+  λ h, (has_deriv_at_arcsin h.1 h.2).differentiable_at⟩
+
+@[simp] lemma deriv_arcsin : deriv arcsin = λ x, 1 / sqrt (1 - x ^ 2) :=
+begin
+  funext x,
+  by_cases h : x ≠ -1 ∧ x ≠ 1,
+  { exact (has_deriv_at_arcsin h.1 h.2).deriv },
+  { rw [deriv_zero_of_not_differentiable_at (mt differentiable_at_arcsin.1 h)],
+    simp only [not_and_distrib, ne.def, not_not] at h,
+    rcases h with (rfl|rfl); simp }
+end
+
+lemma differentiable_on_arcsin : differentiable_on ℝ arcsin {-1, 1}ᶜ :=
+λ x hx, (differentiable_at_arcsin.2
+  ⟨λ h, hx (or.inl h), λ h, hx (or.inr h)⟩).differentiable_within_at
+
+lemma times_cont_diff_on_arcsin {n : with_top ℕ} :
+  times_cont_diff_on ℝ n arcsin {-1, 1}ᶜ :=
+λ x hx, (times_cont_diff_at_arcsin (mt or.inl hx) (mt or.inr hx)).times_cont_diff_within_at
+
+lemma times_cont_diff_at_arcsin_iff {x : ℝ} {n : with_top ℕ} :
+  times_cont_diff_at ℝ n arcsin x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) :=
+⟨λ h, or_iff_not_imp_left.2 $ λ hn, differentiable_at_arcsin.1 $ h.differentiable_at $
+  with_top.one_le_iff_pos.2 (pos_iff_ne_zero.2 hn),
+  λ h, h.elim (λ hn, hn.symm ▸ (times_cont_diff_zero.2 continuous_arcsin).times_cont_diff_at) $
+    λ hx, times_cont_diff_at_arcsin hx.1 hx.2⟩
+
+end arcsin
+
+section arccos
+
+lemma has_strict_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
+  has_strict_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x :=
+(has_strict_deriv_at_arcsin h₁ h₂).const_sub (π / 2)
+
+lemma has_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
+  has_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x :=
+(has_deriv_at_arcsin h₁ h₂).const_sub (π / 2)
+
+lemma times_cont_diff_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} :
+  times_cont_diff_at ℝ n arccos x :=
+times_cont_diff_at_const.sub (times_cont_diff_at_arcsin h₁ h₂)
+
+lemma has_deriv_within_at_arccos_Ici {x : ℝ} (h : x ≠ -1) :
+  has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Ici x) x :=
+(has_deriv_within_at_arcsin_Ici h).const_sub _
+
+lemma has_deriv_within_at_arccos_Iic {x : ℝ} (h : x ≠ 1) :
+  has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Iic x) x :=
+(has_deriv_within_at_arcsin_Iic h).const_sub _
+
+lemma differentiable_within_at_arccos_Ici {x : ℝ} :
+  differentiable_within_at ℝ arccos (Ici x) x ↔ x ≠ -1 :=
+(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Ici
+
+lemma differentiable_within_at_arccos_Iic {x : ℝ} :
+  differentiable_within_at ℝ arccos (Iic x) x ↔ x ≠ 1 :=
+(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Iic
+
+lemma differentiable_at_arccos {x : ℝ} :
+  differentiable_at ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1 :=
+(differentiable_at_const_sub_iff _).trans differentiable_at_arcsin
+
+@[simp] lemma deriv_arccos : deriv arccos = λ x, -(1 / sqrt (1 - x ^ 2)) :=
+funext $ λ x, (deriv_const_sub _).trans $ by simp only [deriv_arcsin]
+
+lemma differentiable_on_arccos : differentiable_on ℝ arccos {-1, 1}ᶜ :=
+differentiable_on_arcsin.const_sub _
+
+lemma times_cont_diff_on_arccos {n : with_top ℕ} :
+  times_cont_diff_on ℝ n arccos {-1, 1}ᶜ :=
+times_cont_diff_on_const.sub times_cont_diff_on_arcsin
+
+lemma times_cont_diff_at_arccos_iff {x : ℝ} {n : with_top ℕ} :
+  times_cont_diff_at ℝ n arccos x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) :=
+by refine iff.trans ⟨λ h, _, λ h, _⟩ times_cont_diff_at_arcsin_iff;
+  simpa [arccos] using (@times_cont_diff_at_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h
+
+end arccos
+
+end real

src/data/complex/basic.lean

@@ -198,12 +198,12 @@ instance : star_ring ℂ :=
 @[simp] lemma conj_re (z : ℂ) : (conj z).re = z.re := rfl
 @[simp] lemma conj_im (z : ℂ) : (conj z).im = -z.im := rfl
 
-@[simp] lemma conj_of_real (r : ℝ) : conj (r : ℂ) = r := ext_iff.2 $ by simp [conj]
+lemma conj_of_real (r : ℝ) : conj (r : ℂ) = r := ext_iff.2 $ by simp [conj]
 
 @[simp] lemma conj_I : conj I = -I := ext_iff.2 $ by simp
 
-@[simp] lemma conj_bit0 (z : ℂ) : conj (bit0 z) = bit0 (conj z) := ext_iff.2 $ by simp [bit0]
-@[simp] lemma conj_bit1 (z : ℂ) : conj (bit1 z) = bit1 (conj z) := ext_iff.2 $ by simp [bit0]
+lemma conj_bit0 (z : ℂ) : conj (bit0 z) = bit0 (conj z) := ext_iff.2 $ by simp [bit0]
+lemma conj_bit1 (z : ℂ) : conj (bit1 z) = bit1 (conj z) := ext_iff.2 $ by simp [bit0]
 
 @[simp] lemma conj_neg_I : conj (-I) = I := ext_iff.2 $ by simp