Skip to content

Commit a077c04

Browse files
grunweggrunweg
committed
Merge branch 'master' into MR-met-weaken
2 parents cb4f038 + 1e919af commit a077c04

798 files changed

Lines changed: 8130 additions & 4998 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Archive/Examples/IfNormalization/Result.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we kno
5454
`e` to the literal booleans given by `l` -/
5555
def normalize (l : AList (fun _ : ℕ => Bool)) :
5656
(e : IfExpr) → { e' : IfExpr //
57-
(∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
57+
(∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) id))
5858
∧ e'.normalized
5959
∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
6060
| lit b => ⟨lit b, ◾⟩

‎Archive/Examples/IfNormalization/WithoutAesop.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ theorem eval_ite_ite' {a b c d e : IfExpr} {f : ℕ → Bool} :
3636
`e` to the literal booleans given by `l` -/
3737
def normalize' (l : AList (fun _ : ℕ => Bool)) :
3838
(e : IfExpr) → { e' : IfExpr //
39-
(∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
39+
(∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) id))
4040
∧ e'.normalized
4141
∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
4242
| lit b => ⟨lit b, by simp⟩

‎Archive/Imo/Imo2021Q1.lean‎

Lines changed: 19 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ import Mathlib.Tactic.Linarith
1010
/-!
1111
# IMO 2021 Q1
1212
13-
Let `n≥100` be an integer. Ivan writes the numbers `n, n+1,..., 2n` each on different cards.
13+
Let `n ≥ 100` be an integer. Ivan writes the numbers `n, n+1, ..., 2*n` each on different cards.
1414
He then shuffles these `n+1` cards, and divides them into two piles. Prove that at least one
1515
of the piles contains two cards such that the sum of their numbers is a perfect square.
1616
@@ -30,7 +30,7 @@ which can be solved to give
3030
b = 2 * l ^ 2 + 1
3131
c = 2 * l ^ 2 + 4 * l
3232
33-
Therefore, it is enough to show that there exists a natural number l such that
33+
Therefore, it is enough to show that there exists a natural number `l` such that
3434
`n ≤ 2 * l ^ 2 - 4 * l` and `2 * l ^ 2 + 4 * l ≤ 2 * n` for `n ≥ 100`.
3535
3636
Then, by the Pigeonhole principle, at least two numbers in the triplet must lie in the same pile,
@@ -41,13 +41,13 @@ open Finset
4141

4242
namespace Imo2021Q1
4343

44-
-- We will later make use of the fact that there exists (l : ℕ) such that
45-
-- n ≤ 2 * l ^ 2 - 4 * l and 2 * l ^ 2 + 4 * l ≤ 2 * n for n ≥ 100.
46-
theorem exists_numbers_in_interval (n : ℕ) (hn : 100 ≤ n) :
44+
-- We will later make use of the fact that there exists `l : ℕ` such that
45+
-- `n ≤ 2 * l ^ 2 - 4 * l` and `2 * l ^ 2 + 4 * l ≤ 2 * n` for `n ≥ 100`.
46+
lemma exists_numbers_in_interval {n : ℕ} (hn : 100 ≤ n) :
4747
∃ l : ℕ, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n := by
4848
have hn' : 1 ≤ Nat.sqrt (n + 1) := by
4949
rw [Nat.le_sqrt]
50-
linarith
50+
apply Nat.le_add_left
5151
have h₁ := Nat.sqrt_le' (n + 1)
5252
have h₂ := Nat.succ_le_succ_sqrt' (n + 1)
5353
have h₃ : 10 ≤ (n + 1).sqrt := by
@@ -60,11 +60,11 @@ theorem exists_numbers_in_interval (n : ℕ) (hn : 100 ≤ n) :
6060
_ ≤ 2 * l ^ 2 := by nlinarith only [h₃]
6161
· linarith only [h₁]
6262

