Skip to content

Commit 0cfb4bc

Browse files
dwrenshadwrensha
committed
update mathlib
1 parent ae082db commit 0cfb4bc

4 files changed

Lines changed: 48 additions & 48 deletions

File tree

‎Compfiles/Bulgaria1998P11.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -82,24 +82,24 @@ lemma two_le_pow_two (l : ℕ) : 2 ≤ 2 ^ (l + 1) := by
8282

8383
lemma two_n_and_rest_factorisation (m : ℕ) (even_m : Even m) (h: 0 < m) :
8484
∃ (l : ℕ) (m₁ : ℕ), 1 ≤ l ∧ Odd m₁ ∧ m = 2 ^ l * m₁ := by
85-
have ⟨a, ha⟩ := Nat.maxPowDiv.pow_dvd 2 m
86-
refine ⟨Nat.maxPowDiv 2 m, a, ?_⟩
85+
have ⟨a, ha⟩ := (pow_padicValNat_dvd : 2 ^ padicValNat 2 m ∣ m)
86+
refine ⟨padicValNat 2 m, a, ?_⟩
8787
obtain ⟨k, hk⟩ := even_iff_two_dvd.mp even_m
8888
have hk0 : 0 < k := by lia
8989
refine ⟨?_, ?_, ha⟩
9090
· rw [hk]
9191
rw [show 2 * k = 2^1 * k from rfl]
92-
rw [Nat.maxPowDiv.base_pow_mul one_lt_two hk0]
93-
exact Nat.le_add_left 1 (Nat.maxPowDiv 2 k)
92+
rw [padicValNat_base_pow_mul one_lt_two hk0.ne']
93+
exact Nat.le_add_left 1 (padicValNat 2 k)
9494
· by_contra! Ha
9595
rw [Nat.not_odd_iff_even] at Ha
9696
obtain ⟨b, hb⟩ := Ha
97-
have h3 : 2 ^ (Nat.maxPowDiv 2 m + 1) ∣ m := by
97+
have h3 : 2 ^ (padicValNat 2 m + 1) ∣ m := by
9898
use b
9999
rw [hb] at ha
100100
rw [pow_succ]
101101
linarith only [ha]
102-
have h4 := Nat.maxPowDiv.le_of_dvd one_lt_two (Nat.ne_zero_of_lt h) h3
102+
have h4 := (Nat.pow_dvd_iff_le_padicValNat (by omega) (Nat.ne_zero_of_lt h)).mp h3
103103
exact (lt_self_iff_false _).mp (Nat.succ_le_iff.mp h4)
104104

105105
lemma m_mod_2_contradiction (m n A : ℕ)

‎Compfiles/Imo1988P6.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ →
142142
-- Let m be the smallest element of the nonempty set S.
143143
let m : ℕ := WellFounded.min Nat.lt_wfRel.wf S S_nonempty
144144
have m_mem : m ∈ S := WellFounded.min_mem Nat.lt_wfRel.wf S S_nonempty
145-
have m_min : ∀ k ∈ S, ¬k < m := fun k hk => WellFounded.not_lt_min Nat.lt_wfRel.wf S S_nonempty hk
145+
have m_min : ∀ k ∈ S, ¬k < m := fun k hk => WellFounded.not_lt_min Nat.lt_wfRel.wf S hk
146146
-- It suffices to show that there is point (a,b) with b ∈ S and b < m.
147147
rsuffices ⟨p', p'_mem, p'_small⟩ : ∃ p' : ℕ × ℕ, p'.2 ∈ S ∧ p'.2 < m
148148
· solve_by_elim

‎Compfiles/Usa2023P4.lean‎

Lines changed: 39 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -110,61 +110,61 @@ lemma end_inevitable_n {a : ℕ+} {n : ℕ} {m : ℕ} {s : State n}
110110
| AliceTurn _ _ _ _ ih => exact .Step _ ih
111111

112112
lemma lemma3 (N : ℕ) (b : Blackboard N)
113-
(hd : ∑ i : Fin N, Nat.maxPowDiv 2 (b i) = 0) :
113+
(hd : ∑ i : Fin N, padicValNat 2 (b i) = 0) :
114114
∀ i : Fin N, ¬ Even (b i).val := by
115115
intro i hei
116-
have h1 : 0 < Nat.maxPowDiv 2 (b i).val := by
116+
have h1 : 0 < padicValNat 2 (b i).val := by
117117
have h2 : 2 ∣ (b i : ℕ) := even_iff_two_dvd.mp hei
118118
replace h2 : 2^1 ∣ (b i : ℕ) := h2
119-
exact Nat.maxPowDiv.le_of_dvd one_lt_two (PNat.ne_zero (b i)) h2
119+
exact (Nat.pow_dvd_iff_le_padicValNat (by omega) (PNat.ne_zero (b i))).mp h2
120120
rw [Finset.sum_eq_zero_iff] at hd
121121
have h2 := hd i (Finset.mem_univ i)
122122
lia
123123

124124
lemma lemma5 {a x : ℕ} (hx : 0 < x)
125-
(hax : Nat.maxPowDiv 2 x < Nat.maxPowDiv 2 a) :
126-
Nat.maxPowDiv 2 (x + a) < Nat.maxPowDiv 2 a := by
125+
(hax : padicValNat 2 x < padicValNat 2 a) :
126+
padicValNat 2 (x + a) < padicValNat 2 a := by
127127
by_contra! H
128-
have h1 : 2 ^ (Nat.maxPowDiv 2 (x + a)) ∣ x + a := Nat.maxPowDiv.pow_dvd 2 (x + a)
129-
have h2 : 2 ^ (Nat.maxPowDiv 2 a) ∣ a := Nat.maxPowDiv.pow_dvd 2 a
130-
have h4 : 2 ^ (Nat.maxPowDiv 2 a) ∣ x + a :=
128+
have h1 : 2 ^ (padicValNat 2 (x + a)) ∣ x + a := pow_padicValNat_dvd
129+
have h2 : 2 ^ (padicValNat 2 a) ∣ a := pow_padicValNat_dvd
130+
have h4 : 2 ^ (padicValNat 2 a) ∣ x + a :=
131131
Nat.pow_dvd_of_le_of_pow_dvd H h1
132-
have h5 : 2 ^ (Nat.maxPowDiv 2 a) ∣ x := (Nat.dvd_add_iff_left h2).mpr h4
133-
have h6 := Nat.maxPowDiv.le_of_dvd one_lt_two (Nat.ne_zero_of_lt hx) h5
132+
have h5 : 2 ^ (padicValNat 2 a) ∣ x := (Nat.dvd_add_iff_left h2).mpr h4
133+
have h6 := (Nat.pow_dvd_iff_le_padicValNat (by omega) (Nat.ne_zero_of_lt hx)).mp h5
134134
lia
135135

136136
lemma lemma5' {a x : ℕ} (hx : 0 < x)
137-
(hax : Nat.maxPowDiv 2 x < Nat.maxPowDiv 2 a) :
138-
Nat.maxPowDiv 2 (x + a) = Nat.maxPowDiv 2 x := by
139-
have h1 : 2 ^ (Nat.maxPowDiv 2 (x + a)) ∣ x + a := Nat.maxPowDiv.pow_dvd 2 (x + a)
140-
have h2 : 2 ^ (Nat.maxPowDiv 2 a) ∣ a := Nat.maxPowDiv.pow_dvd 2 a
141-
have h4 : 2 ^ (Nat.maxPowDiv 2 x) ∣ x := Nat.maxPowDiv.pow_dvd 2 x
137+
(hax : padicValNat 2 x < padicValNat 2 a) :
138+
padicValNat 2 (x + a) = padicValNat 2 x := by
139+
have h1 : 2 ^ (padicValNat 2 (x + a)) ∣ x + a := pow_padicValNat_dvd
140+
have h2 : 2 ^ (padicValNat 2 a) ∣ a := pow_padicValNat_dvd
141+
have h4 : 2 ^ (padicValNat 2 x) ∣ x := pow_padicValNat_dvd
142142

143-
obtain ⟨c, hc⟩ : ∃ c, (Nat.maxPowDiv 2 a) = (Nat.maxPowDiv 2 x) + 1 + c :=
143+
obtain ⟨c, hc⟩ : ∃ c, (padicValNat 2 a) = (padicValNat 2 x) + 1 + c :=
144144
Nat.exists_eq_add_of_le hax
145145

146146
obtain ⟨aa, haa⟩ := h2
147147
obtain ⟨xx, hxx⟩ := h4
148148
obtain ⟨xa, hxa⟩ := h1
149149
rw [hc, add_assoc, pow_add] at haa
150150

151-
have h10 : x + a = 2 ^ Nat.maxPowDiv 2 x * (xx + 2 ^ (1 + c) * aa) := by
151+
have h10 : x + a = 2 ^ padicValNat 2 x * (xx + 2 ^ (1 + c) * aa) := by
152152
nth_rw 1 [hxx]
153153
nth_rw 1 [haa]
154154
rw [mul_assoc, ←mul_add]
155155

156-
have h12 : 2 ^ Nat.maxPowDiv 2 x ∣ x + a := Dvd.intro _ h10.symm
157-
replace h12 := Nat.maxPowDiv.le_of_dvd one_lt_two (by lia) h12
158-
suffices H : Nat.maxPowDiv 2 (x + a) ≤ Nat.maxPowDiv 2 x from Nat.le_antisymm H h12
156+
have h12 : 2 ^ padicValNat 2 x ∣ x + a := Dvd.intro _ h10.symm
157+
replace h12 := (Nat.pow_dvd_iff_le_padicValNat (by omega) (by lia)).mp h12
158+
suffices H : padicValNat 2 (x + a) ≤ padicValNat 2 x from Nat.le_antisymm H h12
159159
by_contra! H
160160

161161
rw [h10] at H
162162

163163
have h16 : ¬ 2 ∣ xx := by
164164
rintro ⟨z, rfl⟩
165165
rw [←mul_assoc, ←pow_succ] at hxx
166-
have h17 : 2 ^ (Nat.maxPowDiv 2 x + 1) ∣ x := Dvd.intro z hxx.symm
167-
replace h17 := Nat.maxPowDiv.le_of_dvd one_lt_two (Nat.ne_zero_of_lt hx) h17
166+
have h17 : 2 ^ (padicValNat 2 x + 1) ∣ x := Dvd.intro z hxx.symm
167+
replace h17 := (Nat.pow_dvd_iff_le_padicValNat (by omega) (Nat.ne_zero_of_lt hx)).mp h17
168168
lia
169169

170170
have h15' : ¬ 2 ∣ xx + 2 ^ (1 + c) * aa := by
@@ -175,13 +175,13 @@ lemma lemma5' {a x : ℕ} (hx : 0 < x)
175175
have : 2 ∣ xx := (Nat.dvd_add_iff_left h19).mpr HH
176176
contradiction
177177

178-
have h15 : Nat.maxPowDiv 2 (xx + 2 ^ (1 + c) * aa) = 0 := by
178+
have h15 : padicValNat 2 (xx + 2 ^ (1 + c) * aa) = 0 := by
179179
by_contra! HH
180-
replace HH : 0 < Nat.maxPowDiv 2 (xx + 2 ^ (1 + c) * aa) := Nat.zero_lt_of_ne_zero HH
180+
replace HH : 0 < padicValNat 2 (xx + 2 ^ (1 + c) * aa) := Nat.zero_lt_of_ne_zero HH
181181
generalize hee : xx + 2 ^ (1 + c) * aa = ee
182182
rw [hee] at HH h15'
183-
have h18 := Nat.maxPowDiv.pow_dvd 2 ee
184-
generalize hee' : Nat.maxPowDiv 2 ee = ee'
183+
have h18 : 2 ^ padicValNat 2 ee ∣ ee := pow_padicValNat_dvd
184+
generalize hee' : padicValNat 2 ee = ee'
185185
rw [hee'] at h18 HH
186186
cases ee' with | zero => lia | succ ee' =>
187187
rw [pow_succ] at h18
@@ -194,15 +194,15 @@ lemma lemma5' {a x : ℕ} (hx : 0 < x)
194194
rw [hk]
195195
exact Nat.zero_lt_succ (2 * k)
196196

197-
rw [Nat.maxPowDiv.base_pow_mul one_lt_two h13] at H
197+
rw [padicValNat_base_pow_mul one_lt_two h13.ne'] at H
198198
rw [h15, zero_add] at H
199199
lia
200200

201201
lemma alice_move_preserves_nu
202202
(a : ℕ+) (N : ℕ) (b0 : Blackboard N)
203-
(hd : ∀ i : Fin N, Nat.maxPowDiv 2 (b0 i) < Nat.maxPowDiv 2 a)
203+
(hd : ∀ i : Fin N, padicValNat 2 (b0 i) < padicValNat 2 a)
204204
(s1 : State N) (hs1 : s1 ∈ valid_moves a N ⟨b0, .Alice⟩) :
205-
∀ i : Fin N, Nat.maxPowDiv 2 (s1.board i) < Nat.maxPowDiv 2 a := by
205+
∀ i : Fin N, padicValNat 2 (s1.board i) < padicValNat 2 a := by
206206
intro i
207207
dsimp [valid_moves] at hs1
208208
obtain ⟨j, rfl⟩ := hs1
@@ -224,9 +224,9 @@ lemma alice_move_preserves_nu
224224

225225
lemma alice_move_preserves_nu'
226226
(a : ℕ+) (N : ℕ) (b0 : Blackboard N)
227-
(hd : ∀ i : Fin N, Nat.maxPowDiv 2 (b0 i) < Nat.maxPowDiv 2 a)
227+
(hd : ∀ i : Fin N, padicValNat 2 (b0 i) < padicValNat 2 a)
228228
(s1 : State N) (hs1 : s1 ∈ valid_moves a N ⟨b0, .Alice⟩) :
229-
∀ i, Nat.maxPowDiv 2 (s1.board i) = Nat.maxPowDiv 2 (b0 i) := by
229+
∀ i, padicValNat 2 (s1.board i) = padicValNat 2 (b0 i) := by
230230
intro i
231231
dsimp [valid_moves] at hs1
232232
obtain ⟨j, rfl⟩ := hs1
@@ -254,15 +254,15 @@ lemma bob_moves_after_alice {a : ℕ+} {N : Nat} (b0 : Blackboard N)
254254
simp
255255

256256
lemma lemma6 {x : ℕ} (hp : 0 < x) (hx : Even x)
257-
: Nat.maxPowDiv x / 2 + 1 = Nat.maxPowDiv x := by
257+
: padicValNat 2 (x / 2) + 1 = padicValNat 2 x := by
258258
sorry
259259

260260
-- When N ≥ 2, if ν2(x) < ν2(a) for all x ∈ S, the game must terminate
261261
-- in ∑_{x∈S} ν2(x) moves, no matter what either player does.
262262
lemma lemma2' (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
263-
(hd : ∀ i : Fin N, Nat.maxPowDiv 2 (s0.board i) < Nat.maxPowDiv 2 a) :
264-
EndInevitableIn a N (∑ i : Fin N, Nat.maxPowDiv 2 (s0.board i)) s0 := by
265-
generalize hms : ∑ i : Fin N, Nat.maxPowDiv 2 (s0.board i) = ms
263+
(hd : ∀ i : Fin N, padicValNat 2 (s0.board i) < padicValNat 2 a) :
264+
EndInevitableIn a N (∑ i : Fin N, padicValNat 2 (s0.board i)) s0 := by
265+
generalize hms : ∑ i : Fin N, padicValNat 2 (s0.board i) = ms
266266
revert s0
267267
induction' ms with ms' ih
268268
· intro s0 hd hms
@@ -281,10 +281,10 @@ lemma lemma2' (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
281281
apply EndInevitableIn.AliceTurn _ ⟨b0, .Alice⟩
282282
intro s hs
283283
have h2 : Even (a:ℕ) := by
284-
have ha : 0 < Nat.maxPowDiv 2 ↑a := by
284+
have ha : 0 < padicValNat 2 ↑a := by
285285
have := hd ⟨0, by lia⟩
286286
lia
287-
have ha1 := Nat.maxPowDiv.pow_dvd 2 a
287+
have ha1 : 2 ^ padicValNat 2 (a : ℕ) ∣ (a : ℕ) := pow_padicValNat_dvd
288288
rw [even_iff_two_dvd]
289289
exact Nat.dvd_of_pow_dvd ha ha1
290290
apply EndInevitableIn.BaseCase
@@ -325,7 +325,7 @@ lemma lemma2' (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
325325
intro s hs
326326
have h1 := alice_move_preserves_nu' a N b0 hd s hs
327327
dsimp at hms
328-
have h2 : ∑ i : Fin N, Nat.maxPowDiv 2 ↑(b0 i) = ∑ i : Fin N, Nat.maxPowDiv 2 ↑(s.board i) := by
328+
have h2 : ∑ i : Fin N, padicValNat 2 ↑(b0 i) = ∑ i : Fin N, padicValNat 2 ↑(s.board i) := by
329329
congr
330330
ext i
331331
exact (h1 i).symm
@@ -346,7 +346,7 @@ lemma lemma2' (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
346346
-- When N ≥ 2, if ν2(x) < ν2(a) for all x ∈ S, the game must terminate no
347347
-- matter what either player does.
348348
lemma lemma2 (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
349-
(hd : ∀ i : Fin N, Nat.maxPowDiv 2 (s0.board i) < Nat.maxPowDiv 2 a) :
349+
(hd : ∀ i : Fin N, padicValNat 2 (s0.board i) < padicValNat 2 a) :
350350
EndInevitable a N s0 := by
351351
exact end_inevitable_n (lemma2' a N hN s0 hd)
352352

‎lake-manifest.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "b12200df69d09d1b1979c99e00bbd45be65121e7",
18+
"rev": "a8fbd155de0f70e47ebaba82deff888299e9d7f3",
1919
"name": "mathlib",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "master",
@@ -85,7 +85,7 @@
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover-community",
88-
"rev": "87f6314ff2cc922489cd73cd0fbc2252f39aa153",
88+
"rev": "77a5160a74772214ef37caba2847cfe9ab600285",
8989
"name": "batteries",
9090
"manifestFile": "lake-manifest.json",
9191
"inputRev": "main",

0 commit comments

Comments
 (0)