chore: rm @[simp] from factorial_succ (#6840)

Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Aug 30, 2023 · e8477a9 · e8477a9
1 parent c83178f
commit e8477a9
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -1596,7 +1596,7 @@ theorem sum_div_factorial_le {α : Type*} [LinearOrderedField α] (n j : ℕ) (h
       · rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
         exact Nat.factorial_mul_pow_le_factorial
     _ = (n.factorial : α)⁻¹ * ∑ m in range (j - n), (n.succ : α)⁻¹ ^ m := by
-      simp [mul_inv, mul_sum.symm, sum_mul.symm, -Nat.factorial_succ, mul_comm, inv_pow]
+      simp [mul_inv, mul_sum.symm, sum_mul.symm, mul_comm, inv_pow]
     _ = ((n.succ : α) - n.succ * (n.succ : α)⁻¹ ^ (j - n)) / (n.factorial * n) := by
       have h₁ : (n.succ : α) ≠ 1 :=
         @Nat.cast_one α _ ▸ mt Nat.cast_inj.1 (mt Nat.succ.inj (pos_iff_ne_zero.1 hn))

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -44,7 +44,6 @@ theorem factorial_zero : 0! = 1 :=
   rfl
 #align nat.factorial_zero Nat.factorial_zero
 
-@[simp]
 theorem factorial_succ (n : ℕ) : n.succ ! = (n + 1) * n ! :=
   rfl
 #align nat.factorial_succ Nat.factorial_succ