Skip to content

Commit 1362a3a

Browse files
eric-wiesereric-wieser
committed
Merge commit 'f25139b758e258bad4af67c9e503d4ed82dfd65a' into mans0954/non-assoc-star-mul
2 parents 6afc5de + f25139b commit 1362a3a

File tree

1,075 files changed

+11669
-4280
lines changed

Some content is hidden

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

1,075 files changed

+11669
-4280
lines changed

‎.github/workflows/bors.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -187,3 +187,14 @@ jobs:
187187
curl --request DELETE \
188188
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
189189
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
190+
191+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
192+
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
193+
uses: GrantBirki/[email protected]
194+
with:
195+
token: ${{ secrets.AUTO_MERGE_TOKEN }}
196+
issue-number: ${{ steps.PR.outputs.number }}
197+
body: |
198+
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
199+
200+
bors merge

‎.github/workflows/build.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,3 +193,14 @@ jobs:
193193
curl --request DELETE \
194194
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
195195
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
196+
197+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
198+
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
199+
uses: GrantBirki/[email protected]
200+
with:
201+
token: ${{ secrets.AUTO_MERGE_TOKEN }}
202+
issue-number: ${{ steps.PR.outputs.number }}
203+
body: |
204+
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
205+
206+
bors merge

‎.github/workflows/build.yml.in‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -173,3 +173,14 @@ jobs:
173173
curl --request DELETE \
174174
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
175175
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
176+
177+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
178+
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
179+
uses: GrantBirki/[email protected]
180+
with:
181+
token: ${{ secrets.AUTO_MERGE_TOKEN }}
182+
issue-number: ${{ steps.PR.outputs.number }}
183+
body: |
184+
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
185+
186+
bors merge

‎.github/workflows/build_fork.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,3 +191,14 @@ jobs:
191191
curl --request DELETE \
192192
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
193193
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
194+
195+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
196+
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
197+
uses: GrantBirki/[email protected]
198+
with:
199+
token: ${{ secrets.AUTO_MERGE_TOKEN }}
200+
issue-number: ${{ steps.PR.outputs.number }}
201+
body: |
202+
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
203+
204+
bors merge

