[Merged by Bors] - chore: remove Complex/RCLike bit0/1 lemmas

Mathlib/Analysis/RCLike/Basic.lean

@@ -180,28 +180,12 @@ theorem ofReal_inj {z w : ℝ} : (z : K) = (w : K) ↔ z = w :=
   algebraMap.coe_inj
 #align is_R_or_C.of_real_inj RCLike.ofReal_inj
 
-set_option linter.deprecated false in
-@[deprecated, rclike_simps] -- Porting note (#10618): was `simp` but `simp` can prove it
-theorem bit0_re (z : K) : re (bit0 z) = bit0 (re z) :=
-  map_bit0 _ _
-#align is_R_or_C.bit0_re RCLike.bit0_re
-
-set_option linter.deprecated false in
-@[deprecated, simp, rclike_simps]
-theorem bit1_re (z : K) : re (bit1 z) = bit1 (re z) := by simp only [bit1, map_add, bit0_re, one_re]
-#align is_R_or_C.bit1_re RCLike.bit1_re
-
-set_option linter.deprecated false in
-@[deprecated, rclike_simps] -- Porting note (#10618): was `simp` but `simp` can prove it
-theorem bit0_im (z : K) : im (bit0 z) = bit0 (im z) :=
-  map_bit0 _ _
-#align is_R_or_C.bit0_im RCLike.bit0_im
-
-set_option linter.deprecated false in
-@[deprecated, simp, rclike_simps]
-theorem bit1_im (z : K) : im (bit1 z) = bit0 (im z) := by
-  simp only [bit1, map_add, bit0_im, one_im, add_zero]
-#align is_R_or_C.bit1_im RCLike.bit1_im
+-- replaced by `RCLike.ofNat_re`
+#noalign is_R_or_C.bit0_re
+#noalign is_R_or_C.bit1_re
+-- replaced by `RCLike.ofNat_im`
+#noalign is_R_or_C.bit0_im
+#noalign is_R_or_C.bit1_im
 
 theorem ofReal_eq_zero {x : ℝ} : (x : K) = 0 ↔ x = 0 :=
   algebraMap.lift_map_eq_zero_iff x
@@ -216,17 +200,9 @@ theorem ofReal_add (r s : ℝ) : ((r + s : ℝ) : K) = r + s :=
   algebraMap.coe_add _ _
 #align is_R_or_C.of_real_add RCLike.ofReal_add
 
-set_option linter.deprecated false in
-@[deprecated, simp, rclike_simps, norm_cast]
-theorem ofReal_bit0 (r : ℝ) : ((bit0 r : ℝ) : K) = bit0 (r : K) :=
-  ofReal_add _ _
-#align is_R_or_C.of_real_bit0 RCLike.ofReal_bit0
-
-set_option linter.deprecated false in
-@[deprecated, simp, rclike_simps, norm_cast]
-theorem ofReal_bit1 (r : ℝ) : ((bit1 r : ℝ) : K) = bit1 (r : K) :=
-  map_bit1 (algebraMap ℝ K) r
-#align is_R_or_C.of_real_bit1 RCLike.ofReal_bit1
+-- replaced by `RCLike.ofReal_ofNat`
+#noalign is_R_or_C.of_real_bit0
+#noalign is_R_or_C.of_real_bit1
 
 @[simp, norm_cast, rclike_simps]
 theorem ofReal_neg (r : ℝ) : ((-r : ℝ) : K) = -r :=
@@ -368,17 +344,15 @@ theorem conj_ofReal (r : ℝ) : conj (r : K) = (r : K) := by
   simp only [ofReal_im, conj_im, eq_self_iff_true, conj_re, and_self_iff, neg_zero]
 #align is_R_or_C.conj_of_real RCLike.conj_ofReal
 
-set_option linter.deprecated false in
-@[deprecated, rclike_simps] -- Porting note (#10618): was `simp` but `simp` can prove it
-theorem conj_bit0 (z : K) : conj (bit0 z) = bit0 (conj z) :=
-  map_bit0 _ _
-#align is_R_or_C.conj_bit0 RCLike.conj_bit0
-
-set_option linter.deprecated false in
-@[deprecated, rclike_simps] -- Porting note (#10618): was `simp` but `simp` can prove it
-theorem conj_bit1 (z : K) : conj (bit1 z) = bit1 (conj z) :=
-  map_bit1 _ _
-#align is_R_or_C.conj_bit1 RCLike.conj_bit1
+-- replaced by `RCLike.conj_ofNat`
+#noalign is_R_or_C.conj_bit0
+#noalign is_R_or_C.conj_bit1
+
+theorem conj_nat_cast (n : ℕ) : conj (n : K) = n := map_natCast _ _
+
+-- See note [no_index around OfNat.ofNat]
+theorem conj_ofNat (n : ℕ) [n.AtLeastTwo] : conj (no_index (OfNat.ofNat n : K)) = OfNat.ofNat n :=
+  map_ofNat _ _
 
 @[rclike_simps] -- Porting note (#10618): was a `simp` but `simp` can prove it
 theorem conj_neg_I : conj (-I) = (I : K) := by rw [map_neg, conj_I, neg_neg]

Mathlib/Data/Complex/Basic.lean

@@ -201,44 +201,21 @@ theorem add_im (z w : ℂ) : (z + w).im = z.im + w.im :=
   rfl
 #align complex.add_im Complex.add_im
 
-section
-set_option linter.deprecated false
-@[simp]
-theorem bit0_re (z : ℂ) : (bit0 z).re = bit0 z.re :=
-  rfl
-#align complex.bit0_re Complex.bit0_re
-
-@[simp]
-theorem bit1_re (z : ℂ) : (bit1 z).re = bit1 z.re :=
-  rfl
-#align complex.bit1_re Complex.bit1_re
-
-@[simp]
-theorem bit0_im (z : ℂ) : (bit0 z).im = bit0 z.im :=
-  Eq.refl _
-#align complex.bit0_im Complex.bit0_im
-
-@[simp]
-theorem bit1_im (z : ℂ) : (bit1 z).im = bit0 z.im :=
-  add_zero _
-#align complex.bit1_im Complex.bit1_im
+-- replaced by `re_ofNat`
+#noalign complex.bit0_re
+#noalign complex.bit1_re
+-- replaced by `im_ofNat`
+#noalign complex.bit0_im
+#noalign complex.bit1_im
 
 @[simp, norm_cast]
 theorem ofReal_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s :=
   ext_iff.2 <| by simp [ofReal']
 #align complex.of_real_add Complex.ofReal_add
 
-@[simp, norm_cast]
-theorem ofReal_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 (r : ℂ) :=
-  ext_iff.2 <| by simp [bit0]
-#align complex.of_real_bit0 Complex.ofReal_bit0
-
-@[simp, norm_cast]
-theorem ofReal_bit1 (r : ℝ) : ((bit1 r : ℝ) : ℂ) = bit1 (r : ℂ) :=
-  ext_iff.2 <| by simp [bit1]
-#align complex.of_real_bit1 Complex.ofReal_bit1
-
-end
+-- replaced by `Complex.ofReal_ofNat`
+#noalign complex.of_real_bit0
+#noalign complex.of_real_bit1
 
 instance : Neg ℂ :=
   ⟨fun z => ⟨-z.re, -z.im⟩⟩
@@ -556,17 +533,15 @@ theorem conj_I : conj I = -I :=
   set_option linter.uppercaseLean3 false in
 #align complex.conj_I Complex.conj_I
 
+#noalign complex.conj_bit0
+#noalign complex.conj_bit1
 
-section
-set_option linter.deprecated false
-theorem conj_bit0 (z : ℂ) : conj (bit0 z) = bit0 (conj z) :=
-  ext_iff.2 <| by simp [bit0]
-#align complex.conj_bit0 Complex.conj_bit0
+theorem conj_nat_cast (n : ℕ) : conj (n : ℂ) = n := map_natCast _ _
+
+-- See note [no_index around OfNat.ofNat]
+theorem conj_ofNat (n : ℕ) [n.AtLeastTwo] : conj (no_index (OfNat.ofNat n : ℂ)) = OfNat.ofNat n :=
+  map_ofNat _ _
 
-theorem conj_bit1 (z : ℂ) : conj (bit1 z) = bit1 (conj z) :=
-  ext_iff.2 <| by simp [bit0]
-#align complex.conj_bit1 Complex.conj_bit1
-end
 -- @[simp]
 /- Porting note (#11119): `simp` attribute removed as the result could be proved
 by `simp only [@map_neg, Complex.conj_i, @neg_neg]`