From f889a384b66e61c87e2e67309671170937068e84 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 25 Nov 2024 23:10:25 -0500 Subject: [PATCH] refactor: add `_self` --- src/Init/Data/Nat/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index c9bcfccc6256..8d55ec055552 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -851,11 +851,11 @@ protected theorem lt_pow_self {n a : Nat} (h : 1 < a) : n < a ^ n := by | zero => exact Nat.zero_lt_one | succ _ ih => exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ih 1) (Nat.pow_lt_pow_succ h) -protected theorem lt_two_pow : n < 2 ^ n := +protected theorem lt_two_pow_self : n < 2 ^ n := Nat.lt_pow_self Nat.one_lt_two @[simp] -protected theorem mod_two_pow : n % 2 ^ n = n := +protected theorem mod_two_pow_self : n % 2 ^ n = n := Nat.mod_eq_of_lt Nat.lt_two_pow @[simp]