{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":365697493,"defaultBranch":"master","name":"mathlib4","ownerLogin":"leanprover-community","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-05-09T07:52:01.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/41703605?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1727248214.0","currentOid":""},"activityList":{"items":[{"before":"9279de040545553678ff493ef831ef4efba2ce92","after":"5063953f2838f61cb18f6cc655ee3bbba7aa61f8","ref":"refs/heads/FR_quotlike","pushedAt":"2024-09-25T07:15:19.000Z","pushType":"push","commitsCount":526,"pusher":{"login":"FR-vdash-bot","name":"FR","path":"/FR-vdash-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19634778?s=80&v=4"},"commit":{"message":"universe, docs","shortMessageHtmlLink":"universe, docs"}},{"before":null,"after":"63199d759d268c9d5391bd93fc9e78258db4235d","ref":"refs/heads/MR-nonempty-generalise-proofs","pushedAt":"2024-09-25T07:10:14.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"SPECULATIVE chore(Tactic/GeneraliseProofs): reduce Inhabited to Nonempty\nSeems to work, but need to test this.","shortMessageHtmlLink":"SPECULATIVE chore(Tactic/GeneraliseProofs): reduce Inhabited to Nonempty"}},{"before":null,"after":"8628315c69d0ceff51939a298a2490c232de35df","ref":"refs/heads/MR-fintype-symmFundamental","pushedAt":"2024-09-25T07:09:15.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"chore(Symmetric/FundamentalTheorem): omit unused Fintype assumption","shortMessageHtmlLink":"chore(Symmetric/FundamentalTheorem): omit unused Fintype assumption"}},{"before":"d7bb26a5f9ccafbb4618d0d50a59659562c2c760","after":"2d16f345206338113667c85822894da34795b9d8","ref":"refs/heads/MR-setoption-autoImplicit","pushedAt":"2024-09-25T07:07:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"Don't lint mathlib's test directory.","shortMessageHtmlLink":"Don't lint mathlib's test directory."}},{"before":"a920bf2fa85a8f1153c3b42a45f11aa36cd9dc42","after":"d7bb26a5f9ccafbb4618d0d50a59659562c2c760","ref":"refs/heads/MR-setoption-autoImplicit","pushedAt":"2024-09-25T07:03:05.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"Cleaner linter.","shortMessageHtmlLink":"Cleaner linter."}},{"before":"5ddf5ecc7e73d575347f1a855484243bed3a3aa2","after":"5c8a35dcad942f42dd8cb5c0be4ff9de0d4cc8c5","ref":"refs/heads/lean-pr-testing-5464","pushedAt":"2024-09-25T06:59:15.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"kim-em","name":"Kim Morrison","path":"/kim-em","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/477956?s=80&v=4"},"commit":{"message":"bump batteries for leanprover/lean4#5464","shortMessageHtmlLink":"bump batteries for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2547025178\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5464\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5464/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5464\">leanprover/lean4#5464</a>"}},{"before":"7bfb69ec0f874864f3d56261d4d4b621451d2cbe","after":"db0c3d26c6b9d3de17ec31896dea718da927c8e8","ref":"refs/heads/YK-no-roots","pushedAt":"2024-09-25T06:56:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Fix","shortMessageHtmlLink":"Fix"}},{"before":"ab53fa9197f1218acc07c09a3f784aaf4fbdcf49","after":null,"ref":"refs/heads/staging.tmp","pushedAt":"2024-09-25T06:53:50.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"}},{"before":"f7eb186981d26df6a660ad65bc92771d8bcf146b","after":"2f407c34aa1095d5b89ccdba28582291f9b6c16e","ref":"refs/heads/staging","pushedAt":"2024-09-25T06:53:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"feat: `match_scalars` and `module` tactics (#16593)\n\nThis PR contributes two new tactics `match_scalars` and `module`.\r\n\r\nGiven a goal which is an equality in a type `M` (with `M` an `AddCommMonoid`), the `match_scalars` tactic parses the LHS and RHS of the goal as linear combinations of `M`-atoms over some semiring `R`, and reduces the goal to the respective equalities of the `R`-coefficients of each atom.\r\n\r\nFor example, this produces the goal `⊢ a * 1 + b * 1 = (b + a) * 1`:\r\n```lean\r\nexample [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :\r\n    a • x + b • x = (b + a) • x := by\r\n  match_scalars\r\n```\r\nThis produces the two goals `⊢ a * (a * 1) + b * (b * 1) = 1` (from the `x` atom) and\r\n`⊢ a * -(b * 1) + b * (a * 1) = 0` (from the `y` atom):\r\n```lean\r\nexample [AddCommGroup M] [Ring R] [Module R M] (a b : R) (x : M) :\r\n    a • (a • x - b • y) + (b • a • y + b • b • x) = x := by\r\n  match_scalars\r\n```\r\n\r\nThe `module` tactic runs the `match_scalars` tactic and then runs the `ring` tactic on each of the coefficient-wise equalities which are created, failing if this does not resolve them.  For example, it solves the following goals:\r\n```lean\r\nexample [AddCommMonoid M] [CommSemiring R] [Module R M] (a b : R) (x : M) :\r\n    a • x + b • x = (b + a) • x := by\r\n  module\r\n\r\nexample [AddCommMonoid M] [Field K] [CharZero K] [Module K M] (x : M) :\r\n    (2:K)⁻¹ • x + (3:K)⁻¹ • x + (6:K)⁻¹ • x = x := by\r\n  module\r\n\r\nexample [AddCommGroup M] [CommRing R] [Module R M] (a : R) (v w : M) :\r\n    (1 + a ^ 2) • (v + w) - a • (a • v - w) = v + (1 + a + a ^ 2) • w := by\r\n  module\r\n```\r\nThe scalar type `R` in these tactics is not pre-determined: instead it starts as `ℕ` (when each atom is initially given a scalar `(1:ℕ)`) and gets bumped up into bigger semirings when such semirings are encountered.  However, to permit this, it is assumed that there is a \"linear order\" on all the semirings which appear in the expression: for any two semirings `R` and `S` which occur, we have either `Algebra R S` or `Algebra S R`).\r\n\r\n\n\nCo-authored-by: Eric Wieser <wieser.eric@gmail.com>","shortMessageHtmlLink":"feat: <code>match_scalars</code> and <code>module</code> tactics (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2512108928\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/16593\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/16593/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/16593\">#16593</a>)"}},{"before":"add05d2641f30da5bbf4db828e5654cdd84c3e66","after":null,"ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-09-25T06:53:49.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"}},{"before":"f7eb186981d26df6a660ad65bc92771d8bcf146b","after":"add05d2641f30da5bbf4db828e5654cdd84c3e66","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-09-25T06:53:49.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-861880545d7159ab883fe52c65e2e9ffc38e3c18","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-861880545d7159ab88…"}},{"before":null,"after":"f7eb186981d26df6a660ad65bc92771d8bcf146b","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-09-25T06:53:48.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"fix: remove non-breaking-space (#17116)\n\nReplace more non-breaking-spaces with regular spaces","shortMessageHtmlLink":"fix: remove non-breaking-space (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2546582794\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/17116\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/17116/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/17116\">#17116</a>)"}},{"before":"a68aefbe3c932ea6d8b1f03f1c3647e0f71458aa","after":"ab53fa9197f1218acc07c09a3f784aaf4fbdcf49","ref":"refs/heads/staging.tmp","pushedAt":"2024-09-25T06:53:47.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-16593","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-16593"}},{"before":null,"after":"a68aefbe3c932ea6d8b1f03f1c3647e0f71458aa","ref":"refs/heads/staging.tmp","pushedAt":"2024-09-25T06:53:46.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify]","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify]"}},{"before":"d8d4f99612e157eb958f0a1577a02fabfa81bbad","after":"7bfb69ec0f874864f3d56261d4d4b621451d2cbe","ref":"refs/heads/YK-no-roots","pushedAt":"2024-09-25T06:52:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Shake","shortMessageHtmlLink":"Shake"}},{"before":"9517975bb7b559a5c68c55bc8dc9442e6a788c75","after":"9a1baea0d8bdeb8feccca3995fb9f249b7455130","ref":"refs/heads/YnirPaz/mk_sigma_congr","pushedAt":"2024-09-25T06:50:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"YnirPaz","name":null,"path":"/YnirPaz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/126973178?s=80&v=4"},"commit":{"message":"fix merge","shortMessageHtmlLink":"fix merge"}},{"before":null,"after":"5ddf5ecc7e73d575347f1a855484243bed3a3aa2","ref":"refs/heads/lean-pr-testing-5464","pushedAt":"2024-09-25T06:45:02.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/5464","shortMessageHtmlLink":"Update lean-toolchain for testing <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2547025178\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5464\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5464/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5464\">leanprover/lean4#5464</a>"}},{"before":"16d9b0e4124e8ff2691d27e7e16b4b9cedf1952d","after":"9517975bb7b559a5c68c55bc8dc9442e6a788c75","ref":"refs/heads/YnirPaz/mk_sigma_congr","pushedAt":"2024-09-25T06:43:35.000Z","pushType":"push","commitsCount":167,"pusher":{"login":"YnirPaz","name":null,"path":"/YnirPaz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/126973178?s=80&v=4"},"commit":{"message":"Merge branch 'master' into YnirPaz/mk_sigma_congr","shortMessageHtmlLink":"Merge branch 'master' into YnirPaz/mk_sigma_congr"}},{"before":"ec2c8b8038e585cce908d25146ee2ef5f2b10ca9","after":"4664aee1a521325e319f4ff157094d0d5c6f0868","ref":"refs/heads/Nir/out_lift_equiv","pushedAt":"2024-09-25T06:39:02.000Z","pushType":"push","commitsCount":118,"pusher":{"login":"YnirPaz","name":null,"path":"/YnirPaz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/126973178?s=80&v=4"},"commit":{"message":"merge","shortMessageHtmlLink":"merge"}},{"before":"0cf91d23004a46977d7ea2ce4f00ea28704a16ac","after":"7ec3480f6bedd4aad326c706cc06e5549c01001d","ref":"refs/heads/lean-pr-testing-5463","pushedAt":"2024-09-25T06:36:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"kim-em","name":"Kim Morrison","path":"/kim-em","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/477956?s=80&v=4"},"commit":{"message":"fixes for leanprover/lean4#5463","shortMessageHtmlLink":"fixes for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2546995033\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5463\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5463/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5463\">leanprover/lean4#5463</a>"}},{"before":"d3a99369ff6eb3935b1dc03ad44cd92582de10d1","after":"141ab0f4045e99b4910d53bfbe13df77b52339b5","ref":"refs/heads/mans0954/absconvexhull","pushedAt":"2024-09-25T06:27:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mans0954","name":"Christopher Hoskin","path":"/mans0954","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4855578?s=80&v=4"},"commit":{"message":"Tidy argument","shortMessageHtmlLink":"Tidy argument"}},{"before":"6144bd1fec57b4c76a2f13a023a21018df777b96","after":"d3a99369ff6eb3935b1dc03ad44cd92582de10d1","ref":"refs/heads/mans0954/absconvexhull","pushedAt":"2024-09-25T06:16:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mans0954","name":"Christopher Hoskin","path":"/mans0954","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4855578?s=80&v=4"},"commit":{"message":"Balanced.hullAdd","shortMessageHtmlLink":"Balanced.hullAdd"}},{"before":"d0b4f4e2170a246fc09f6e3544bfe2b74c20426c","after":"6144bd1fec57b4c76a2f13a023a21018df777b96","ref":"refs/heads/mans0954/absconvexhull","pushedAt":"2024-09-25T06:15:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mans0954","name":"Christopher Hoskin","path":"/mans0954","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4855578?s=80&v=4"},"commit":{"message":"AbsConvex.hullAdd","shortMessageHtmlLink":"AbsConvex.hullAdd"}},{"before":"4fce95c5352084fe343788fb7f3ec94819f92e87","after":"e39388412761336a4845b8d2105182247b0a5041","ref":"refs/heads/mans0954/Banach-Dieudonne-lemma","pushedAt":"2024-09-25T06:11:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mans0954","name":"Christopher Hoskin","path":"/mans0954","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4855578?s=80&v=4"},"commit":{"message":"AbsConvex.hullAdd","shortMessageHtmlLink":"AbsConvex.hullAdd"}},{"before":"8f18d4e37b8db7372c03e67d25f976f496b9af6f","after":"16d9b0e4124e8ff2691d27e7e16b4b9cedf1952d","ref":"refs/heads/YnirPaz/mk_sigma_congr","pushedAt":"2024-09-25T06:10:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"YnirPaz","name":null,"path":"/YnirPaz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/126973178?s=80&v=4"},"commit":{"message":"lift versions","shortMessageHtmlLink":"lift versions"}},{"before":null,"after":"0cf91d23004a46977d7ea2ce4f00ea28704a16ac","ref":"refs/heads/lean-pr-testing-5463","pushedAt":"2024-09-25T06:10:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/5463","shortMessageHtmlLink":"Update lean-toolchain for testing <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2546995033\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5463\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5463/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5463\">leanprover/lean4#5463</a>"}},{"before":"945a2fc3355b40f1b381cc46dd65cb9856dbf55e","after":"4fce95c5352084fe343788fb7f3ec94819f92e87","ref":"refs/heads/mans0954/Banach-Dieudonne-lemma","pushedAt":"2024-09-25T05:58:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mans0954","name":"Christopher Hoskin","path":"/mans0954","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4855578?s=80&v=4"},"commit":{"message":"Balanced.hullAdd","shortMessageHtmlLink":"Balanced.hullAdd"}},{"before":"dc056cb8f834008ea4f89448b63c7cb8810a4073","after":"1068c188bd8a0c47ea2b16e6e90c212c758b1137","ref":"refs/heads/ira/OrdinalApprox_monos","pushedAt":"2024-09-25T05:39:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PhoenixIra","name":"Ira Fesefeldt","path":"/PhoenixIra","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9974411?s=80&v=4"},"commit":{"message":"comments","shortMessageHtmlLink":"comments"}},{"before":"7cd815a13a090a62d103a7d6afafb4a0a3a47a14","after":"689cf2d6a8a8d8f5c20be2975eb8677207d4fc3c","ref":"refs/heads/tfae-have-deprecate","pushedAt":"2024-09-25T05:06:44.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"thorimur","name":null,"path":"/thorimur","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/68410468?s=80&v=4"},"commit":{"message":"chore: fix hovers","shortMessageHtmlLink":"chore: fix hovers"}},{"before":null,"after":"26a2732b1999aabf30c115028f1fe106d689b856","ref":"refs/heads/lean-pr-testing-5462","pushedAt":"2024-09-25T04:41:29.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/5462","shortMessageHtmlLink":"Update lean-toolchain for testing <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2546863351\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5462\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5462/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5462\">leanprover/lean4#5462</a>"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yNVQwNzoxNToxOS4wMDAwMDBazwAAAAS_-0D_","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yNVQwNzoxNToxOS4wMDAwMDBazwAAAAS_-0D_","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yNVQwNDo0MToyOS4wMDAwMDBazwAAAAS_3zoa"}},"title":"Activity · leanprover-community/mathlib4"}