chore(data/nat/factorial): use n + 1 instead of n.succ in nat.factorial_succ (#9645)

Author: urkud

src/data/nat/choose/basic.lean

@@ -93,7 +93,7 @@ lemma choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k * k
 | (n + 1) (succ k) hk :=
 begin
   cases lt_or_eq_of_le hk with hk₁ hk₁,
-  { have h : choose n k * k.succ! * (n-k)! = k.succ * n! :=
+  { have h : choose n k * k.succ! * (n-k)! = (k + 1) * n! :=
       by rw ← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk);
       simp [factorial_succ, mul_comm, mul_left_comm],
     have h₁ : (n - k)! = (n - k) * (n - k.succ)! :=
@@ -102,7 +102,7 @@ begin
       by rw ← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁);
       simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc],
     have h₃ : k * n! ≤ n * n! := nat.mul_le_mul_right _ (le_of_succ_le_succ hk),
-  rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, ← add_one, add_mul,
+    rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul,
       nat.mul_sub_right_distrib, factorial_succ, ← nat.add_sub_assoc h₃, add_assoc, ← add_mul,
       nat.add_sub_cancel_left, add_comm] },
   { simp [hk₁, mul_comm, choose, nat.sub_self] }

src/data/nat/factorial/basic.lean

@@ -35,7 +35,7 @@ variables {m n : ℕ}
 
 @[simp] theorem factorial_zero : 0! = 1 := rfl
 
-@[simp] theorem factorial_succ (n : ℕ) : n.succ! = succ n * n! := rfl
+@[simp] theorem factorial_succ (n : ℕ) : n.succ! = (n + 1) * n! := rfl
 
 @[simp] theorem factorial_one : 1! = 1 := rfl
 
@@ -125,7 +125,7 @@ end
 lemma add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
   i + (n + 1)! < (i + n + 1)! :=
 begin
-  rw [factorial_succ (i + _), succ_eq_add_one, add_mul, one_mul],
+  rw [factorial_succ (i + _), add_mul, one_mul],
   have : i ≤ i + n := le.intro rfl,
   exact add_lt_add_of_lt_of_le (this.trans_lt ((lt_mul_iff_one_lt_right (zero_lt_two.trans_le
     (hi.trans this))).mpr (lt_iff_le_and_ne.mpr ⟨(i + n).factorial_pos, λ g,

src/number_theory/liouville/liouville_constant.lean

@@ -23,7 +23,7 @@ We prove that, for $m \in \mathbb{N}$ satisfying $2 \le m$, Liouville's constant
 is a transcendental number.  Classically, the Liouville number for $m = 2$ is the one called
 ``Liouville's constant''.
 
-# Implementation notes
+## Implementation notes
 
 The indexing $m$ is eventually a natural number satisfying $2 ≤ m$.  However, we prove the first few
 lemmas for $m \in \mathbb{R}$.
@@ -159,7 +159,7 @@ begin
     { norm_cast,
       rw [add_mul, one_mul, nat.factorial_succ,
         show k.succ * k! - k! = (k.succ - 1) * k!, by rw [nat.mul_sub_right_distrib, one_mul],
-        nat.succ_sub_one, nat.succ_eq_add_one, add_mul, one_mul, pow_add],
+        nat.succ_sub_one, add_mul, one_mul, pow_add],
       simp [mul_assoc] },
     refine mul_ne_zero_iff.mpr ⟨_, _⟩,
     all_goals { exact pow_ne_zero _ (nat.cast_ne_zero.mpr hm.ne.symm) } }