@@ -35,7 +35,7 @@ lemma ENat.le_floor_NNReal_iff (x : ENat) (y : ℝ≥0) (hx_ne_top : x ≠ ⊤)
3535 (x : ENat) ≤ ((Nat.floor y) : ENat) ↔ x.toNat ≤ Nat.floor y := by
3636 lift x to ℕ using hx_ne_top
3737 -- y : ℝ≥0, x : ℕ, ⊢ ↑x ≤ ↑⌊y⌋₊ ↔ (↑x).toNat ≤ ⌊y⌋₊
38- simp only [Nat.cast_le , toNat_coe]
38+ simp only [ENat.coe_le_coe , toNat_coe]
3939
4040section ENNReal
4141open ENNReal
@@ -49,29 +49,11 @@ variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0}
4949-- lemma ENNReal.div_lt_div_right (hc₀ : c ≠ 0) (hc : c ≠ ∞) (hab : a < b) : a / c < b / c :=
5050-- (ENNReal.div_lt_div_iff_left hc₀ hc).2 hab
5151
52- theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0 ) (hb : b ≠ 0 ) :
53- ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ := by
54- -- Let x = ↑a and y = ↑b for readability
55- let x : ENNReal := a
56- let y : ENNReal := b
57- -- Prove x and y are non-zero and finite (needed for inv_cancel)
58- have hx_ne_zero : x ≠ 0 := by exact Nat.cast_ne_zero.mpr ha
59- have hy_ne_zero : y ≠ 0 := by exact Nat.cast_ne_zero.mpr hb
60- have hx_ne_top : x ≠ ∞ := by exact ENNReal.natCast_ne_top a
61- have hy_ne_top : y ≠ ∞ := by exact ENNReal.natCast_ne_top b
62- have ha_NNReal_ne0 : (a : ℝ≥0 ) ≠ 0 := by exact Nat.cast_ne_zero.mpr ha
63- have hb_NNReal_ne0 : (b : ℝ≥0 ) ≠ 0 := by exact Nat.cast_ne_zero.mpr hb
64- -- (a * b)⁻¹ = b⁻¹ * a⁻¹
65- have hlhs : ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ℝ≥0 )⁻¹ * (b : ℝ≥0 )⁻¹) := by
66- rw [coe_inv (hr := by exact ha_NNReal_ne0)]
67- rw [coe_inv (hr := by exact hb_NNReal_ne0)]
68- rw [ENNReal.coe_natCast, ENNReal.coe_natCast]
69- have hrhs : ((a : ENNReal) * (b : ENNReal))⁻¹ = ((a : ℝ≥0 ) * (b : ℝ≥0 ))⁻¹ := by
70- rw [coe_inv (hr := (mul_ne_zero_iff_right hb_NNReal_ne0).mpr (ha_NNReal_ne0))]
71- simp only [coe_mul, coe_natCast]
72- rw [hlhs, hrhs]
73- rw [mul_inv_rev (a := (a : ℝ≥0 )) (b := (b : ℝ≥0 ))]
74- rw [coe_mul, mul_comm]
52+ theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0 ) :
53+ ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ :=
54+ (ENNReal.mul_inv
55+ (Or.inl (Nat.cast_ne_zero.mpr ha))
56+ (Or.inl (ENNReal.natCast_ne_top a))).symm
7557
7658lemma ENNReal.coe_le_of_NNRat {a b : ℚ≥0 } : ((a : ENNReal)) ≤ (b) ↔ a ≤ b := by
7759 exact ENNReal.coe_le_coe.trans (by norm_cast)
@@ -367,7 +349,7 @@ lemma getBit_two_pow {i k : ℕ} : (getBit k (2^i) = if i == k then 1 else 0) :=
367349 simp only [Nat.and_one_is_mod, BEq.rfl, ↓reduceIte]
368350 rw [Nat.shiftLeft_shiftRight]
369351 else
370- push_neg at h_i_eq_k
352+ push Not at h_i_eq_k
371353 simp only [beq_iff_eq, h_i_eq_k, ↓reduceIte]
372354 if h_k_lt_i: i < k then
373355 have h_res : (1 <<< i >>> k &&& 1 ) = 0 := by
@@ -390,7 +372,7 @@ lemma getBit_two_pow {i k : ℕ} : (getBit k (2^i) = if i == k then 1 else 0) :=
390372 rw [h_one_div_2_pow_k_sub_i, Nat.zero_and]
391373 rw [h_res]
392374 else
393- push_neg at h_k_lt_i
375+ push Not at h_k_lt_i
394376 have h_res : (1 <<< i >>> k &&& 1 ) = 0 := by
395377 set i_sub_k := i - k with h_i_sub_k
396378 have h_i_sub_k_le_1: i_sub_k ≥ 1 := by omega
@@ -419,7 +401,7 @@ lemma and_two_pow_eq_zero_of_getBit_0 {n i : ℕ} (h_getBit : getBit i n = 0) :
419401 rw [getBit, h_k.symm] at h_getBit
420402 rw [getBit, h_getBit, Nat.zero_and]
421403 else
422- push_neg at h_k
404+ push Not at h_k
423405 simp only [beq_iff_eq, h_k.symm, ↓reduceIte] at h_getBit_two_pow
424406 rw [getBit] at h_getBit_two_pow
425407 rw [getBit, getBit, h_getBit_two_pow]
@@ -448,7 +430,7 @@ lemma and_two_pow_eq_two_pow_of_getBit_eq_one {n i : ℕ} (h_getBit: getBit i n
448430 rw [Nat.shiftRight_and_distrib, Nat.and_assoc, Nat.and_comm (2 ^k >>> k) 1 , ←Nat.and_assoc]
449431 rw [h_getBit, ←one_mul (2 ^k), ←Nat.shiftLeft_eq, Nat.shiftLeft_shiftRight, Nat.and_self]
450432 else
451- push_neg at h_k
433+ push Not at h_k
452434 simp only [beq_iff_eq, h_k.symm, ↓reduceIte] at h_getBit_two_pow
453435 rw [getBit] at h_getBit_two_pow
454436 rw [h_getBit_two_pow, Nat.shiftRight_and_distrib, Nat.and_assoc, h_getBit_two_pow]
@@ -465,9 +447,7 @@ lemma eq_zero_or_eq_one_of_lt_two {n : ℕ} (h_lt : n < 2) : n = 0 ∨ n = 1 :=
465447
466448lemma div_2_form {nD2 b : ℕ} (h_b : b < 2 ) :
467449 (nD2 * 2 + b) / 2 = nD2 := by
468- rw [←add_comm, ←mul_comm]
469- rw [Nat.add_mul_div_left (x := b) (y := 2 ) (z := nD2) (H := by norm_num)]
470- norm_num; exact h_b;
450+ omega
471451
472452lemma and_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2 ) (h_bm : bm < 2 )
473453 (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm) :
@@ -656,7 +636,7 @@ lemma sum_eq_xor_plus_twice_and (n : Nat) : ∀ m : ℕ, n + m = (n ^^^ m) + 2 *
656636 rw [h_and_getBits, mul_comm (a := (n2 &&& m2)) (b := 2 )];
657637 _ = 2 * (nVal &&& mVal) := by rw [h_and];
658638 rw [h_right]
659- · push_neg at h_and_getBitN_getBitM_eq_1;
639+ · push Not at h_and_getBitN_getBitM_eq_1;
660640 have h_and_getBitN_getBitM_eq_0 : (getBitN &&& getBitM) = 0 := by
661641 interval_cases (getBitN &&& getBitM)
662642 · rfl
@@ -895,7 +875,7 @@ lemma getBit_of_sub_two_pow_of_bit_1 {n i j: ℕ} (h_getBit_eq_1: getBit i n = 1
895875 rw [Nat.getBit_two_pow]
896876 simp only [beq_iff_eq]
897877 simp only [h_j_eq_i, ↓reduceIte]
898- push_neg at h_j_eq_i
878+ push Not at h_j_eq_i
899879 simp only [if_neg h_j_eq_i.symm, xor_zero]
900880
901881lemma getBit_of_lowBits {n: ℕ} (numLowBits : ℕ) : ∀ k, getBit k (getLowBits numLowBits n) =
@@ -915,7 +895,7 @@ lemma getBit_of_lowBits {n: ℕ} (numLowBits : ℕ) : ∀ k, getBit k (getLowBit
915895 · simp only [Nat.and_one_is_mod]
916896 · simp only [Nat.and_one_is_mod]
917897 else
918- push_neg at h_k
898+ push Not at h_k
919899 have getBit_k_mask : getBit k (1 <<< numLowBits - 1 ) = 0 := by
920900 rw [Nat.shiftLeft_eq, one_mul]
921901 rw [getBit_of_two_pow_sub_one (i := numLowBits) (k := k)]
@@ -964,7 +944,7 @@ theorem getBit_repr {ℓ : Nat} :
964944 interval_cases j
965945 · simp only [getBit, Nat.shiftRight_zero, Nat.and_one_is_mod, Nat.zero_mod]
966946 · simp only [getBit, Nat.shiftRight_zero, Nat.and_one_is_mod]
967- · push_neg at h_ℓ₁
947+ · push Not at h_ℓ₁
968948 set ℓ := ℓ₁ + 1
969949 have h_ℓ_eq : ℓ = ℓ₁ + 1 := by rfl
970950 intro j h_j
@@ -991,7 +971,7 @@ theorem getBit_repr {ℓ : Nat} :
991971 _ = b + 2 * m := by omega;
992972 have h_m : m < 2 ^ℓ₁ := by
993973 by_contra h_m_ge_2_pow_ℓ
994- push_neg at h_m_ge_2_pow_ℓ
974+ push Not at h_m_ge_2_pow_ℓ
995975 have h_j_ge : j ≥ 2 ^ℓ := by
996976 calc _ = 2 * m + b := by rw [h_j_eq]; omega
997977 _ ≥ 2 * (2 ^ℓ₁) + b := by omega
@@ -1261,7 +1241,7 @@ lemma getBit_of_lt_two_pow {n: ℕ} (a: Fin (2^n)) (k: ℕ) :
12611241lemma exist_bit_diff_if_diff {n: ℕ} (a: Fin (2 ^n)) (b: Fin (2 ^n)) (h_a_ne_b: a ≠ b) :
12621242 ∃ k: Fin n, getBit k a ≠ getBit k b := by
12631243 by_contra h_no_diff
1264- push_neg at h_no_diff
1244+ push Not at h_no_diff
12651245 have h_a_eq_b: a = b := by
12661246 apply Fin.eq_of_val_eq
12671247 apply eq_iff_eq_all_getBits.mpr
@@ -1371,7 +1351,7 @@ lemma getBit_of_binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary: ∀ j
13711351 if h_k_lt_n: k < n then
13721352 have h_k_lt_n_add_1: k < n + 1 := by omega
13731353 simp only [h_k_lt_n_add_1, ↓reduceDIte]
1374- push_neg at h_k_eq
1354+ push Not at h_k_eq
13751355 simp only [h_k_lt_n, ↓reduceDIte]
13761356 unfold msbTerm
13771357 interval_cases h_m_last_val: m ⟨n, by omega⟩
0 commit comments