chore: bump for std4#314

Mathlib/Algebra/Ring/Defs.lean

@@ -175,7 +175,7 @@ variable [NonAssocSemiring α]
 
 -- Porting note: was [has_add α] [mul_one_class α] [right_distrib_class α]
 theorem two_mul (n : α) : 2 * n = n + n :=
-  (congrArg₂ _ one_add_one_eq_two.symm rfl).trans <| (right_distrib 1 1 n).trans (by rw [one_mul])
+  (congr_arg₂ _ one_add_one_eq_two.symm rfl).trans <| (right_distrib 1 1 n).trans (by rw [one_mul])
 #align two_mul two_mul
 
 -- Porting note: was [has_add α] [mul_one_class α] [right_distrib_class α]
@@ -186,7 +186,7 @@ theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
 
 -- Porting note: was [has_add α] [mul_one_class α] [left_distrib_class α]
 theorem mul_two (n : α) : n * 2 = n + n :=
-  (congrArg₂ _ rfl one_add_one_eq_two.symm).trans <| (left_distrib n 1 1).trans (by rw [mul_one])
+  (congr_arg₂ _ rfl one_add_one_eq_two.symm).trans <| (left_distrib n 1 1).trans (by rw [mul_one])
 #align mul_two mul_two
 
 end NonAssocSemiring

Mathlib/Computability/PartrecCode.lean

@@ -159,6 +159,7 @@ def ofNatCode : ℕ → Code
     | false, true  => comp (ofNatCode m.unpair.1) (ofNatCode m.unpair.2)
     | true , false => prec (ofNatCode m.unpair.1) (ofNatCode m.unpair.2)
     | true , true  => rfind' (ofNatCode m)
+decreasing_by simp_wf; simp [hm, _m1, _m2]
 #align nat.partrec.code.of_nat_code Nat.Partrec.Code.ofNatCode
 
 /-- Proof that `Nat.Partrec.Code.ofNatCode` is the inverse of `Nat.Partrec.Code.encodeCode`-/
@@ -183,6 +184,7 @@ private theorem encode_ofNatCode : ∀ n, encodeCode (ofNatCode n) = n
     simp only [ofNatCode._eq_5]
     cases n.bodd <;> cases n.div2.bodd <;>
       simp [encodeCode, ofNatCode, IH, IH1, IH2, Nat.bit_val]
+decreasing_by simp_wf; simp [hm, _m1, _m2]
 
 instance instDenumerable : Denumerable Code :=
   mk'

Mathlib/Computability/Primrec.lean

@@ -948,7 +948,7 @@ instance sum : Primcodable (Sum α β) :=
                 to₂ <| nat_double.comp (Primrec.encode.comp snd)))).of_eq
         fun n =>
         show _ = encode (decodeSum n) by
-          simp only [decodeSum, Nat.boddDiv2_eq]
+          simp only [decodeSum]
           cases Nat.bodd n <;> simp [decodeSum]
           · cases @decode α _ n.div2 <;> rfl
           · cases @decode β _ n.div2 <;> rfl⟩

Mathlib/Data/Bool/Basic.lean

@@ -225,8 +225,6 @@ theorem eq_false_of_not_eq_true' {a : Bool} : !a = true → a = false := by
 #align bool.bor_bnot_self Bool.or_not_self
 #align bool.bnot_bor_self Bool.not_or_self
 
-theorem bne_eq_xor : bne = xor := by funext a b; revert a b; decide
-
 #align bool.bxor_comm Bool.xor_comm
 
 attribute [simp] xor_assoc

Mathlib/Data/Int/Bitwise.lean

