refactor: remove @[simp] from Pi.natCast_def and Pi.intCast_def (#23430)

These lemmas prevented general simp lemmas about rings applying to the product ring.

Also adds `@[simp]` to a lemma that previously was not simp-normal but now is.

Author: eric-wieser

Mathlib/Data/Int/Cast/Pi.lean

@@ -26,15 +26,16 @@ variable {ι : Type*} {π : ι → Type*} [∀ i, IntCast (π i)]
 
 instance instIntCast : IntCast (∀ i, π i) where intCast n _ := n
 
+@[simp]
 theorem intCast_apply (n : ℤ) (i : ι) : (n : ∀ i, π i) i = n :=
   rfl
 
-@[simp]
 theorem intCast_def (n : ℤ) : (n : ∀ i, π i) = fun _ => ↑n :=
   rfl
 
 end Pi
 
+@[simp]
 theorem Sum.elim_intCast_intCast {α β γ : Type*} [IntCast γ] (n : ℤ) :
     Sum.elim (n : α → γ) (n : β → γ) = n :=
   Sum.elim_lam_const_lam_const (γ := γ) n

Mathlib/Data/Nat/Cast/Basic.lean

@@ -186,10 +186,10 @@ variable [∀ a, NatCast (π a)]
 
 instance instNatCast : NatCast (∀ a, π a) where natCast n _ := n
 
+@[simp]
 theorem natCast_apply (n : ℕ) (a : α) : (n : ∀ a, π a) a = n :=
   rfl
 
-@[simp]
 theorem natCast_def (n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n :=
   rfl
 

Mathlib/RingTheory/WittVector/Basic.lean

@@ -174,8 +174,7 @@ private theorem ghostFun_add : ghostFun (x + y) = ghostFun x + ghostFun y := by
 
 private theorem ghostFun_natCast (i : ℕ) : ghostFun (i : 𝕎 R) = i :=
   show ghostFun i.unaryCast = _ by
-    induction i <;>
-      simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.natCast_def]
+    induction i <;> simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add]
 
 private theorem ghostFun_sub : ghostFun (x - y) = ghostFun x - ghostFun y := by
   ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]
@@ -187,8 +186,7 @@ private theorem ghostFun_neg : ghostFun (-x) = -ghostFun x := by ghost_fun_tac -
 
 private theorem ghostFun_intCast (i : ℤ) : ghostFun (i : 𝕎 R) = i :=
   show ghostFun i.castDef = _ by
-    cases i <;> simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg, -Pi.natCast_def,
-      -Pi.intCast_def]
+    cases i <;> simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg]
 
 private lemma ghostFun_nsmul (m : ℕ) (x : WittVector p R) : ghostFun (m • x) = m • ghostFun x := by
   ghost_fun_tac m • (X 0), ![x.coeff]