63-
theorem exists_triplet_summing_to_squares (n : ℕ) (hn : 100 ≤ n) :
63+
lemma exists_triplet_summing_to_squares {n : ℕ} (hn : 100 ≤ n) :
6464
∃ a b c : ℕ, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧
65-
(∃ k : ℕ, a + b = k ^ 2) ∧ (∃ l : ℕ, c + a = l ^ 2) ∧ ∃ m : ℕ, b + c = m ^ 2 := by
66-
obtain ⟨l, hl1, hl2⟩ := exists_numbers_in_interval n hn
67-
have p : 1 < l := by contrapose! hl1; interval_cases l <;> linarith
65+
IsSquare (a + b) ∧ IsSquare (c + a) ∧ IsSquare (b + c) := by
66+
obtain ⟨l, hl1, hl2⟩ := exists_numbers_in_interval hn
67+
have hl : 1 < l := by contrapose! hl1; interval_cases l <;> linarith
6868
have h₁ : 4 * l ≤ 2 * l ^ 2 := by linarith
6969
have h₂ : 1 ≤ 2 * l := by linarith
7070
refine ⟨2 * l ^ 2 - 4 * l, 2 * l ^ 2 + 1, 2 * l ^ 2 + 4 * l, ?_, ?_, ?_,
@@ -74,15 +74,14 @@ theorem exists_triplet_summing_to_squares (n : ℕ) (hn : 100 ≤ n) :
7474
-- Since it will be more convenient to work with sets later on, we will translate the above claim
7575
-- to state that there always exists a set B ⊆ [n, 2n] of cardinality at least 3, such that each
7676
-- pair of pairwise unequal elements of B sums to a perfect square.
77-
theorem exists_finset_3_le_card_with_pairs_summing_to_squares (n : ℕ) (hn : 100 ≤ n) :
77+
lemma exists_finset_3_le_card_with_pairs_summing_to_squares {n : ℕ} (hn : 100 ≤ n) :
7878
∃ B : Finset ℕ,
7979
2 * 1 + 1 ≤ B.card ∧
80-
(∀ a ∈ B, ∀ b ∈ B, a ≠ b → ∃ k, a + b = k ^ 2) ∧
80+
(∀ a ∈ B, ∀ b ∈ B, a ≠ b → IsSquare (a + b)) ∧
8181
∀ c ∈ B, n ≤ c ∧ c ≤ 2 * n := by
82-
obtain ⟨a, b, c, hna, hab, hbc, hcn, h₁, h₂, h₃⟩ := exists_triplet_summing_to_squares n hn
82+
obtain ⟨a, b, c, hna, hab, hbc, hcn, h₁, h₂, h₃⟩ := exists_triplet_summing_to_squares hn
8383
refine ⟨{a, b, c}, ?_, ?_, ?_⟩
84-
· suffices ({a, b, c} : Finset ℕ).card = 3 by rw [this]
85-
suffices a ∉ {b, c} ∧ b ∉ {c} by
84+
· suffices a ∉ {b, c} ∧ b ∉ {c} by
8685
rw [Finset.card_insert_of_not_mem this.1, Finset.card_insert_of_not_mem this.2,
8786
Finset.card_singleton]
8887
rw [Finset.mem_insert, Finset.mem_singleton, Finset.mem_singleton]
@@ -105,22 +104,20 @@ open Imo2021Q1
105104