@@ -95,18 +95,16 @@ theorem bodd_mul (m n : ℤ) : bodd (m * n) = (bodd m && bodd n) := by
 -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.xor_comm]`
 #align int.bodd_mul Int.bodd_mul
 
-theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
+theorem div2_add_bodd : ∀ n, 2 * div2 n + cond (bodd n) 1 0 = n
   | (n : ℕ) => by
     rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
-    exact congr_arg ofNat n.bodd_add_div2
+    exact congr_arg ofNat n.div2_add_bodd
   | -[n+1] => by
-    refine' Eq.trans _ (congr_arg negSucc n.bodd_add_div2)
+    refine' Eq.trans _ (congr_arg negSucc n.div2_add_bodd)
     dsimp [bodd]; cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]
-    · change -[2 * Nat.div2 n+1] = _
-      rw [zero_add]
-    · rw [zero_add, add_comm]
-      rfl
-#align int.bodd_add_div2 Int.bodd_add_div2
+    · rfl
+    · rw [add_zero]; rfl
+#align int.bodd_add_div2 Int.div2_add_boddₓ
 
 theorem div2_val : ∀ n, div2 n = n / 2
   | (n : ℕ) => congr_arg ofNat n.div2_val
@@ -134,7 +132,7 @@ theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
 #align int.bit_val Int.bit_val
 
 theorem bit_decomp (n : ℤ) : bit (bodd n) (div2 n) = n :=
-  (bit_val _ _).trans <| (add_comm _ _).trans <| bodd_add_div2 _
+  (bit_val _ _).trans <| div2_add_bodd _
 #align int.bit_decomp Int.bit_decomp
 
 /-- Defines a function from `ℤ` conditionally, if it is defined for odd and even integers separately

Mathlib/Data/Nat/Bits.lean

@@ -32,14 +32,9 @@ universe u
 
 variable {n : ℕ}
 
-/-! ### `boddDiv2_eq` and `bodd` -/
+/-! ### `div2` and `bodd` -/
 
 
-@[simp]
-theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := by
-  unfold bodd div2; cases boddDiv2 n; rfl
-#align nat.bodd_div2_eq Nat.boddDiv2_eq
-
 @[simp]
 theorem bodd_bit0 (n) : bodd (bit0 n) = false :=
   bodd_bit false n
@@ -152,59 +147,9 @@ protected theorem bit0_eq_zero {n : ℕ} : bit0 n = 0 ↔ n = 0 :=
   ⟨Nat.eq_zero_of_add_eq_zero_left, fun h => by simp [h]⟩
 #align nat.bit0_eq_zero Nat.bit0_eq_zero
 
-theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
-  constructor
-  · cases b <;> simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
-  · rintro ⟨rfl, rfl⟩
-    rfl
 #align nat.bit_eq_zero_iff Nat.bit_eq_zero_iff
-
-/--
-The same as `binaryRec_eq`,
-but that one unfortunately requires `f` to be the identity when appending `false` to `0`.
-Here, we allow you to explicitly say that that case is not happening,
-i.e. supplying `n = 0 → b = true`. -/
-theorem binaryRec_eq' {C : ℕ → Sort*} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
-    (h : f false 0 z = z ∨ (n = 0 → b = true)) :
-    binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
-  rw [binaryRec]
-  split_ifs with h'
-  · rcases bit_eq_zero_iff.mp h' with ⟨rfl, rfl⟩
-    rw [binaryRec_zero]
-    simp only [imp_false, or_false_iff, eq_self_iff_true, not_true] at h
-    exact h.symm
-  · dsimp only []
-    -- Porting note: this line was `generalize_proofs e`:
-    generalize @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
-      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) = e
-    revert e
-    rw [bodd_bit, div2_bit]
-    intros
-    rfl
-#align nat.binary_rec_eq' Nat.binaryRec_eq'
-
-/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
-  the bit being appended is `true`-/
-@[elab_as_elim]
-def binaryRec' {C : ℕ → Sort*} (z : C 0) (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) :
-    ∀ n, C n :=
-  binaryRec z fun b n ih =>
-    if h : n = 0 → b = true then f b n h ih
-    else by
-      convert z
-      rw [bit_eq_zero_iff]
-      simpa using h
+#align nat.binary_rec_eq' Nat.binaryRec_eq
 #align nat.binary_rec' Nat.binaryRec'
-
-/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
-@[elab_as_elim]
-def binaryRecFromOne {C : ℕ → Sort*} (z₀ : C 0) (z₁ : C 1) (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) :
-    ∀ n, C n :=
-  binaryRec' z₀ fun b n h ih =>
-    if h' : n = 0 then by
-      rw [h', h h']
-      exact z₁
-    else f b n h' ih
 #align nat.binary_rec_from_one Nat.binaryRecFromOne
 
 @[simp]
@@ -214,7 +159,7 @@ theorem zero_bits : bits 0 = [] := by simp [Nat.bits]
 @[simp]
 theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
     (bit b n).bits = b :: n.bits := by
-  rw [Nat.bits, binaryRec_eq']
+  rw [Nat.bits, Nat.bits, binaryRec_eq]
   simpa
 #align nat.bits_append_bit Nat.bits_append_bit
 

Mathlib/Data/Nat/Bitwise.lean

@@ -44,21 +44,8 @@ set_option linter.deprecated false
 section
 variable {f : Bool → Bool → Bool}
 
-@[simp]
-lemma bitwise_zero_left (m : Nat) : bitwise f 0 m = if f false true then m else 0 :=
-  rfl
 #align nat.bitwise_zero_left Nat.bitwise_zero_left
-
-@[simp]
-lemma bitwise_zero_right (n : Nat) : bitwise f n 0 = if f true false then n else 0 := by
-  unfold bitwise
-  simp only [ite_self, decide_False, Nat.zero_div, ite_true, ite_eq_right_iff]
-  rintro ⟨⟩
-  split_ifs <;> rfl
 #align nat.bitwise_zero_right Nat.bitwise_zero_right
-
-lemma bitwise_zero : bitwise f 0 0 = 0 := by
-  simp only [bitwise_zero_right, ite_self]
 #align nat.bitwise_zero Nat.bitwise_zero
 
 lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
@@ -67,15 +54,6 @@ lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
   have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
     simp [mod_two_of_bodd, cond]; cases bodd x <;> rfl
   simp only [hn, hm, mod_two_iff_bod, ite_false, bit, bit1, bit0, Bool.cond_eq_ite]
-  split_ifs <;> rfl
-
-theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
-    (h : n ≠ 0) :
-    binaryRec z f n = bit_decomp n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n)) := by
-  rw [Eq.rec_eq_cast]
-  rw [binaryRec]
-  dsimp only
-  rw [dif_neg h, eq_mpr_eq_cast]
 
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
@@ -177,7 +155,6 @@ lemma bitwise_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool)
   simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit, ne_eq,
     ite_false]
   conv_rhs => simp only [bit, bit1, bit0, Bool.cond_eq_ite]
-  split_ifs with hf <;> rfl
 
 lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
     bitwise f =
@@ -211,9 +188,7 @@ theorem testBit_eq_false_of_lt {n i} (h : n < 2 ^ i) : n.testBit i = false := by
 /-- The ith bit is the ith element of `n.bits`. -/
 theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i := by
   induction' i with i ih generalizing n
-  · simp only [testBit, zero_eq, shiftRight_zero, and_one_is_mod, mod_two_of_bodd,
-      bodd_eq_bits_head, List.getI_zero_eq_headI]
-    cases List.headI (bits n) <;> rfl
+  · simp [testBit, bodd_eq_bits_head, List.getI_zero_eq_headI]
   conv_lhs => rw [← bit_decomp n]
   rw [testBit_succ, ih n.div2, div2_bits_eq_tail]
   cases n.bits <;> simp
@@ -272,20 +247,19 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
 
 @[simp]
 theorem testBit_two_pow_self (n : ℕ) : testBit (2 ^ n) n = true := by
-  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n)]
-  simp
+  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n), bodd_one]
 #align nat.test_bit_two_pow_self Nat.testBit_two_pow_self
 
 theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = false := by
   rw [testBit, shiftRight_eq_div_pow]
   cases' hm.lt_or_lt with hm hm
-  · rw [Nat.div_eq_of_lt]
-    · simp
-    · exact pow_lt_pow_right one_lt_two hm
+  · rw [Nat.div_eq_of_lt, bodd_zero]
+    exact pow_lt_pow_right one_lt_two hm
   · rw [pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)]
     -- Porting note: XXX why does this make it work?
     rw [(rfl : succ 0 = 1)]
-    simp [pow_succ, and_one_is_mod, mul_mod_left]
+    simp only [pow_succ, bodd_mul, Bool.and_eq_false_eq_eq_false_or_eq_false]
+    exact Or.inr rfl
 #align nat.test_bit_two_pow_of_ne Nat.testBit_two_pow_of_ne
 
 theorem testBit_two_pow (n m : ℕ) : testBit (2 ^ n) m = (n = m) := by
@@ -327,7 +301,7 @@ theorem land_comm (n m : ℕ) : n &&& m = m &&& n :=
 #align nat.land_comm Nat.land_comm
 
 theorem xor_comm (n m : ℕ) : n ^^^ m = m ^^^ n :=
-  bitwise_comm (Bool.bne_eq_xor ▸ Bool.xor_comm) n m
+  bitwise_comm Bool.xor_comm n m
 #align nat.lxor_comm Nat.xor_comm
 
 lemma and_two_pow (n i : ℕ) : n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i := by

Mathlib/Data/Nat/Digits.lean

@@ -597,9 +597,9 @@ theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1
   rw [bits_append_bit _ _ fun hn => absurd hn h]
   cases b
   · rw [digits_def' one_lt_two]
-    · simpa [Nat.bit, Nat.bit0_val n]
+    · simpa [bit_false, bit0_val n]
     · simpa [pos_iff_ne_zero, bit_eq_zero_iff]
-  · simpa [Nat.bit, Nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
+  · simpa [bit_true, bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
 #align nat.digits_two_eq_bits Nat.digits_two_eq_bits
 
 /-! ### Modular Arithmetic -/

Mathlib/Data/Nat/EvenOddRec.lean

@@ -40,7 +40,7 @@ theorem evenOddRec_even (n : ℕ) (P : ℕ → Sort*) (h0 : P 0) (h_even : ∀ i
     @evenOddRec _ h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n) :=
   have : ∀ a, bit false n = a →
       HEq (@evenOddRec _ h0 h_even h_odd a) (h_even n (evenOddRec h0 h_even h_odd n))
-    | _, rfl => by rw [evenOddRec, binaryRec_eq]; apply eq_rec_heq; exact H
+    | _, rfl => by rw [evenOddRec, binaryRec_eq]; apply eq_rec_heq; exact .inl H
   eq_of_heq (this _ (bit0_val _))
 #align nat.even_odd_rec_even Nat.evenOddRec_even
 
@@ -50,7 +50,7 @@ theorem evenOddRec_odd (n : ℕ) (P : ℕ → Sort*) (h0 : P 0) (h_even : ∀ i,
     @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) :=
   have : ∀ a, bit true n = a →
       HEq (@evenOddRec _ h0 h_even h_odd a) (h_odd n (evenOddRec h0 h_even h_odd n))
-    | _, rfl => by rw [evenOddRec, binaryRec_eq]; apply eq_rec_heq; exact H
+    | _, rfl => by rw [evenOddRec, binaryRec_eq]; apply eq_rec_heq; exact .inl H
   eq_of_heq (this _ (bit1_val _))
 #align nat.even_odd_rec_odd Nat.evenOddRec_odd
 

Mathlib/Data/Nat/Fib/Basic.lean

@@ -252,15 +252,13 @@ theorem fast_fib_aux_bit_tt (n : ℕ) :
 #align nat.fast_fib_aux_bit_tt Nat.fast_fib_aux_bit_tt
 
 theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1)) := by
-  apply Nat.binaryRec _ (fun b n' ih => _) n
-  · simp [fastFibAux]
-  · intro b
-    intro n'
-    intro ih
+  induction n using Nat.binaryRec with
+  | z => simp [fastFibAux]
+  | f b n' ih =>
     cases b <;>
           simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih,
             congr_arg Prod.snd ih, Prod.mk.inj_iff] <;>
-          simp [bit, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
+          simp [bit_false, bit_true, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
 #align nat.fast_fib_aux_eq Nat.fast_fib_aux_eq
 
 theorem fast_fib_eq (n : ℕ) : fastFib n = fib n := by rw [fastFib, fast_fib_aux_eq]

Mathlib/Data/Nat/Multiplicity.lean

@@ -307,7 +307,7 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
     cases b
     · simpa [bit0_eq_two_mul n]
     · suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
-        simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0,
+        simpa [multiplicity.mul, h2, ← two_mul, Nat.bit1_eq_succ_bit0,
           bit0_eq_two_mul n, factorial]
       rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
       refine' this.trans _

Mathlib/Data/Nat/Order/Basic.lean

@@ -485,11 +485,6 @@ theorem sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by
     @add_tsub_cancel_left, ← mul_tsub k, Nat.mul_mod_right]
 #align nat.sub_mod_eq_zero_of_mod_eq Nat.sub_mod_eq_zero_of_mod_eq
 
-@[simp]
-theorem one_mod (n : ℕ) : 1 % (n + 2) = 1 :=
-  Nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1)
-#align nat.one_mod Nat.one_mod
-
 theorem one_mod_of_ne_one : ∀ {n : ℕ}, n ≠ 1 → 1 % n = 1
   | 0, _ | (n + 2), _ => by simp
 

Mathlib/Data/Nat/Parity.lean

@@ -24,14 +24,7 @@ namespace Nat
 
 variable {m n : ℕ}
 
-@[simp]
-theorem mod_two_ne_one : ¬n % 2 = 1 ↔ n % 2 = 0 := by
-  cases' mod_two_eq_zero_or_one n with h h <;> simp [h]
 #align nat.mod_two_ne_one Nat.mod_two_ne_one
-
-@[simp]
-theorem mod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by
-  cases' mod_two_eq_zero_or_one n with h h <;> simp [h]
 #align nat.mod_two_ne_zero Nat.mod_two_ne_zero
 
 theorem even_iff : Even n ↔ n % 2 = 0 :=
@@ -95,14 +88,7 @@ theorem mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (
     rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]
 #align nat.mod_two_add_add_odd_mod_two Nat.mod_two_add_add_odd_mod_two
 
-@[simp]
-theorem mod_two_add_succ_mod_two (m : ℕ) : m % 2 + (m + 1) % 2 = 1 :=
-  mod_two_add_add_odd_mod_two m odd_one
 #align nat.mod_two_add_succ_mod_two Nat.mod_two_add_succ_mod_two
-
-@[simp]
-theorem succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1 := by
-  rw [add_comm, mod_two_add_succ_mod_two]
 #align nat.succ_mod_two_add_mod_two Nat.succ_mod_two_add_mod_two
 
 @[simp] theorem not_even_one : ¬Even 1 := odd_iff_not_even.1 odd_one