chore(analysis/complex/circle): minor review (#11059)

* use implicit arg in `mem_circle_iff_abs`;
* rename `abs_eq_of_mem_circle` to `abs_coe_circle` to reflect the type of LHS;
* add `mem_circle_iff_norm_sq`.

Author: urkud

src/analysis/complex/circle.lean

@@ -45,11 +45,15 @@ def circle : submonoid ℂ :=
     simp [ha, hb],
   end }
 
-@[simp] lemma mem_circle_iff_abs (z : ℂ) : z ∈ circle ↔ abs z = 1 := mem_sphere_zero_iff_norm
+@[simp] lemma mem_circle_iff_abs {z : ℂ} : z ∈ circle ↔ abs z = 1 := mem_sphere_zero_iff_norm
 
-lemma circle_def : ↑circle = {z : ℂ | abs z = 1} := by { ext, simp }
+lemma circle_def : ↑circle = {z : ℂ | abs z = 1} := set.ext $ λ z, mem_circle_iff_abs
 
-@[simp] lemma abs_eq_of_mem_circle (z : circle) : abs z = 1 := by { convert z.2, simp }
+@[simp] lemma abs_coe_circle (z : circle) : abs z = 1 :=
+mem_circle_iff_abs.mp z.2
+
+lemma mem_circle_iff_norm_sq {z : ℂ} : z ∈ circle ↔ norm_sq z = 1 :=
+by rw [mem_circle_iff_abs, complex.abs, real.sqrt_eq_one]
 
 @[simp] lemma norm_sq_eq_of_mem_circle (z : circle) : norm_sq z = 1 := by simp [norm_sq_eq_abs]
 

src/analysis/special_functions/complex/circle.lean

@@ -20,7 +20,7 @@ open_locale real
 namespace circle
 
 lemma injective_arg : injective (λ z : circle, arg z) :=
-λ z w h, subtype.ext $ ext_abs_arg ((abs_eq_of_mem_circle z).trans (abs_eq_of_mem_circle w).symm) h
+λ z w h, subtype.ext $ ext_abs_arg ((abs_coe_circle z).trans (abs_coe_circle w).symm) h
 
 @[simp] lemma arg_eq_arg {z w : circle} : arg z = arg w ↔ z = w := injective_arg.eq_iff