106105
theorem imo2021_q1 :
107106
∀ n : ℕ, 100 ≤ n → ∀ A ⊆ Finset.Icc n (2 * n),
108-
(∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ ∃ k : ℕ, a + b = k ^ 2) ∨
109-
∃ a ∈ Finset.Icc n (2 * n) \ A, ∃ b ∈ Finset.Icc n (2 * n) \ A,
110-
a ≠ b ∧ ∃ k : ℕ, a + b = k ^ 2 := by
107+
(∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ IsSquare (a + b)) ∨
108+
∃ a ∈ Finset.Icc n (2 * n) \ A, ∃ b ∈ Finset.Icc n (2 * n) \ A, a ≠ b ∧ IsSquare (a + b) := by
111109
intro n hn A hA
112110
-- For each n ∈ ℕ such that 100 ≤ n, there exists a pairwise unequal triplet {a, b, c} ⊆ [n, 2n]
113111
-- such that all pairwise sums are perfect squares. In practice, it will be easier to use
114112
-- a finite set B ⊆ [n, 2n] such that all pairwise unequal pairs of B sum to a perfect square
115113
-- noting that B has cardinality greater or equal to 3, by the explicit construction of the
116114
-- triplet {a, b, c} before.
117-
obtain ⟨B, hB, h₁, h₂⟩ := exists_finset_3_le_card_with_pairs_summing_to_squares n hn
115+
obtain ⟨B, hB, h₁, h₂⟩ := exists_finset_3_le_card_with_pairs_summing_to_squares hn
118116
have hBsub : B ⊆ Finset.Icc n (2 * n) := by
119117
intro c hcB; simpa only [Finset.mem_Icc] using h₂ c hcB
120118
have hB' : 2 * 1 < (B ∩ (Finset.Icc n (2 * n) \ A) ∪ B ∩ A).card := by
121-
rw [← inter_union_distrib_left, sdiff_union_self_eq_union, union_eq_left.2 hA,
122-
inter_eq_left.2 hBsub]
123-
exact Nat.succ_le_iff.mp hB
119+
rwa [← inter_union_distrib_left, sdiff_union_self_eq_union, union_eq_left.2 hA,
120+
inter_eq_left.2 hBsub, ← Nat.succ_le_iff]
124121
-- Since B has cardinality greater or equal to 3, there must exist a subset C ⊆ B such that
125122
-- for any A ⊆ [n, 2n], either C ⊆ A or C ⊆ [n, 2n] \ A and C has cardinality greater
126123
-- or equal to 2.

