{"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:1720708437.0","currentOid":""},"activityList":{"items":[{"before":"4af23afd6672d6841ed2b48406288ec49a07470c","after":"2c86b169dbbab239be689b7c9cc00663462be52f","ref":"refs/heads/YnirPaz/clubs-file","pushedAt":"2024-07-11T14:47:04.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":"feat(SetTheory/Ordinal/Clubs): define club sets and basic properties","shortMessageHtmlLink":"feat(SetTheory/Ordinal/Clubs): define club sets and basic properties"}},{"before":"a469f1b05349a0db26ce24fe01c56b5807dc864d","after":"7afa0a413434bcbb04880ab37f636328f1e87eae","ref":"refs/heads/pullbacks-API","pushedAt":"2024-07-11T14:41:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"callesonne","name":"Calle Sönne","path":"/callesonne","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16383526?s=80&v=4"},"commit":{"message":"merge fix again","shortMessageHtmlLink":"merge fix again"}},{"before":"28832fb4f3896bb5b2da6a8d0fd8bd4365d7bc65","after":"a1ec7ac48c173ec817b5a72b72795362f38852a5","ref":"refs/heads/adomani/endOfLinter_allow_noncomputable","pushedAt":"2024-07-11T14:37:38.000Z","pushType":"push","commitsCount":23,"pusher":{"login":"adomani","name":"damiano","path":"/adomani","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29467745?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/master' into adomani/endOfLinter_allow_noncomputable","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/master' into adomani/endOfLinter…"}},{"before":"6f0c23c8fde707e58896096a0773be0f5795d7e2","after":"e9a50e55aac0d4f59a1844dd91af10d63d5e3349","ref":"refs/heads/adomani/nowhitespacel","pushedAt":"2024-07-11T14:35:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"adomani","name":"damiano","path":"/adomani","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29467745?s=80&v=4"},"commit":{"message":"add lints around brackets","shortMessageHtmlLink":"add lints around brackets"}},{"before":"9273dc1403ce3036d19c47b486fa7e81d3f963a0","after":"6f0c23c8fde707e58896096a0773be0f5795d7e2","ref":"refs/heads/adomani/nowhitespacel","pushedAt":"2024-07-11T14:34:57.000Z","pushType":"push","commitsCount":160,"pusher":{"login":"adomani","name":"damiano","path":"/adomani","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29467745?s=80&v=4"},"commit":{"message":"Merge branch 'master' into adomani/nowhitespacel","shortMessageHtmlLink":"Merge branch 'master' into adomani/nowhitespacel"}},{"before":"8272acb47a9e9a1d8fc322596487b20919e6e3eb","after":null,"ref":"refs/heads/YK-group-sfinite","pushedAt":"2024-07-11T14:33:57.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":"e4e6ef586cf02d472cd98e071653fccd9dd45fd5","after":"33d2c7a16a4141b58f515a3beb2603d11872396a","ref":"refs/heads/master","pushedAt":"2024-07-11T14:33:54.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(MeasureTheory): weaken assumptions from `SigmaFinite` to `SFinite` (#14638)\n\n- Weaken TC assumptions of many lemmas from `SigmaFinite` to `SFinite`.\n- Drop some `MeasurableSet` assumptions.","shortMessageHtmlLink":"feat(MeasureTheory): weaken assumptions from <code>SigmaFinite</code> to `SFinit…"}},{"before":"386d13b13fe1b11ee44141ba27f3286d281ad5be","after":"2fe0c53e6e82965740b84cc346ccef03f791b870","ref":"refs/heads/fiberedcategories_stronglycartesian","pushedAt":"2024-07-11T14:19:46.000Z","pushType":"push","commitsCount":536,"pusher":{"login":"callesonne","name":"Calle Sönne","path":"/callesonne","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16383526?s=80&v=4"},"commit":{"message":"Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into fiberedcategories_stronglycartesian","shortMessageHtmlLink":"Merge branch 'master' of <a href=\"https://github.com/leanprover-community/mathlib4\">https://github.com/leanprover-community/math…</a>"}},{"before":"6c70829d758280cd8a6d8a259e1d13eb80873887","after":null,"ref":"refs/heads/staging.tmp","pushedAt":"2024-07-11T14:18:13.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":"e4e6ef586cf02d472cd98e071653fccd9dd45fd5","after":"33d2c7a16a4141b58f515a3beb2603d11872396a","ref":"refs/heads/staging","pushedAt":"2024-07-11T14:18:13.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(MeasureTheory): weaken assumptions from `SigmaFinite` to `SFinite` (#14638)\n\n- Weaken TC assumptions of many lemmas from `SigmaFinite` to `SFinite`.\n- Drop some `MeasurableSet` assumptions.","shortMessageHtmlLink":"feat(MeasureTheory): weaken assumptions from <code>SigmaFinite</code> to `SFinit…"}},{"before":"6e06ec798071006a50792a37fd4f75ca9ad261af","after":null,"ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-07-11T14:18:13.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":"e4e6ef586cf02d472cd98e071653fccd9dd45fd5","after":"6e06ec798071006a50792a37fd4f75ca9ad261af","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-07-11T14:18:12.000Z","pushType":"push","commitsCount":5,"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-8272acb47a9e9a1d8fc322596487b20919e6e3eb","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-8272acb47a9e9a1d8f…"}},{"before":null,"after":"e4e6ef586cf02d472cd98e071653fccd9dd45fd5","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-07-11T14:18:11.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":"chore: robustify proof in CategoryTheory.Limit.VanKampen (#14635)\n\nDefensive change preparing for https://github.com/leanprover/lean4/pull/4595.","shortMessageHtmlLink":"chore: robustify proof in CategoryTheory.Limit.VanKampen (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2402041607\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/14635\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/14635/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/14635\">#14635</a>)"}},{"before":"b337970bb9aba884633b8c752f742d29c8d3b9b7","after":"6c70829d758280cd8a6d8a259e1d13eb80873887","ref":"refs/heads/staging.tmp","pushedAt":"2024-07-11T14:18:11.000Z","pushType":"push","commitsCount":5,"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-14638","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-14638"}},{"before":"0bc479ab0f41dc7c341b503b97a20c5c65d20da5","after":null,"ref":"refs/heads/robustify_vankmapen","pushedAt":"2024-07-11T14:18:10.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":null,"after":"b337970bb9aba884633b8c752f742d29c8d3b9b7","ref":"refs/heads/staging.tmp","pushedAt":"2024-07-11T14:18:10.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":"110a7888e9a529bc684830746a3e778b85dbf7ee","after":"dbba2de5b7da0fcb9e0ab7920b7cf82b9be21cd6","ref":"refs/heads/eric-wieser/quadratic_form-sum","pushedAt":"2024-07-11T14:18:09.000Z","pushType":"push","commitsCount":335,"pusher":{"login":"eric-wieser","name":"Eric Wieser","path":"/eric-wieser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/425260?s=80&v=4"},"commit":{"message":"Merge branch 'eric-wieser/sym2-lemmas' into eric-wieser/quadratic_form-sum","shortMessageHtmlLink":"Merge branch 'eric-wieser/sym2-lemmas' into eric-wieser/quadratic_for…"}},{"before":"945a24f242964a6df4a4859b8b6a5ec0572e42eb","after":"e4e6ef586cf02d472cd98e071653fccd9dd45fd5","ref":"refs/heads/master","pushedAt":"2024-07-11T14:18:06.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":"chore: robustify proof in CategoryTheory.Limit.VanKampen (#14635)\n\nDefensive change preparing for https://github.com/leanprover/lean4/pull/4595.","shortMessageHtmlLink":"chore: robustify proof in CategoryTheory.Limit.VanKampen (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2402041607\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/14635\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/14635/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/14635\">#14635</a>)"}},{"before":"48efe8cfe20771e1d12d6465d97bd55cb7977915","after":"be4d3a557e1a03e0a79711d9d5e3bd28ae396595","ref":"refs/heads/eric-wieser/sym2-lemmas","pushedAt":"2024-07-11T14:14:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"eric-wieser","name":"Eric Wieser","path":"/eric-wieser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/425260?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":"d55aed06c6fa7223b2ec2ef954bde06f014f38e0","after":"a469f1b05349a0db26ce24fe01c56b5807dc864d","ref":"refs/heads/pullbacks-API","pushedAt":"2024-07-11T14:14:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"callesonne","name":"Calle Sönne","path":"/callesonne","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16383526?s=80&v=4"},"commit":{"message":"another merge mistake","shortMessageHtmlLink":"another merge mistake"}},{"before":null,"after":"3ff288548311e24fade3e48daa8de71f51e72790","ref":"refs/heads/lean-pr-testing-4728","pushedAt":"2024-07-11T14:14:12.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/4728","shortMessageHtmlLink":"Update lean-toolchain for testing <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2403262044\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4728\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4728/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4728\">leanprover/lean4#4728</a>"}},{"before":"252e65218d3695f6a5b446e97e1727860cb59d1d","after":"4bbe4570396328ab6f70fb7175bab953be7a0d51","ref":"refs/heads/igorkhavkine/vitali_convergence_update","pushedAt":"2024-07-11T14:14:11.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"igorkhavkine","name":null,"path":"/igorkhavkine","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/133780155?s=80&v=4"},"commit":{"message":"Merge branch 'igorkhavkine/rpow_inv_lt_iff' into igorkhavkine/vitali_convergence_update","shortMessageHtmlLink":"Merge branch 'igorkhavkine/rpow_inv_lt_iff' into igorkhavkine/vitali_…"}},{"before":"0b546cd2b2e19d07eac8bb644f2e94c3d8629724","after":"d55aed06c6fa7223b2ec2ef954bde06f014f38e0","ref":"refs/heads/pullbacks-API","pushedAt":"2024-07-11T14:09:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"callesonne","name":"Calle Sönne","path":"/callesonne","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16383526?s=80&v=4"},"commit":{"message":"fix merge mistake","shortMessageHtmlLink":"fix merge mistake"}},{"before":"875b5b4d1e9ebe84db1aa2a365b151f469a3a851","after":"e4e6ef586cf02d472cd98e071653fccd9dd45fd5","ref":"refs/heads/staging","pushedAt":"2024-07-11T14:02:12.000Z","pushType":"force_push","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":"chore: robustify proof in CategoryTheory.Limit.VanKampen (#14635)\n\nDefensive change preparing for https://github.com/leanprover/lean4/pull/4595.","shortMessageHtmlLink":"chore: robustify proof in CategoryTheory.Limit.VanKampen (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2402041607\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/14635\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/14635/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/14635\">#14635</a>)"}},{"before":"bc5d6bed7fa70f393d606a28ae117d1fd93e51c9","after":null,"ref":"refs/heads/staging.tmp","pushedAt":"2024-07-11T14:02:12.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":"fb0c3bbc77ba427cc8c44ef2ef2adb432a9c3ca5","after":null,"ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-07-11T14:02:11.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":"945a24f242964a6df4a4859b8b6a5ec0572e42eb","after":"fb0c3bbc77ba427cc8c44ef2ef2adb432a9c3ca5","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-07-11T14:02:11.000Z","pushType":"push","commitsCount":3,"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-0bc479ab0f41dc7c341b503b97a20c5c65d20da5","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-0bc479ab0f41dc7c34…"}},{"before":null,"after":"945a24f242964a6df4a4859b8b6a5ec0572e42eb","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-07-11T14:02:10.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":"chore: add source information to `maintainer merge` Zulip message (#14645)","shortMessageHtmlLink":"chore: add source information to <code>maintainer merge</code> Zulip message (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2402517778\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/14645\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/14645/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/14645\">#1…</a>"}},{"before":"cc72c458826edc316919744d1d1cedb2950f6fb2","after":"bc5d6bed7fa70f393d606a28ae117d1fd93e51c9","ref":"refs/heads/staging.tmp","pushedAt":"2024-07-11T14:02:10.000Z","pushType":"push","commitsCount":3,"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-14635","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-14635"}},{"before":null,"after":"cc72c458826edc316919744d1d1cedb2950f6fb2","ref":"refs/heads/staging.tmp","pushedAt":"2024-07-11T14:02:09.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]"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEfPPLmQA","startCursor":null,"endCursor":null}},"title":"Activity · leanprover-community/mathlib4"}