‎Archive/Imo/Imo1988Q6.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -207,7 +207,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
207207
hk (fun x => k * x) (fun x => x * x - k) fun _ _ => False <;>
208208
clear hk a b
209209
· -- We will now show that the fibers of the solution set are described by a quadratic equation.
210-
intro x y; dsimp only
210+
intro x y
211211
rw [← Int.coe_nat_inj', ← sub_eq_zero]
212212
apply eq_iff_eq_cancel_right.2
213213
simp; ring
@@ -265,7 +265,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
265265
hk (fun x => k * x) (fun x => x * x + 1) fun x _ => x ≤ 1 <;>
266266
clear hk a b
267267
· -- We will now show that the fibers of the solution set are described by a quadratic equation.
268-
intro x y; dsimp only
268+
intro x y
269269
rw [← Int.coe_nat_inj', ← sub_eq_zero]
270270
apply eq_iff_eq_cancel_right.2
271271
simp; ring

‎Archive/Sensitivity.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -399,7 +399,6 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
399399
let W := Span (e '' H)
400400
let img := range (g m)
401401
suffices 0 < dim (W ⊓ img) by
402-
simp only [exists_prop]
403402
exact_mod_cast exists_mem_ne_zero_of_rank_pos this
404403
have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1) := by
405404
convert ← rank_submodule_le (W ⊔ img)

‎Archive/Wiedijk100Theorems/BallotProblem.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,7 @@ theorem first_vote_pos :
242242
exact subset_union_left _ _
243243
rw [(condCount_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, condCount,
244244
cond_apply _ list_int_measurableSet, hint, count_injective_image List.cons_injective,
245-
count_countedSequence, count_countedSequence, one_mul, MulZeroClass.zero_mul, add_zero,
245+
count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
246246
Nat.cast_add, Nat.cast_one]
247247
· rw [mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
248248
· norm_cast

‎Archive/Wiedijk100Theorems/FriendshipGraphs.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ theorem adjMatrix_sq_of_ne {v w : V} (hvw : v ≠ w) :
9393
We use it to show that nonadjacent vertices have equal degrees. -/
9494
theorem adjMatrix_pow_three_of_not_adj {v w : V} (non_adj : ¬G.Adj v w) :
9595
(G.adjMatrix R ^ 3 : Matrix V V R) v w = degree G v := by
96-
rw [pow_succ, mul_eq_mul, adjMatrix_mul_apply, degree, card_eq_sum_ones, Nat.cast_sum]
96+
rw [pow_succ, adjMatrix_mul_apply, degree, card_eq_sum_ones, Nat.cast_sum]
9797
apply sum_congr rfl
9898
intro x hx
9999
rw [adjMatrix_sq_of_ne _ hG, Nat.cast_one]
@@ -114,8 +114,8 @@ theorem degree_eq_of_not_adj {v w : V} (hvw : ¬G.Adj v w) : degree G v = degree
114114
← adjMatrix_pow_three_of_not_adj ℕ hG hvw,
115115
← adjMatrix_pow_three_of_not_adj ℕ hG fun h => hvw (G.symm h)]
116116
conv_lhs => rw [← transpose_adjMatrix]
117-
simp only [pow_succ _ 2, sq, mul_eq_mul, ← transpose_mul, transpose_apply]
118-
simp only [← mul_eq_mul, mul_assoc]
117+
simp only [pow_succ _ 2, sq, ← transpose_mul, transpose_apply]
118+
simp only [mul_assoc]
119119
#align theorems_100.friendship.degree_eq_of_not_adj Theorems100.Friendship.degree_eq_of_not_adj
120120

121121
/-- Let `A` be the adjacency matrix of a graph `G`.
@@ -125,7 +125,7 @@ theorem degree_eq_of_not_adj {v w : V} (hvw : ¬G.Adj v w) : degree G v = degree
125125
theorem adjMatrix_sq_of_regular (hd : G.IsRegularOfDegree d) :
126126
G.adjMatrix R ^ 2 = of fun v w => if v = w then (d : R) else (1 : R) := by
127127
ext (v w); by_cases h : v = w
128-
· rw [h, sq, mul_eq_mul, adjMatrix_mul_self_apply_self, hd]; simp
128+
· rw [h, sq, adjMatrix_mul_self_apply_self, hd]; simp
129129
· rw [adjMatrix_sq_of_ne R hG h, of_apply, if_neg h]
130130
#align theorems_100.friendship.adj_matrix_sq_of_regular Theorems100.Friendship.adjMatrix_sq_of_regular
131131

@@ -184,7 +184,7 @@ theorem card_of_regular (hd : G.IsRegularOfDegree d) : d + (Fintype.card V - 1)
184184
Ne.def, not_false_iff, add_right_inj, false_and_iff, of_apply]
185185
rw [Finset.sum_const_nat, card_erase_of_mem (mem_univ v), mul_one]; · rfl
186186
intro x hx; simp [(ne_of_mem_erase hx).symm]
187-
· rw [sq, mul_eq_mul, ← mulVec_mulVec]
187+
· rw [sq, ← mulVec_mulVec]
188188
simp only [adjMatrix_mulVec_const_apply_of_regular hd, neighborFinset,
189189
card_neighborSet_eq_degree, hd v, Function.const_def, adjMatrix_mulVec_apply _ _ (mulVec _ _),
190190
mul_one, sum_const, Set.toFinset_card, Algebra.id.smul_eq_mul, Nat.cast_id]
@@ -206,7 +206,7 @@ end Nonempty
206206
theorem adjMatrix_sq_mul_const_one_of_regular (hd : G.IsRegularOfDegree d) :
207207
G.adjMatrix R * of (fun _ _ => 1) = of (fun _ _ => (d : R)) := by
208208
ext x
209-
simp only [← hd x, degree, mul_eq_mul, adjMatrix_mul_apply, sum_const, Nat.smul_one_eq_coe,
209+
simp only [← hd x, degree, adjMatrix_mul_apply, sum_const, Nat.smul_one_eq_coe,
210210
of_apply]
211211
#align theorems_100.friendship.adj_matrix_sq_mul_const_one_of_regular Theorems100.Friendship.adjMatrix_sq_mul_const_one_of_regular
212212

‎Archive/Wiedijk100Theorems/Partition.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ theorem num_series' [Field α] (i : ℕ) :
289289
rw [Nat.mul_sub_left_distrib, ← hp, ← a_left, mul_one, Nat.add_sub_cancel]
290290
· rintro ⟨rfl, rfl⟩
291291
match p with
292-
| 0 => rw [MulZeroClass.mul_zero] at hp; cases hp
292+
| 0 => rw [mul_zero] at hp; cases hp
293293
| p + 1 => rw [hp]; simp [mul_add]
294294
· suffices
295295
(filter (fun a : ℕ × ℕ => i + 1 ∣ a.fst ∧ a.snd = i + 1) (Nat.antidiagonal n.succ)).card =

‎Cache/Hashing.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Arthur Paulino
66

77
import Cache.IO
88
import Lean.Elab.ParseImportsFast
9+
import Lake.Build.Trace
910

1011
namespace Cache.Hashing
1112

@@ -52,7 +53,7 @@ def getFileImports (source : String) (pkgDirs : PackageDirs) : Array FilePath :=
5253
/-- Computes a canonical hash of a file's contents. -/
5354
def hashFileContents (contents : String) : UInt64 :=
5455
-- revert potential file transformation by git's `autocrlf`
55-
let contents := contents.replace "\r\n" "\n"
56+
let contents := Lake.crlf2lf contents
5657
hash contents
5758

5859
/--

0 commit comments

Comments
 (0)