‎Archive/Imo/Imo2024Q1.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
7171
by_contra! hn
7272
have hr : 1 < ⌈α⁻¹⌉₊ := by
7373
rw [Nat.lt_ceil]
74-
exact_mod_cast one_lt_inv h0 hn
74+
exact_mod_cast (one_lt_inv₀ h0).2 hn
7575
apply hr.ne'
7676
suffices ⌈α⁻¹⌉₊ = (1 : ℤ) from mod_cast this
7777
apply Int.eq_one_of_dvd_one (Int.zero_le_ofNat _)
@@ -153,7 +153,7 @@ lemma not_condition_of_mem_Ioo {α : ℝ} (h : α ∈ Set.Ioo 0 2) : ¬Condition
153153
convert hna using 1
154154
field_simp
155155
rw [sub_eq_add_neg, ← le_sub_iff_add_le', neg_le, neg_sub] at hna'
156-
rw [le_inv (by linarith) (mod_cast hn), ← not_lt] at hna'
156+
rw [le_inv_comm₀ (by linarith) (mod_cast hn), ← not_lt] at hna'
157157
apply hna'
158158
exact_mod_cast Nat.lt_floor_add_one (_ : ℝ)
159159

‎Archive/Wiedijk100Theorems/BallotProblem.lean‎

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Bhavik Mehta, Kexing Ying. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Bhavik Mehta, Kexing Ying
55
-/
6-
import Mathlib.Probability.CondCount
6+
import Mathlib.Probability.UniformOn
77

88
/-!
99
# Ballot problem
@@ -188,21 +188,21 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
188188

189189
theorem first_vote_pos :
190190
∀ p q,
191-
0 < p + q → condCount (countedSequence p q : Set (List ℤ)) {l | l.headI = 1} = p / (p + q)
191+
0 < p + q → uniformOn (countedSequence p q : Set (List ℤ)) {l | l.headI = 1} = p / (p + q)
192192
| p + 1, 0, _ => by
193-
rw [counted_right_zero, condCount_singleton]
193+
rw [counted_right_zero, uniformOn_singleton]
194194
simp [ENNReal.div_self _ _, List.replicate_succ]
195195
| 0, q + 1, _ => by
196-
rw [counted_left_zero, condCount_singleton]
196+
rw [counted_left_zero, uniformOn_singleton]
197197
simp only [List.replicate, Nat.add_eq, add_zero, mem_setOf_eq, List.headI_cons, Nat.cast_zero,
198198
ENNReal.zero_div, ite_eq_right_iff]
199199
decide
200200
| p + 1, q + 1, _ => by
201201
simp_rw [counted_succ_succ]
202-
rw [← condCount_disjoint_union ((countedSequence_finite _ _).image _)
202+
rw [← uniformOn_disjoint_union ((countedSequence_finite _ _).image _)
203203
((countedSequence_finite _ _).image _) (disjoint_bits _ _),
204204
← counted_succ_succ,
205-
condCount_eq_one_of ((countedSequence_finite p (q + 1)).image _)
205+
uniformOn_eq_one_of ((countedSequence_finite p (q + 1)).image _)
206206
((countedSequence_nonempty _ _).image _)]
207207
· have : List.cons (-1) '' countedSequence (p + 1) q ∩ {l : List ℤ | l.headI = 1} = ∅ := by
208208
ext
@@ -215,7 +215,7 @@ theorem first_vote_pos :
215215
List.cons 1 '' countedSequence p (q + 1) := by
216216
rw [inter_eq_right, counted_succ_succ]
217217
exact subset_union_left
218-
rw [(condCount_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, condCount,
218+
rw [(uniformOn_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, uniformOn,
219219
cond_apply _ list_int_measurableSet, hint, count_injective_image List.cons_injective,
220220
count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
221221
Nat.cast_add, Nat.cast_one, mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
@@ -230,27 +230,27 @@ theorem headI_mem_of_nonempty {α : Type*} [Inhabited α] : ∀ {l : List α} (_
230230
| x::l, _ => List.mem_cons_self x l
231231

232232
theorem first_vote_neg (p q : ℕ) (h : 0 < p + q) :
233-
condCount (countedSequence p q) {l | l.headI = 1}ᶜ = q / (p + q) := by
233+
uniformOn (countedSequence p q) {l | l.headI = 1}ᶜ = q / (p + q) := by
234234
have h' : (p + q : ℝ≥0∞) ≠ 0 := mod_cast h.ne'
235-
have := condCount_compl
235+
have := uniformOn_compl
236236
{l : List ℤ | l.headI = 1}ᶜ (countedSequence_finite p q) (countedSequence_nonempty p q)
237237
rw [compl_compl, first_vote_pos _ _ h] at this
238238
rw [ENNReal.eq_sub_of_add_eq _ this, ENNReal.eq_div_iff, ENNReal.mul_sub, mul_one,
239239
ENNReal.mul_div_cancel', ENNReal.add_sub_cancel_left]
240240
all_goals simp_all [ENNReal.div_eq_top]
241241

242-
theorem ballot_same (p : ℕ) : condCount (countedSequence (p + 1) (p + 1)) staysPositive = 0 := by
243-
rw [condCount_eq_zero_iff (countedSequence_finite _ _), eq_empty_iff_forall_not_mem]
242+
theorem ballot_same (p : ℕ) : uniformOn (countedSequence (p + 1) (p + 1)) staysPositive = 0 := by
243+
rw [uniformOn_eq_zero_iff (countedSequence_finite _ _), eq_empty_iff_forall_not_mem]
244244
rintro x ⟨hx, t⟩
245245
apply ne_of_gt (t x _ x.suffix_refl)
246246
· simpa using sum_of_mem_countedSequence hx
247247
· refine List.ne_nil_of_length_pos ?_
248248
rw [length_of_mem_countedSequence hx]
249249
exact Nat.add_pos_left (Nat.succ_pos _) _
250250

251-
theorem ballot_edge (p : ℕ) : condCount (countedSequence (p + 1) 0) staysPositive = 1 := by
251+
theorem ballot_edge (p : ℕ) : uniformOn (countedSequence (p + 1) 0) staysPositive = 1 := by
252252
rw [counted_right_zero]
253-
refine condCount_eq_one_of (finite_singleton _) (singleton_nonempty _) ?_
253+
refine uniformOn_eq_one_of (finite_singleton _) (singleton_nonempty _) ?_
254254
refine singleton_subset_iff.2 fun l hl₁ hl₂ => List.sum_pos _ (fun x hx => ?_) hl₁
255255
rw [List.eq_of_mem_replicate (hl₂.mem hx)]
256256
norm_num
@@ -267,9 +267,9 @@ theorem countedSequence_int_pos_counted_succ_succ (p q : ℕ) :
267267
norm_num
268268

269269
theorem ballot_pos (p q : ℕ) :
270-
condCount (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}) staysPositive =
271-
condCount (countedSequence p (q + 1)) staysPositive := by
272-
rw [countedSequence_int_pos_counted_succ_succ, condCount, condCount,
270+
uniformOn (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}) staysPositive =
271+
uniformOn (countedSequence p (q + 1)) staysPositive := by
272+
rw [countedSequence_int_pos_counted_succ_succ, uniformOn, uniformOn,
273273
cond_apply _ list_int_measurableSet, cond_apply _ list_int_measurableSet,
274274
count_injective_image List.cons_injective]
275275
congr 1
@@ -294,9 +294,9 @@ theorem countedSequence_int_neg_counted_succ_succ (p q : ℕ) :
294294
norm_num
295295

296296
theorem ballot_neg (p q : ℕ) (qp : q < p) :
297-
condCount (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}ᶜ) staysPositive =
298-
condCount (countedSequence (p + 1) q) staysPositive := by
299-
rw [countedSequence_int_neg_counted_succ_succ, condCount, condCount,
297+
uniformOn (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}ᶜ) staysPositive =
298+
uniformOn (countedSequence (p + 1) q) staysPositive := by
299+
rw [countedSequence_int_neg_counted_succ_succ, uniformOn, uniformOn,
300300
cond_apply _ list_int_measurableSet, cond_apply _ list_int_measurableSet,
301301
count_injective_image List.cons_injective]
302302
congr 1
@@ -310,7 +310,7 @@ theorem ballot_neg (p q : ℕ) (qp : q < p) :
310310
exact List.cons_injective
311311

312312
theorem ballot_problem' :
313-
∀ q p, q < p → (condCount (countedSequence p q) staysPositive).toReal = (p - q) / (p + q) := by
313+
∀ q p, q < p → (uniformOn (countedSequence p q) staysPositive).toReal = (p - q) / (p + q) := by
314314
classical
315315
apply Nat.diag_induction
316316
· intro p
@@ -322,12 +322,12 @@ theorem ballot_problem' :
322322
rw [div_self]
323323
exact Nat.cast_add_one_ne_zero p
324324
· intro q p qp h₁ h₂
325-
haveI := condCount_isProbabilityMeasure
325+
haveI := uniformOn_isProbabilityMeasure
326326
(countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _)
327-
haveI := condCount_isProbabilityMeasure
327+
haveI := uniformOn_isProbabilityMeasure
328328
(countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _)
329329
have h₃ : p + 1 + (q + 1) > 0 := Nat.add_pos_left (Nat.succ_pos _) _
330-
rw [← condCount_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
330+
rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
331331
first_vote_pos _ _ h₃, first_vote_neg _ _ h₃, ballot_pos, ballot_neg _ _ qp]
332332
rw [ENNReal.toReal_add, ENNReal.toReal_mul, ENNReal.toReal_mul, ← Nat.cast_add,
333333
ENNReal.toReal_div, ENNReal.toReal_div, ENNReal.toReal_nat, ENNReal.toReal_nat,
@@ -349,12 +349,12 @@ theorem ballot_problem' :
349349

350350
/-- The ballot problem. -/
351351
theorem ballot_problem :
352-
∀ q p, q < p → condCount (countedSequence p q) staysPositive = (p - q) / (p + q) := by
352+
∀ q p, q < p → uniformOn (countedSequence p q) staysPositive = (p - q) / (p + q) := by
353353
intro q p qp
354354
haveI :=
355-
condCount_isProbabilityMeasure (countedSequence_finite p q) (countedSequence_nonempty _ _)
355+
uniformOn_isProbabilityMeasure (countedSequence_finite p q) (countedSequence_nonempty _ _)
356356
have :
357-
(condCount (countedSequence p q) staysPositive).toReal =
357+
(uniformOn (countedSequence p q) staysPositive).toReal =
358358
((p - q) / (p + q) : ℝ≥0∞).toReal := by
359359
rw [ballot_problem' q p qp]
360360
rw [ENNReal.toReal_div, ← Nat.cast_add, ← Nat.cast_add, ENNReal.toReal_nat,

‎Archive/Wiedijk100Theorems/BirthdayProblem.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Rodriguez
55
-/
66
import Mathlib.Data.Fintype.CardEmbedding
7-
import Mathlib.Probability.CondCount
7+
import Mathlib.Probability.UniformOn
88
import Mathlib.Probability.Notation
99

1010
/-!
@@ -52,15 +52,15 @@ instance : MeasurableSingletonClass (Fin m) :=
5252
/- We then endow the space with a canonical measure, which is called ℙ.
5353
We define this to be the conditional counting measure. -/
5454
noncomputable instance : MeasureSpace (Fin n → Fin m) :=
55-
⟨condCount Set.univ⟩
55+
⟨uniformOn Set.univ⟩
5656

5757
-- The canonical measure on `Fin n → Fin m` is a probability measure (except on an empty space).
5858
instance : IsProbabilityMeasure (ℙ : Measure (Fin n → Fin (m + 1))) :=
59-
condCount_isProbabilityMeasure Set.finite_univ Set.univ_nonempty
59+
uniformOn_isProbabilityMeasure Set.finite_univ Set.univ_nonempty
6060

6161
theorem FinFin.measure_apply {s : Set <| Fin n → Fin m} :
6262
ℙ s = |s.toFinite.toFinset| / ‖Fin n → Fin m‖ := by
63-
erw [condCount_univ, Measure.count_apply_finite]
63+
erw [uniformOn_univ, Measure.count_apply_finite]
6464

6565
/-- **Birthday Problem**: first probabilistic interpretation. -/
6666
theorem birthday_measure :

‎Archive/Wiedijk100Theorems/Partition.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -329,7 +329,7 @@ theorem partialDistinctGF_prop [CommSemiring α] (n m : ℕ) :
329329
-/
330330
theorem distinctGF_prop [CommSemiring α] (n m : ℕ) (h : n < m + 1) :
331331
((Nat.Partition.distincts n).card : α) = coeff α n (partialDistinctGF m) := by
332-
erw [← partialDistinctGF_prop, Nat.Partition.distincts]
332+
rw [← partialDistinctGF_prop, Nat.Partition.distincts]
333333
congr with p
334334
apply (and_iff_left _).symm
335335
intro i hi

‎Cache/Hashing.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,9 +73,9 @@ def getRootHash : CacheM UInt64 := do
7373
pure id
7474
else
7575
pure ((← mathlibDepPath) / ·)
76-
let hashs ← rootFiles.mapM fun path =>
76+
let hashes ← rootFiles.mapM fun path =>
7777
hashFileContents <$> IO.FS.readFile (qualifyPath path)
78-
return hash (hash Lean.githash :: hashs)
78+
return hash (hash Lean.githash :: hashes)
7979

8080
/--
8181
Computes the hash of a file, which mixes:

‎Counterexamples/CliffordAlgebraNotInjective.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,7 @@ def Q : QuadraticForm K L :=
208208
QuadraticMap.ofPolar
209209
(fun x =>
210210
Quotient.liftOn' x Q' fun a b h => by
211-
rw [Submodule.quotientRel_r_def] at h
211+
rw [Submodule.quotientRel_def] at h
212212
suffices Q' (a - b) = 0 by rwa [Q'_sub, sub_eq_zero] at this
213213
apply Q'_zero_under_ideal (a - b) h)
214214
(fun a x => by

‎Counterexamples/SorgenfreyLine.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ theorem nhds_countable_basis_Ico_inv_pnat (a : ℝₗ) :
110110
theorem nhds_antitone_basis_Ico_inv_pnat (a : ℝₗ) :
111111
(𝓝 a).HasAntitoneBasis fun n : ℕ+ => Ico a (a + (n : ℝₗ)⁻¹) :=
112112
⟨nhds_basis_Ico_inv_pnat a, monotone_const.Ico <| Antitone.const_add
113-
(fun k _l hkl => inv_le_inv_of_le (Nat.cast_pos.2 k.2)
113+
(fun k _l hkl => inv_anti₀ (Nat.cast_pos.2 k.2)
114114
(Nat.mono_cast <| Subtype.coe_le_coe.2 hkl)) _⟩
115115

116116
theorem isOpen_iff {s : Set ℝₗ} : IsOpen s ↔ ∀ x ∈ s, ∃ y > x, Ico x y ⊆ s :=

0 commit comments

Comments
 (0)