chore(NumberTheory/EllipticDivisibilitySequence): simplify proofs and deprecate lemmas (leanprover-community#24964)

Simplify proofs with terminal `rw`s to terminal `simp`s and deprecate `even/odd_ofNat` lemmas.

Author: Multramate

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

@@ -95,12 +95,6 @@ open scoped Polynomial.Bivariate
 local macro "C_simp" : tactic =>
   `(tactic| simp only [map_ofNat, C_0, C_1, C_neg, C_add, C_sub, C_mul, C_pow])
 
-local macro "map_simp" : tactic =>
-  `(tactic| simp only [map_ofNat, map_neg, map_add, map_sub, map_mul, map_pow, map_div₀,
-    Polynomial.map_ofNat, Polynomial.map_one, map_C, map_X, Polynomial.map_neg, Polynomial.map_add,
-    Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_div, coe_mapRingHom,
-    apply_ite <| mapRingHom _, WeierstrassCurve.map])
-
 universe r s u v
 
 namespace WeierstrassCurve
@@ -125,10 +119,10 @@ lemma C_Ψ₂Sq : C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial := by
   ring1
 
 lemma ψ₂_sq : W.ψ₂ ^ 2 = C W.Ψ₂Sq + 4 * W.toAffine.polynomial := by
-  rw [C_Ψ₂Sq, sub_add_cancel]
+  simp [C_Ψ₂Sq]
 
 lemma Affine.CoordinateRing.mk_ψ₂_sq : mk W W.ψ₂ ^ 2 = mk W (C W.Ψ₂Sq) := by
-  rw [C_Ψ₂Sq, map_sub, map_mul, AdjoinRoot.mk_self, mul_zero, sub_zero, map_pow]
+  simp [C_Ψ₂Sq]
 
 -- TODO: remove `twoTorsionPolynomial` in favour of `Ψ₂Sq`
 lemma Ψ₂Sq_eq : W.Ψ₂Sq = W.twoTorsionPolynomial.toPoly :=
@@ -220,16 +214,6 @@ lemma preΨ_three : W.preΨ 3 = W.Ψ₃ :=
 lemma preΨ_four : W.preΨ 4 = W.preΨ₄ :=
   preNormEDS_four ..
 
-lemma preΨ_even_ofNat (m : ℕ) : W.preΨ (2 * (m + 3)) =
-    W.preΨ (m + 2) ^ 2 * W.preΨ (m + 3) * W.preΨ (m + 5) -
-      W.preΨ (m + 1) * W.preΨ (m + 3) * W.preΨ (m + 4) ^ 2 :=
-  preNormEDS_even_ofNat ..
-
-lemma preΨ_odd_ofNat (m : ℕ) : W.preΨ (2 * (m + 2) + 1) =
-    W.preΨ (m + 4) * W.preΨ (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
-      W.preΨ (m + 1) * W.preΨ (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
-  preNormEDS_odd_ofNat ..
-
 @[simp]
 lemma preΨ_neg (n : ℤ) : W.preΨ (-n) = -W.preΨ n :=
   preNormEDS_neg ..
@@ -239,11 +223,15 @@ lemma preΨ_even (m : ℤ) : W.preΨ (2 * m) =
       W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2 :=
   preNormEDS_even ..
 
+@[deprecated (since := "2025-05-15")] alias preΨ_even_ofNat := preΨ_even
+
 lemma preΨ_odd (m : ℤ) : W.preΨ (2 * m + 1) =
     W.preΨ (m + 2) * W.preΨ m ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
       W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
   preNormEDS_odd ..
 
+@[deprecated (since := "2025-05-15")] alias preΨ_odd_ofNat := preΨ_odd
+
 end preΨ
 
 section ΨSq
@@ -256,52 +244,46 @@ noncomputable def ΨSq (n : ℤ) : R[X] :=
 
 @[simp]
 lemma ΨSq_ofNat (n : ℕ) : W.ΨSq n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1 := by
-  simp only [ΨSq, preΨ_ofNat, Int.even_coe_nat]
+  simp [ΨSq]
 
 @[simp]
 lemma ΨSq_zero : W.ΨSq 0 = 0 := by
-  rw [← Nat.cast_zero, ΨSq_ofNat, preΨ'_zero, zero_pow two_ne_zero, zero_mul]
+  simp [ΨSq]
 
 @[simp]
 lemma ΨSq_one : W.ΨSq 1 = 1 := by
-  rw [← Nat.cast_one, ΨSq_ofNat, preΨ'_one, one_pow, one_mul, if_neg Nat.not_even_one]
+  simp [ΨSq]
 
 @[simp]
 lemma ΨSq_two : W.ΨSq 2 = W.Ψ₂Sq := by
-  rw [← Nat.cast_two, ΨSq_ofNat, preΨ'_two, one_pow, one_mul, if_pos even_two]
+  simp [ΨSq]
 
 @[simp]
 lemma ΨSq_three : W.ΨSq 3 = W.Ψ₃ ^ 2 := by
-  rw [← Nat.cast_three, ΨSq_ofNat, preΨ'_three, if_neg <| by decide, mul_one]
+  simp [ΨSq, show ¬Even (3 : ℤ) by decide]
 
 @[simp]
 lemma ΨSq_four : W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq := by
-  rw [← Nat.cast_four, ΨSq_ofNat, preΨ'_four, if_pos <| by decide]
-
-lemma ΨSq_even_ofNat (m : ℕ) : W.ΨSq (2 * (m + 3)) =
-    (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
-      W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq := by
-  rw_mod_cast [ΨSq_ofNat, preΨ'_even, if_pos <| even_two_mul _]
-
-lemma ΨSq_odd_ofNat (m : ℕ) : W.ΨSq (2 * (m + 2) + 1) =
-    (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
-      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2 := by
-  rw_mod_cast [ΨSq_ofNat, preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, mul_one]
+  simp [ΨSq, show ¬Odd (4 : ℤ) by decide]
 
 @[simp]
 lemma ΨSq_neg (n : ℤ) : W.ΨSq (-n) = W.ΨSq n := by
-  simp only [ΨSq, preΨ_neg, neg_sq, even_neg]
+  simp [ΨSq]
 
 lemma ΨSq_even (m : ℤ) : W.ΨSq (2 * m) =
     (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) -
       W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq := by
-  rw [ΨSq, preΨ_even, if_pos <| even_two_mul _]
+  rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]
+
+@[deprecated (since := "2025-05-15")] alias ΨSq_even_ofNat := ΨSq_even
 
 lemma ΨSq_odd (m : ℤ) : W.ΨSq (2 * m + 1) =
     (W.preΨ (m + 2) * W.preΨ m ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
       W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2 := by
   rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
 
+@[deprecated (since := "2025-05-15")] alias ΨSq_odd_ofNat := ΨSq_odd
+
 end ΨSq
 
 section Ψ
@@ -316,67 +298,54 @@ open WeierstrassCurve (Ψ)
 
 @[simp]
 lemma Ψ_ofNat (n : ℕ) : W.Ψ n = C (W.preΨ' n) * if Even n then W.ψ₂ else 1 := by
-  simp only [Ψ, preΨ_ofNat, Int.even_coe_nat]
+  simp [Ψ]
 
 @[simp]
 lemma Ψ_zero : W.Ψ 0 = 0 := by
-  rw [← Nat.cast_zero, Ψ_ofNat, preΨ'_zero, C_0, zero_mul]
+  simp [Ψ]
 
 @[simp]
 lemma Ψ_one : W.Ψ 1 = 1 := by
-  rw [← Nat.cast_one, Ψ_ofNat, preΨ'_one, C_1, if_neg Nat.not_even_one, mul_one]
+  simp [Ψ]
 
 @[simp]
 lemma Ψ_two : W.Ψ 2 = W.ψ₂ := by
-  rw [← Nat.cast_two, Ψ_ofNat, preΨ'_two, C_1, one_mul, if_pos even_two]
+  simp [Ψ]
 
 @[simp]
 lemma Ψ_three : W.Ψ 3 = C W.Ψ₃ := by
-  rw [← Nat.cast_three, Ψ_ofNat, preΨ'_three, if_neg <| by decide, mul_one]
+  simp [Ψ, show ¬Even (3 : ℤ) by decide]
 
 @[simp]
 lemma Ψ_four : W.Ψ 4 = C W.preΨ₄ * W.ψ₂ := by
-  rw [← Nat.cast_four, Ψ_ofNat, preΨ'_four, if_pos <| by decide]
-
-lemma Ψ_even_ofNat (m : ℕ) : W.Ψ (2 * (m + 3)) * W.ψ₂ =
-    W.Ψ (m + 2) ^ 2 * W.Ψ (m + 3) * W.Ψ (m + 5) - W.Ψ (m + 1) * W.Ψ (m + 3) * W.Ψ (m + 4) ^ 2 := by
-  repeat rw_mod_cast [Ψ_ofNat]
-  simp_rw [preΨ'_even, if_pos <| even_two_mul _, Nat.even_add_one, ite_not]
-  split_ifs <;> C_simp <;> ring1
-
-lemma Ψ_odd_ofNat (m : ℕ) : W.Ψ (2 * (m + 2) + 1) =
-    W.Ψ (m + 4) * W.Ψ (m + 2) ^ 3 - W.Ψ (m + 1) * W.Ψ (m + 3) ^ 3 +
-      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
-        C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3
-            else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3) := by
-  repeat rw_mod_cast [Ψ_ofNat]
-  simp_rw [preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, Nat.even_add_one, ite_not]
-  split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1
+  simp [Ψ, show ¬Odd (4 : ℤ) by decide]
 
 @[simp]
 lemma Ψ_neg (n : ℤ) : W.Ψ (-n) = -W.Ψ n := by
-  simp only [Ψ, preΨ_neg, C_neg, neg_mul (α := R[X][Y]), even_neg]
+  simp_rw [Ψ, preΨ_neg, C_neg, neg_mul, even_neg]
 
 lemma Ψ_even (m : ℤ) : W.Ψ (2 * m) * W.ψ₂ =
     W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2 := by
-  repeat rw [Ψ]
-  simp_rw [preΨ_even, if_pos <| even_two_mul _, Int.even_add_one, show m + 2 = m + 1 + 1 by ring1,
-    Int.even_add_one, show m - 2 = m - 1 - 1 by ring1, Int.even_sub_one, ite_not]
+  simp_rw [Ψ, preΨ_even, if_pos <| even_two_mul m, Int.even_add, Int.even_sub, even_two, iff_true,
+    Int.not_even_one, iff_false]
   split_ifs <;> C_simp <;> ring1
 
+@[deprecated (since := "2025-05-15")] alias Ψ_even_ofNat := Ψ_even
+
 lemma Ψ_odd (m : ℤ) : W.Ψ (2 * m + 1) =
     W.Ψ (m + 2) * W.Ψ m ^ 3 - W.Ψ (m - 1) * W.Ψ (m + 1) ^ 3 +
       W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
         C (if Even m then W.preΨ (m + 2) * W.preΨ m ^ 3
             else -W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3) := by
-  repeat rw [Ψ]
-  simp_rw [preΨ_odd, if_neg m.not_even_two_mul_add_one, show m + 2 = m + 1 + 1 by ring1,
-    Int.even_add_one, Int.even_sub_one, ite_not]
+  simp_rw [Ψ, preΨ_odd, if_neg m.not_even_two_mul_add_one, Int.even_add, Int.even_sub, even_two,
+    iff_true, Int.not_even_one, iff_false]
   split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1
 
+@[deprecated (since := "2025-05-15")] alias Ψ_odd_ofNat := Ψ_odd
+
 lemma Affine.CoordinateRing.mk_Ψ_sq (n : ℤ) : mk W (W.Ψ n) ^ 2 = mk W (C <| W.ΨSq n) := by
-  simp only [Ψ, ΨSq, map_one, map_mul, map_pow, one_pow, mul_pow, ite_pow, apply_ite C,
-    apply_ite <| mk W, mk_ψ₂_sq]
+  simp_rw [Ψ, ΨSq, map_mul, apply_ite C, apply_ite <| mk W, mul_pow, ite_pow, mk_ψ₂_sq, map_one,
+    one_pow, map_pow]
 
 end Ψ
 
@@ -394,19 +363,17 @@ open WeierstrassCurve (Φ)
 lemma Φ_ofNat (n : ℕ) : W.Φ (n + 1) =
     X * W.preΨ' (n + 1) ^ 2 * (if Even n then 1 else W.Ψ₂Sq) -
       W.preΨ' (n + 2) * W.preΨ' n * (if Even n then W.Ψ₂Sq else 1) := by
-  rw [Φ, ← Nat.cast_one, ← Nat.cast_add, ΨSq_ofNat, ← mul_assoc, ← Nat.cast_add, preΨ_ofNat,
-    Nat.cast_add, add_sub_cancel_right, preΨ_ofNat, ← Nat.cast_add]
-  simp only [Nat.even_add_one, Int.even_add_one, Int.even_coe_nat, ite_not]
+  rw [Φ, add_sub_cancel_right]
+  norm_cast
+  simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]
 
 @[simp]
 lemma Φ_zero : W.Φ 0 = 1 := by
-  rw [Φ, ΨSq_zero, mul_zero, zero_sub, zero_add, preΨ_one, one_mul, zero_sub, preΨ_neg, preΨ_one,
-    neg_one_mul, neg_neg, if_pos Even.zero]
+  simp [Φ]
 
 @[simp]
 lemma Φ_one : W.Φ 1 = X := by
-  rw [show 1 = ((0 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_one, one_pow, mul_one, if_pos Even.zero,
-    mul_one, preΨ'_zero, mul_zero, zero_mul, sub_zero]
+  simp [Φ]
 
 @[simp]
 lemma Φ_two : W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈ := by
@@ -429,8 +396,8 @@ lemma Φ_four : W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄
 
 @[simp]
 lemma Φ_neg (n : ℤ) : W.Φ (-n) = W.Φ n := by
-  simp only [Φ, ΨSq_neg, neg_add_eq_sub, ← neg_sub n, preΨ_neg, ← neg_add', preΨ_neg, neg_mul_neg,
-    mul_comm <| W.preΨ <| n - 1, even_neg]
+  simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
+    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
 
 end Φ
 
@@ -464,14 +431,6 @@ lemma ψ_three : W.ψ 3 = C W.Ψ₃ :=
 lemma ψ_four : W.ψ 4 = C W.preΨ₄ * W.ψ₂ :=
   normEDS_four ..
 
-lemma ψ_even_ofNat (m : ℕ) : W.ψ (2 * (m + 3)) * W.ψ₂ =
-    W.ψ (m + 2) ^ 2 * W.ψ (m + 3) * W.ψ (m + 5) - W.ψ (m + 1) * W.ψ (m + 3) * W.ψ (m + 4) ^ 2 :=
-  normEDS_even_ofNat ..
-
-lemma ψ_odd_ofNat (m : ℕ) : W.ψ (2 * (m + 2) + 1) =
-    W.ψ (m + 4) * W.ψ (m + 2) ^ 3 - W.ψ (m + 1) * W.ψ (m + 3) ^ 3 :=
-  normEDS_odd_ofNat ..
-
 @[simp]
 lemma ψ_neg (n : ℤ) : W.ψ (-n) = -W.ψ n :=
   normEDS_neg ..
@@ -480,12 +439,16 @@ lemma ψ_even (m : ℤ) : W.ψ (2 * m) * W.ψ₂ =
     W.ψ (m - 1) ^ 2 * W.ψ m * W.ψ (m + 2) - W.ψ (m - 2) * W.ψ m * W.ψ (m + 1) ^ 2 :=
   normEDS_even ..
 
+@[deprecated (since := "2025-05-15")] alias ψ_even_ofNat := ψ_even
+
 lemma ψ_odd (m : ℤ) : W.ψ (2 * m + 1) =
     W.ψ (m + 2) * W.ψ m ^ 3 - W.ψ (m - 1) * W.ψ (m + 1) ^ 3 :=
   normEDS_odd ..
 
+@[deprecated (since := "2025-05-15")] alias ψ_odd_ofNat := ψ_odd
+
 lemma Affine.CoordinateRing.mk_ψ (n : ℤ) : mk W (W.ψ n) = mk W (W.Ψ n) := by
-  simp only [ψ, normEDS, Ψ, preΨ, map_mul, map_pow, map_preNormEDS, ← mk_ψ₂_sq, ← pow_mul]
+  simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]
 
 end ψ
 
@@ -501,21 +464,19 @@ open WeierstrassCurve (Ψ Φ φ)
 
 @[simp]
 lemma φ_zero : W.φ 0 = 1 := by
-  rw [φ, ψ_zero, zero_pow two_ne_zero, mul_zero, zero_sub, zero_add, ψ_one, one_mul, zero_sub,
-    ψ_neg, neg_neg, ψ_one]
+  simp [φ]
 
 @[simp]
 lemma φ_one : W.φ 1 = C X := by
-  rw [φ, ψ_one, one_pow, mul_one, sub_self, ψ_zero, mul_zero, sub_zero]
+  simp [φ]
 
 @[simp]
 lemma φ_two : W.φ 2 = C X * W.ψ₂ ^ 2 - C W.Ψ₃ := by
-  rw [φ, ψ_two, two_add_one_eq_three, ψ_three, show (2 - 1 : ℤ) = 1 by rfl, ψ_one, mul_one]
+  simp [φ]
 
 @[simp]
 lemma φ_three : W.φ 3 = C X * C W.Ψ₃ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 2 := by
-  rw [φ, ψ_three, three_add_one_eq_four, ψ_four, mul_assoc, show (3 - 1 : ℤ) = 2 by rfl, ψ_two,
-    ← sq]
+  simp [φ, mul_assoc, sq]
 
 @[simp]
 lemma φ_four :
@@ -527,12 +488,12 @@ lemma φ_four :
 
 @[simp]
 lemma φ_neg (n : ℤ) : W.φ (-n) = W.φ n := by
-  rw [φ, ψ_neg, neg_sq (R := R[X][Y]), neg_add_eq_sub, ← neg_sub n, ψ_neg, ← neg_add', ψ_neg,
-    neg_mul_neg (α := R[X][Y]), mul_comm <| W.ψ _, φ]
+  simp_rw [φ, ψ_neg, neg_sq, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', ψ_neg,
+    neg_mul_neg, mul_comm <| W.ψ <| n - 1]
 
 lemma Affine.CoordinateRing.mk_φ (n : ℤ) : mk W (W.φ n) = mk W (C <| W.Φ n) := by
   simp_rw [φ, Φ, map_sub, map_mul, map_pow, mk_ψ, mk_Ψ_sq, Ψ, map_mul,
-    mul_mul_mul_comm _ <| mk W <| ite .., Int.even_add_one, Int.even_sub_one, ← sq, ite_not,
+    mul_mul_mul_comm _ <| mk W <| ite .., Int.even_add_one, Int.even_sub_one, ite_not, ← sq,
     apply_ite C, apply_ite <| mk W, ite_pow, map_one, one_pow, mk_ψ₂_sq]
 
 end φ
@@ -545,48 +506,52 @@ open WeierstrassCurve (Ψ Φ ψ φ)
 
 variable (f : R →+* S)
 
+@[simp]
 lemma map_ψ₂ : (W.map f).ψ₂ = W.ψ₂.map (mapRingHom f) := by
-  simp only [ψ₂, Affine.map_polynomialY]
+  simp_rw [ψ₂, Affine.map_polynomialY]
 
+@[simp]
 lemma map_Ψ₂Sq : (W.map f).Ψ₂Sq = W.Ψ₂Sq.map f := by
-  simp only [Ψ₂Sq, map_b₂, map_b₄, map_b₆]
-  map_simp
+  simp [Ψ₂Sq, map_ofNat]
 
+@[simp]
 lemma map_Ψ₃ : (W.map f).Ψ₃ = W.Ψ₃.map f := by
-  simp only [Ψ₃, map_b₂, map_b₄, map_b₆, map_b₈]
-  map_simp
+  simp [Ψ₃]
 
+@[simp]
 lemma map_preΨ₄ : (W.map f).preΨ₄ = W.preΨ₄.map f := by
-  simp only [preΨ₄, map_b₂, map_b₄, map_b₆, map_b₈]
-  map_simp
+  simp [preΨ₄]
 
+@[simp]
 lemma map_preΨ' (n : ℕ) : (W.map f).preΨ' n = (W.preΨ' n).map f := by
-  simp only [preΨ', map_Ψ₂Sq, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_preNormEDS']
-  map_simp
+  simp [preΨ', ← coe_mapRingHom]
 
+@[simp]
 lemma map_preΨ (n : ℤ) : (W.map f).preΨ n = (W.preΨ n).map f := by
-  simp only [preΨ, map_Ψ₂Sq, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_preNormEDS]
-  map_simp
+  simp [preΨ, ← coe_mapRingHom]
 
+@[simp]
 lemma map_ΨSq (n : ℤ) : (W.map f).ΨSq n = (W.ΨSq n).map f := by
-  simp only [ΨSq, map_preΨ, map_Ψ₂Sq, ← coe_mapRingHom]
-  map_simp
+  simp [ΨSq, ← coe_mapRingHom, apply_ite <| mapRingHom f]
 
+@[simp]
 lemma map_Ψ (n : ℤ) : (W.map f).Ψ n = (W.Ψ n).map (mapRingHom f) := by
-  simp only [Ψ, map_preΨ, map_ψ₂, ← coe_mapRingHom]
-  map_simp
+  rw [← coe_mapRingHom]
+  simp [Ψ, apply_ite <| mapRingHom _]
 
+@[simp]
 lemma map_Φ (n : ℤ) : (W.map f).Φ n = (W.Φ n).map f := by
-  simp only [Φ, map_ΨSq, map_preΨ, map_Ψ₂Sq, ← coe_mapRingHom]
-  map_simp
+  rw [← coe_mapRingHom]
+  simp [Φ, map_sub, apply_ite <| mapRingHom f]
 
+@[simp]
 lemma map_ψ (n : ℤ) : (W.map f).ψ n = (W.ψ n).map (mapRingHom f) := by
-  simp only [ψ, map_ψ₂, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_normEDS]
-  map_simp
+  rw [← coe_mapRingHom]
+  simp [ψ]
 
+@[simp]
 lemma map_φ (n : ℤ) : (W.map f).φ n = (W.φ n).map (mapRingHom f) := by
-  simp only [φ, map_ψ]
-  map_simp
+  simp [φ]
 
 end Map