Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
commit 8377ae6b176cc857b383b04173fa5577d09f1689 Author: Matthew Ballard <[email protected]> Date: Wed May 17 21:16:04 2023 -0400 update mathlib.lean commit 8d909eb33ad5e164db2deaf8444b0a21351ec99f Author: Matthew Ballard <[email protected]> Date: Wed May 17 21:14:55 2023 -0400 lint commit 6bcb7f5e70763e15c405912988d867fbe0637691 Author: Matthew Ballard <[email protected]> Date: Wed May 17 21:10:16 2023 -0400 fix last errors commit 1b85bed8887c82368d7da6f4189aea86e98991cb Author: Scott Morrison <[email protected]> Date: Thu May 18 10:46:42 2023 +1000 fixes commit 519af1d828205304827466024ee65506eb99186e Merge: 98bf9f9b 8bf78812 Author: Scott Morrison <[email protected]> Date: Thu May 18 09:09:10 2023 +1000 Merge remote-tracking branch 'origin/master' into port/CategoryTheory.Bicategory.Free commit 98bf9f9b293dfe099a631c3bda0bd5e493a7d49e Merge: 1910c612 f9ae3115 Author: Matthew Ballard <[email protected]> Date: Sat May 13 08:31:30 2023 -0400 Merge branch 'master' into port/CategoryTheory.Bicategory.Free commit 1910c612e2e43e3c263f68996ed72b9ac5204f6e Author: Matthew Ballard <[email protected]> Date: Sat May 13 08:31:19 2023 -0400 add new file commit 7af7463b52e7a6d69eb7478235117c023ec8c6aa Merge: f0adc533 269fb63e Author: Matthew Ballard <[email protected]> Date: Sat May 13 08:29:53 2023 -0400 Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.Bicategory.Free' into port/CategoryTheory.Bicategory.Free commit 269fb63e9215d34da56d0b4a7288aca3bde89bc0 Author: Jason Yuen <[email protected]> Date: Wed May 10 05:02:09 2023 +0000 feat: port Analysis.Normed.Group.ControlledClosure (#3880) commit 628125292856eb71f72eeecd4f5f967f006ec773 Author: Kevin Buzzard <[email protected]> Date: Wed May 10 05:02:09 2023 +0000 feat: add some `pp_extended_field_notation`s (#3592) Add some `pp_extended_field_notation`, for opt-in cases with additional arguments. Co-authored-by: Kyle Miller <[email protected]> commit 21708212ef62b7ac824871864a8c3d103f320750 Author: Jason Yuen <[email protected]> Date: Wed May 10 04:45:22 2023 +0000 feat: port Topology.ContinuousFunction.LocallyConstant (#3877) commit 5d84f9b67af72c588b96bb7821b2523f821b1bec Author: Jason Yuen <[email protected]> Date: Wed May 10 01:01:27 2023 +0000 feat: port MeasureTheory.Covering.VitaliFamily (#3867) commit 4f3e6145116f5ddf98f9f2615f7e4b129bd02dce Author: Matthew Robert Ballard <[email protected]> Date: Wed May 10 01:01:26 2023 +0000 feat: port Algebra.Category.Group.EquivalenceGroupAddGroup (#3861) commit 0d738a8fef346fb7f9020b327b61fe7f422d1524 Author: Pol_tta <[email protected]> Date: Wed May 10 01:01:24 2023 +0000 feat: port Dynamics.Ergodic.MeasurePreserving (#3821) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: MonadMaverick <[email protected]> commit 9c00193316232966719be6916399504da82103c7 Author: Pol_tta <[email protected]> Date: Wed May 10 01:01:22 2023 +0000 feat: port MeasureTheory.Measure.OpenPos (#3820) Co-authored-by: Komyyy <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit 55413d4565e6e33a8ff7065b20a3f3f9ba18fc0d Author: Jason Yuen <[email protected]> Date: Wed May 10 00:18:41 2023 +0000 feat: port Analysis.Convex.PartitionOfUnity (#3868) commit 468ee3fa8c1a4a81a0a1ce5829afc0e65226ea97 Author: Pol_tta <[email protected]> Date: Wed May 10 00:18:39 2023 +0000 feat: port MeasureTheory.Lattice (#3824) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: MonadMaverick <[email protected]> commit 01d44eab0e102b78434bd20142f8e1db75e22599 Author: Pol_tta <[email protected]> Date: Wed May 10 00:18:37 2023 +0000 feat: port MeasureTheory.Measure.MutuallySingular (#3818) Co-authored-by: Komyyy <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit 3b3411e0739d9a22e8cabc54b724123a8d773333 Author: Kyle Miller <[email protected]> Date: Wed May 10 00:18:35 2023 +0000 feat: pp_extended_field_notation command to pretty print with dot notation (#3811) The projection notation delaborator that comes from core Lean has some limitations. We introduce a new projection notation delaborator that is able to collapse parent projection sequences, for example `x.toC.toB.toA.val` into `x.val`. The other limitation of the delaborator is that it can only handle true projections that do not have any additional arguments. This commit adds a `pp_extended_field_notation` command to switch on projection notation for specific functions. This command defines app unexpanders that pretty print that function application using dot notation. The app unexpander it produces has a small hack to completely collapse parent projection sequences. Since it is an app unexpander, we do not have access to the actual types, so we use a heuristic that, for example with `A.foo`, if we are looking at `A.foo x.toA y z ...` then we can pretty print this as `x.foo y z`. The projection delaborator is able to collapse parent projection sequences except for the vary last one, so this finishes it off. Note that this heuristic can lead to output that does not round trip if there is a `toA` function that is not a parent projection that happens to be pretty printed with dot notation. commit 7341d34cb0b1173f04f03c7f51daea36a230e35c Author: David Loeffler <[email protected]> Date: Tue May 9 23:59:30 2023 +0000 feat: port Analysis.NormedSpace.CompactOperator (#3805) commit c10b02b9f02a8d212f1ab2cdd18440785e464c58 Author: Scott Morrison <[email protected]> Date: Tue May 9 23:06:55 2023 +0000 feat: port CategoryTheory.Functor.Flat (#3703) Co-authored-by: Kevin Buzzard <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Yaël Dillies <[email protected]> commit 64b7fb14e6a9085f2a3e6fa5bcce317a7120cc3a Author: Pol_tta <[email protected]> Date: Tue May 9 19:44:35 2023 +0000 feat: port MeasureTheory.Measure.AEMeasurable (#3819) Co-authored-by: Komyyy <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit 15da6c20b0e9b06b46b5c6b325f7d21be2d568b7 Author: Jason Yuen <[email protected]> Date: Tue May 9 10:06:14 2023 +0000 feat: port Probability.ProbabilityMassFunction.Basic (#3865) commit 8ecbd9569ffd605712cd21b65d0d8864520dfb66 Author: Matthew Robert Ballard <[email protected]> Date: Tue May 9 10:06:13 2023 +0000 feat: port CategoryTheory.Preadditive.InjectiveResolution (#3860) Co-authored-by: Matthew Robert Ballard <[email protected]> commit da3993ff939d796018ff5e95c41712d1975abfa8 Author: Matthew Robert Ballard <[email protected]> Date: Tue May 9 10:06:12 2023 +0000 feat: port Topology.Category.Top.Limits.Konig (#3853) Co-authored-by: Matthew Robert Ballard <[email protected]> commit c3bace0cd04c23c1dd9ab361b03eb80faa8e2c3d Author: Jason Yuen <[email protected]> Date: Tue May 9 09:46:42 2023 +0000 feat: port MeasureTheory.Measure.Sub (#3866) commit 99bb9fb7ca74cba20b2c2588d2fb9595e5cb98b7 Author: Xavier Roblot <[email protected]> Date: Tue May 9 08:58:57 2023 +0000 feat port: LinearAlgebra.ProjectiveSpace.Subspace (#3832) commit f273bff58209ed6273afcaf85b7bc554a7ceac3a Author: Ruben Van de Velde <[email protected]> Date: Tue May 9 06:29:09 2023 +0000 chore: tidy various files (#3848) commit cfbec6e28f4c3d117debf58d1338e531cb90a3aa Author: Jason Yuen <[email protected]> Date: Tue May 9 06:12:54 2023 +0000 feat: port Topology.PartitionOfUnity (#3863) commit 37807d6a99a0199676e029358f20ac5738d9639f Author: Matthew Robert Ballard <[email protected]> Date: Tue May 9 06:12:53 2023 +0000 feat: port CategoryTheory.Preadditive.Injective (#3859) commit b75c4d73f2b15b8234a5dcdca62ad160ae9caf76 Author: Matthew Robert Ballard <[email protected]> Date: Tue May 9 06:12:52 2023 +0000 feat: port Topology.Category.Top.Limits.Cofiltered (#3855) commit b1ee18a7fb8e0079cb0c0fd0fea1afd019219fe5 Author: David Renshaw <[email protected]> Date: Tue May 9 06:12:51 2023 +0000 fix: remove unneeded LibrarySearch import (#3854) Removes from `Analysis/SpecificLimits/Normed.lean` an `import Mathlib.Tactic.LibrarySearch` that was accidentally included in #3419. commit 4ddbf238481366ca34965e9d10278833f01a3e70 Author: MonadMaverick <[email protected]> Date: Tue May 9 05:50:38 2023 +0000 feat: port MeasureTheory.Measure.MeasureSpace (#3324) This PR also renames instances in `MeasureTheory.MeasurableSpace`. Co-authored-by: Komyyy <[email protected]> Co-authored-by: ChrisHughes24 <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit d52008fd7cc8539b1d1b32c9eac2b0aeac276244 Author: Eric Wieser <[email protected]> Date: Mon May 8 22:44:20 2023 +0000 fix: make `ConcreteCategory.Forget` reducible (#3857) This seems to help in downstream files, [See Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20inference.20not.20seeing.20through.20reducible.20definition/near/356130343) commit a627d110cd7b94a4308c2c71a46f9ed44930bb97 Author: Christopher Hoskin <[email protected]> Date: Mon May 8 21:09:37 2023 +0000 feat: port Topology.ContinuousFunction.Algebra (#3332) Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Ruben Van de Velde <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> Co-authored-by: qawbecrdtey <[email protected]> Co-authored-by: Jireh Loreaux <[email protected]> commit 6863ef07ca5aa72edacb87d14977f8816aa3951d Author: sgouezel <[email protected]> Date: Mon May 8 19:26:28 2023 +0000 chore(*): tweak priorities for linear algebra (#3840) We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`. commit a25c78e5c93a3217b9ee46882955746f08469791 Author: Scott Morrison <[email protected]> Date: Mon May 8 13:36:25 2023 +0000 chore: fix name in Mathlib.Topology.Algebra.Module (#3850) Co-authored-by: Scott Morrison <[email protected]> commit 51e2e32cd407e1965885af13d1a9bb96e0709c05 Author: Xavier Roblot <[email protected]> Date: Mon May 8 11:53:12 2023 +0000 feat port: Topology.Algebra.Nonarchimedean.AdicTopology (#3826) commit a5f2b200a2c1fb019a358e347353e19f09402bd5 Author: Jason Yuen <[email protected]> Date: Mon May 8 11:21:34 2023 +0000 feat: port Data.Complex.Orientation (#3849) commit 2906eb7cfd4f8b36322c63e0209c06e0353a5261 Author: Pol_tta <[email protected]> Date: Mon May 8 10:01:09 2023 +0000 feat: port MeasureTheory.Tactic (#3816) commit b5c7cda33ead3895a3e92b9b41112bdc755a433a Author: Jujian Zhang <[email protected]> Date: Mon May 8 09:17:50 2023 +0000 feat: definition of krull dimension for a preordered set (#3704) Given a preordered set $(S, <)$, the krull dimension of $S$ is defined to be $\sup\{n | a_0 < a_1 < ... < a_n\}$ where the supremum takes place in extended natural numbers $\mathbb N \cup \{\pm \infty\}$, i.e. empty set is negative-infinite dimensional and a set with arbitrary long $a_0 < a_1 < ... < a_n$ is positive dimensional. Similar constructions in mathlib does require a chain to be nonempty so that empty set would have the wrong dimension, so I defined a new structure `StrictSeries` to avoid confusion with `chain`; in this structure, the underlying list is always nonempty. commit 8685958b7012efbeb848057bc4b936aaa4c39b63 Author: Pol_tta <[email protected]> Date: Mon May 8 05:55:43 2023 +0000 fix: remove lambda abstraction of `Nat.rec_zero` and `Nat.rec_add_one` (#3839) ```lean theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : (Nat.rec h0 h : ∀ n, C n) 0 = h0 := rfl ``` The above theorem is elaborated as follow: ```lean theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : (fun n => Nat.rec h0 h n) 0 = h0 := rfl ``` This form of the theorem isn't generic. This PR fixes this problem. Co-authored-by: Pol_tta <[email protected]> commit b840606e7074798762c81e73e53ac4ab2e661de5 Author: Xavier Roblot <[email protected]> Date: Mon May 8 05:55:41 2023 +0000 feat port: LinearAlgebra.Orientation (#3777) I had to add a bunch of `set_option synthInstance.etaExperiment true`, `set_option maxHeartbeats` and `set_option synthInstance.maxHeartbeats` to this file I tried to use the methods described in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/maxHeartbeats/near/356217898) to remove some of the `maxHeartbeats` but I was not successful. Co-authored-by: Scott Morrison <[email protected]> commit 882005842a71af115186357b21dd4f2bbfe2a597 Author: Jason Yuen <[email protected]> Date: Mon May 8 05:55:40 2023 +0000 feat: port Analysis.SpecificLimits.Normed (#3419) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit c2cf5ba958fb0ac9b1536f66d98b73a486aabaee Author: Pol_tta <[email protected]> Date: Mon May 8 03:29:54 2023 +0000 fix: `lift` can't be used when the type of the goal is `Sort.{?u}` while `?u` is assigned by `0` (#3800) For example, this emits error. ```lean example (n : ℕ) : n = 0 ∨ ∃ p : ℕ+, n = p := by by_cases hn : 0 < n · lift n to ℕ+ using hn -- error right exact ⟨n, rfl⟩ · left exact Nat.eq_zero_of_nonpos _ hn ``` The cause is that `lift` doesn't instantiate level metavariables when checking that the type of the goal is `Prop`. This PR makes the above example available. Please refer to `test/lift.lean`. commit 3dd4e55886338c90af2571a024a0418d4fe6b09a Author: Yury G. Kudryashov <[email protected]> Date: Mon May 8 03:29:53 2023 +0000 feat: port Data.Sym.Card (#3109) Co-authored-by: int-y1 <[email protected]> commit 016b02ed781f7804fe6c002d33eabc205a5e30de Author: Pol_tta <[email protected]> Date: Mon May 8 03:07:17 2023 +0000 feat: port Computability.Partrec (#3830) commit 28e49fca3bcedc90c9149a26c10c338ebc00d7a5 Author: Jason Yuen <[email protected]> Date: Mon May 8 02:51:12 2023 +0000 feat: port Topology.Category.Top.OpenNhds (#3834) commit a5a10ca18c91a12454b6317e637d69586c33448c Author: Eric Wieser <[email protected]> Date: Mon May 8 00:54:18 2023 +0000 chore: forward-port leanprover-community/mathlib#18878 (#3742) commit 4350c4e364eda158598503baf5916729406f4e95 Author: Yury G. Kudryashov <[email protected]> Date: Mon May 8 00:54:17 2023 +0000 feat: port Analysis.Normed.Group.Quotient (#3457) Co-authored-by: Mauricio Collares <[email protected]> commit cd0670b6fbe9fc3398ce064cd55f7464e15d7353 Author: Moritz Doll <[email protected]> Date: Mon May 8 00:35:14 2023 +0000 chore: add explicit name for instances in Analysis.Seminorm (#3759) Some names were extremely long. Example: [Seminorm.instConditionallyCompleteLatticeSeminormToSeminormedRingToSeminormedCommRingToNormedCommRingToAddGroupToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToSMulWithZeroToMonoidWithZeroToSemiringToDivisionSemiringToMulActionWithZeroToAddCommMonoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Seminorm.html#Seminorm.instConditionallyCompleteLatticeSeminormToSeminormedRingToSeminormedCommRingToNormedCommRingToAddGroupToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToSMulWithZeroToMonoidWithZeroToSemiringToDivisionSemiringToMulActionWithZeroToAddCommMonoid) commit 6045f2042e5e14e3b45a9ca56bf2be04921827dd Author: Moritz Firsching <[email protected]> Date: Sun May 7 14:02:40 2023 +0000 feat: port Algebra.ContinuedFractions.Computation.Translations (#3794) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> Co-authored-by: Parcly Taxel <[email protected]> commit 0285c2bf3919356b608125ae878487201d15b488 Author: Jeremy Tan Jie Rui <[email protected]> Date: Sun May 7 13:25:52 2023 +0000 chore: forward port leanprover-community/mathlib#18951 (#3837) commit 0633b89bb4e7148fcb22a6c26915d79838a11ad5 Author: Jeremy Tan Jie Rui <[email protected]> Date: Sun May 7 09:18:13 2023 +0000 chore: forward port leanprover-community/mathlib#18866 (#3813) commit b3b1b7dd2388506eceadab75d83ca8183aeeb496 Author: Scott Morrison <[email protected]> Date: Sun May 7 09:18:12 2023 +0000 feat: library_search tries most specific lemmas first, and then those with shorter names first (#3725) It turns out that `DiscrTree.getMatch` returns more specific results later than less specific ones, and so we want to put a `.reverse` in, as `library_search` is more likely to be able to make use of the more specific lemmas. Additionally, within each "batch" of lemmas in the DiscrTree, we sort them so that those with shorter names are tried before those with longer names. You shouldn't expect this to be anymore successful, I think, but maybe the user will be happier getting shorter results rather than longer ones. See some further discussion at [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20timeout/near/356406350). - [x] depends on: #3771 [](https://gitpod.io/from-referrer/) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit c993a4e8f1a1d2c587b3d939af778d3bf3dff420 Author: Jeremy Tan Jie Rui <[email protected]> Date: Sun May 7 08:52:06 2023 +0000 chore: forward port leanprover-community/mathlib#18479 (#3829) commit 038caab459760a87b476351dfd62b7ab2a50bee5 Author: Scott Morrison <[email protected]> Date: Sun May 7 08:35:59 2023 +0000 feat: speedup library_search by using two DiscrTrees (#3771) Previously, `library_search` used a single `DiscrTree`. There is a cached `DiscrTree` covering the whole library (and which is cached to disk), and then when we call `library_search`, we traverse the declarations in the current file, adding those into that `DiscrTree`. This PR speeds up that process by using a second independent `DiscrTree` for the declarations in the current file. This means that the cached tree for the library does not need to be "edited in place", and so we save some time. On the test file on my computer this speeds up from around 10.0s to around 8.2s. When calling `library_search` low down in a large file we should expect larger gains. The PR also does some refactoring work on `DeclCache`, which will be useful if/when we install global caching for other lookup tactics such as `propose` or [`rewrites`](https://github.com/leanprover-community/mathlib4/pull/3119). Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit 18c6e24d4a7c5ec87e4c7e9e295e852475c70c55 Author: Eric Wieser <[email protected]> Date: Sun May 7 07:13:52 2023 +0000 chore: forward-port leanprover-community/mathlib#18934 (#3806) Co-authored-by: Parcly Taxel <[email protected]> commit 424263023c2e9c1588f05d9a28a5abb9ae8ae88b Author: Eric Wieser <[email protected]> Date: Sun May 7 07:13:51 2023 +0000 chore: forward-port leanprover-community/mathlib#18902 (#3770) commit 8a2c2bf047940fdad965814424f3a2c1d8a6644d Author: Jeremy Tan Jie Rui <[email protected]> Date: Sun May 7 05:02:30 2023 +0000 chore: bye-bye, solo `by`s! (#3825) This PR puts, with one exception, every single remaining `by` that lies all by itself on its own line to the previous line, thus matching the current behaviour of `start-port.sh`. The exception is when the `by` begins the second or later argument to a tuple or anonymous constructor; see https://github.com/leanprover-community/mathlib4/pull/3825#discussion_r1186702599. Essentially this is `s/\n *by$/ by/g`, but with manual editing to satisfy the linter's max-100-char-line requirement. The Python style linter is also modified to catch these "isolated `by`s". commit 2d3d9fe6f82530f0355cf06d52cfa44bfbb1a033 Author: Hagb (Junyu Guo 郭俊余) <[email protected]> Date: Sat May 6 19:50:27 2023 +0000 feat(Data/MvPolynomial/Basic): add and generalize some lemmas from Finsupp and MonoidAlgebra (#3604) Most of these changes generalize from `DistribMulAction` to `SmulZeroClass`. The new lemmas are all just proved using corresponding lemmas on the underlying types. Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit 55705f9084276a7a7de523230af1827ba60fb949 Author: Ruben Van de Velde <[email protected]> Date: Sat May 6 19:21:52 2023 +0000 ci: make bors block on the check_imported job (#3827) commit f72485cdca5b6010514168873616232d7765dc90 Author: Scott Morrison <[email protected]> Date: Sat May 6 15:10:58 2023 +0000 chore: bump to Lean 4 nightly-2023-05-06 (#3817) Co-authored-by: Scott Morrison <[email protected]> commit f1ae5b7ec8d705042684482b8fb06cd34adfcb65 Author: Scott Morrison <[email protected]> Date: Sat May 6 12:10:21 2023 +0000 feat: enable cancel_denoms preprocessor in linarith (#3801) Enable the `cancelDenoms` preprocessor in `linarith`. Closes #2714. - [x] depends on: #3797 [](https://gitpod.io/from-referrer/) Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Patrick Massot <[email protected]> Co-authored-by: Floris van Doorn <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit ec38b915d3a36cb7d0adef661259453be01c4728 Author: MonadMaverick <[email protected]> Date: Sat May 6 11:29:51 2023 +0000 feat: port MeasureTheory.Measure.NullMeasurable (#3349) Co-authored-by: MonadMaverick <[email protected]> Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit d8f1f02fd6a548ea4d1f944972a929089cca5869 Author: Jeremy Tan Jie Rui <[email protected]> Date: Sat May 6 08:46:32 2023 +0000 chore: forward port leanprover-community/mathlib#18910 (#3814) commit 79ca50dced9a0a479fd0da6941f7cd67a9927d9e Author: Patrick Massot <[email protected]> Date: Sat May 6 08:46:30 2023 +0000 feat: `cancel_denoms` tactic (#3797) Ports the tactic `CancelDenoms.derive` and the interactive tactic `cancel_denoms`. This tactic is needed to make `linarith` handle divisions by numbers, but this PR does not involve `linarith`. Co-authored-by: Floris van Doorn <[email protected]> Co-authored-by: Kyle Miller <[email protected]> commit b7ed6f5bb61ecc043f01aa3b27276188ba1a2cdf Author: Yury G. Kudryashov <[email protected]> Date: Sat May 6 08:29:50 2023 +0000 chore: fix names (#3812) Forward-port leanprover-community/mathlib#18921 and leanprover-community/mathlib#18924 commit 0fbb715e696b40a5dfa8974c9f59a890a65fd2b7 Author: Xavier Roblot <[email protected]> Date: Sat May 6 07:33:35 2023 +0000 feat port : RingTheory.Ideal.AssociatedPrime (#3810) commit a31acfcf3520728bef79bcfa4e0275466a0834ab Author: EmilieUthaiwat <[email protected]> Date: Sat May 6 07:17:10 2023 +0000 feat: port LinearAlgebra.Lagrange (#3784) commit 2617ac0e6b300c20d8bb10198fafe9332d45df5a Author: MonadMaverick <[email protected]> Date: Sat May 6 06:40:03 2023 +0000 feat: port MeasureTheory.Measure.AEDisjoint (#3351) Co-authored-by: Jeremy Tan Jie Rui <[email protected]> Co-authored-by: Komyyy <[email protected]> commit 214014d2c39d5fe770fbb305588808bcb1a4aff4 Author: Scott Morrison <[email protected]> Date: Fri May 5 22:16:38 2023 +0000 chore: forward-port backports (#3752) * `data.mv_polynomial.basic`, `data.mv_polynomial.funext`: leanprover-community/mathlib#18839 * `category_theory.limits.preserves.finite`, `category_theory.preadditive.projective`: leanprover-community/mathlib#18890 * `category_theory.abelian.basic`, `category_theory.abelian.opposite`: leanprover-community/mathlib#18740 * `topology.category.Top.limits.basic`: leanprover-community/mathlib#18871. Note that this does not show a useful diff on the dashboard pages as file splits aren't tracked well by git. Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> commit 35f51927282d120df99e96c037ddfb4132e947bf Author: Eric Wieser <[email protected]> Date: Fri May 5 14:00:33 2023 +0000 chore: forward-port leanprover-community/mathlib#18906 (#3798) commit ddf1a04c942b901a07d053d2f967f2ad40777e1a Author: Jason Yuen <[email protected]> Date: Fri May 5 13:44:48 2023 +0000 feat: port MeasureTheory.Function.AEMeasurableSequence (#3803) commit e0fd3f7dbf994599af312d5f630bf7fcedbb9bce Author: Ruben Van de Velde <[email protected]> Date: Fri May 5 12:24:18 2023 +0000 chore: tidy various files (#3718) commit f4dd3adaf6847e2e940853c1d3d2b36aaa781425 Author: Eric Wieser <[email protected]> Date: Fri May 5 06:25:34 2023 +0000 chore: update SHA from #3753 (#3799) I forgot to update it in #3753. commit 963ac8132f80aa069680b719e64cb4b0cba54366 Author: Jeremy Tan Jie Rui <[email protected]> Date: Thu May 4 19:07:27 2023 +0000 feat: port Algebra.ContinuedFractions.ConvergentsEquiv (#3795) commit 3a802fc9446bc158d1486997f5f5794e4c402beb Author: Yaël Dillies <[email protected]> Date: Thu May 4 16:30:32 2023 +0000 feat: well-founded or transitive relations don't have cycles (#3793) Match https://github.com/leanprover-community/mathlib/pull/18512 Co-authored-by: Eric Wieser <[email protected]> commit d9ea05decd47313168b7f7febd64643ff7ed1932 Author: Eric Wieser <[email protected]> Date: Thu May 4 11:23:11 2023 +0000 chore: forward-port leanprover-community/mathlib#18922 (#3779) commit 4b452a9fec289cc8ed1e18098680ab0db19079d4 Author: Eric Wieser <[email protected]> Date: Thu May 4 11:23:10 2023 +0000 chore: forward-port leanprover-community/mathlib#18876 (#3753) commit 45acfec0369c6720452249bdf860cbeafa89c25b Author: Eric Wieser <[email protected]> Date: Thu May 4 11:23:09 2023 +0000 chore: forward-port leanprover-community/mathlib#18879 (#3741) commit 700eb94e185cb781b1f8945cb350ff3051f4a52a Author: Moritz Firsching <[email protected]> Date: Thu May 4 09:12:04 2023 +0000 feat: port Algebra.ContinuedFractions.TerminatedStable (#3792) Co-authored-by: Moritz Firsching <[email protected]> commit d7a6de21586b9f2fd41676da624f6fc4ccd3eb18 Author: Jason Yuen <[email protected]> Date: Thu May 4 09:12:03 2023 +0000 feat: port Algebra.ContinuedFractions.Computation.Basic (#3788) Co-authored-by: Moritz Firsching <[email protected]> commit c643d1282c5c47f210c9497d1e19867dbd1bcb74 Author: MonadMaverick <[email protected]> Date: Thu May 4 08:44:21 2023 +0000 feat: port MeasureTheory.Measure.MeasureSpaceDef (#3325) Co-authored-by: Jeremy Tan Jie Rui <[email protected]> Co-authored-by: Komyyy <[email protected]> commit 6ee07bd7ff39032233031f056c2649ccda4cafef Author: Moritz Firsching <[email protected]> Date: Thu May 4 08:21:57 2023 +0000 feat: port Algebra.ContinuedFractions.ContinuantsRecurrence (#3791) Co-authored-by: Moritz Firsching <[email protected]> commit ac2e5438c8c07b7c63166df1bdf15076028c4159 Author: Moritz Firsching <[email protected]> Date: Thu May 4 05:47:35 2023 +0000 feat: port Algebra.ContinuedFractions.Translations (#3783) Co-authored-by: Moritz Firsching <[email protected]> commit e34f9b0fc494772fc304aeffa32e829278a17962 Author: Kyle Miller <[email protected]> Date: Wed May 3 23:01:50 2023 +0000 feat: delaborators for Finset.prod and Finset.sum (#3772) Also fixes some spacing in their `syntax` commands, which impacts pretty printing. commit d490330ae628c357fe9c758990605ded66628194 Author: Kevin Buzzard <[email protected]> Date: Wed May 3 22:31:52 2023 +0000 chore: update Mathlib/Tactic.lean (#3727) Co-authored-by: Scott Morrison <[email protected]> commit 2f62a68be3bd7b099d591820492b5eb668f3843e Author: Alex J Best <[email protected]> Date: Wed May 3 17:20:53 2023 +0000 feat: implement intermediate state for simp_rw (#3738) closes #3680, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Stepping.20through.20simp_rw/near/326712986 commit ee67ae82322f25cafc7534b5dbd33ad93d8faa8b Author: thorimur <[email protected]> Date: Wed May 3 14:00:58 2023 +0000 refactor, fix: `MetaM` version of `rfl` tactic and missing `whnfR`/`instantiateMVars` (#3758) This PR factors out a `MetaM` version of the `rfl` tactic and adds a missing `whnfR` and `instantiateMVars` in front of the goal type. This means that a few `rw`s across mathlib4 now close the goal instead of e.g. requiring a trailing `exact le_rfl`. Note: we do not use `whnfR` on the return type when adding the `refl` extension in the first place, as `forallMetaTelescopeReducing` already performs `whnf` (here, at reducible transparency). See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233758.20.E2.80.93.20rfl.20refactor.20.26.20fix) for some discussion on the internal changes made. Co-authored-by: Floris van Doorn <[email protected]> commit 8cad0a826486d2a0005de7e353e12f2ae143b78e Author: Jason Yuen <[email protected]> Date: Wed May 3 13:39:19 2023 +0000 feat: port LinearAlgebra.AffineSpace.FiniteDimensional (#3670) commit 052deed907b6ffc756bd7ce4ecdedf4d6db1068d Author: JeEyben <[email protected]> Date: Wed May 3 13:39:17 2023 +0000 feat: port RingTheory.Localization.InvSubmonoid (#3384) Co-authored-by: int-y1 <[email protected]> commit 5a77592a11f98444a19c2ea97fad0291fe408b96 Author: Jason Yuen <[email protected]> Date: Wed May 3 13:39:15 2023 +0000 feat: port Algebra.ContinuedFractions.Basic (#3379) Co-authored-by: Jon Eugster <[email protected]> commit 8f6e4d2054a99fd8c847cacfe57b408b8b18646a Author: Moritz Firsching <[email protected]> Date: Wed May 3 13:39:13 2023 +0000 feat: port CategoryTheory.Monoidal.Free.Basic (#2808) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Joël Riou <[email protected]> Co-authored-by: Johan Commelin <[email protected]> commit 30a890eb4e9dbda9dd9dc42c4e2f260b59abb214 Author: Scott Morrison <[email protected]> Date: Wed May 3 13:16:44 2023 +0000 fix: a missing TypeMax (#3781) One was missed; curiously it wasn't harmful in `master`, but when we turn on `etaExperiment` globally this causes a breakage Co-authored-by: Scott Morrison <[email protected]> commit 814f492f80e97836913d1b788911a1ddc76b6f42 Author: Ruben Van de Velde <[email protected]> Date: Wed May 3 12:09:25 2023 +0000 chore: move shortcut instance to Algebra.Algebra.Basic (#3778) See https://github.com/leanprover-community/mathlib/pull/18907 Co-authored-by: Eric Wieser <[email protected]> commit 0ab5e61ca44a52206df99830a0facaf91d8b803e Author: Moritz Doll <[email protected]> Date: Wed May 3 11:33:41 2023 +0000 docs: fix names in Analysis.LocallyConvex.Bounded (#3774) commit ac0fd896f1bb1f197f25f5f654a859b4a02d8516 Author: MonadMaverick <[email protected]> Date: Wed May 3 11:02:26 2023 +0000 feat: port MeasureTheory.Measure.OuterMeasure (#3674) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Komyyy <[email protected]> Co-authored-by: Johan Commelin <[email protected]> commit ae90d57d66ab4137eb22d9152cdd2d6aa0f19cd6 Author: Jason Yuen <[email protected]> Date: Wed May 3 06:27:24 2023 +0000 feat: port LinearAlgebra.AffineSpace.Matrix (#3775) commit 3ad45ada879ff7d1eb0c425df6bf8d4bec66adba Author: Xavier-François Roblot <[email protected]> Date: Wed May 3 01:24:20 2023 +0000 feat port: Algebra.FreeModule.Determinant (#3767) commit c577bee1ea0537d6a4488ad569f3252ed2123784 Author: Ruben Van de Velde <[email protected]> Date: Wed May 3 01:24:19 2023 +0000 feat: port Data.Complex.Determinant (#3765) commit c89277f05e074a327f79381c14d659b05e68168b Author: Ruben Van de Velde <[email protected]> Date: Wed May 3 01:24:17 2023 +0000 feat: port Analysis.SpecialFunctions.Trigonometric.Chebyshev (#3764) commit 1dac593b7e1c149c4d234973754b4347de968595 Author: Ruben Van de Velde <[email protected]> Date: Wed May 3 01:24:16 2023 +0000 feat: port Analysis.Convex.Complex (#3763) commit efb20cbedfb68cb1b2967449ef92b374c0f9724b Author: Ruben Van de Velde <[email protected]> Date: Wed May 3 01:24:16 2023 +0000 feat: port Data.Matrix.Rank (#3762) commit a65601d186c742e05cece1797b1046322f8f16f4 Author: Joël Riou <[email protected]> Date: Wed May 3 01:24:14 2023 +0000 feat: port CategoryTheory.Category.Groupoid (#3761) commit 4ddf8c7c266db2c9486475955bfb75a6ccafc360 Author: Yaël Dillies <[email protected]> Date: Wed May 3 01:24:13 2023 +0000 chore: tweak `subsingleton_of_trichotomous_of_irrefl` (#3749) Match https://github.com/leanprover-community/mathlib/pull/18749 commit 94cd04e32c71f1a64c15e6aee06eabaa6c059fb4 Author: Scott Morrison <[email protected]> Date: Tue May 2 22:58:39 2023 +0000 feat: better display of partial results from library_search (#3743) On @PatrickMassot's [example](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20regression/near/353375130): ```lean import Mathlib.Topology.Instances.Real import Mathlib.Topology.Algebra.Order.Compact import Mathlib.Tactic.LibrarySearch example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by library_search ``` we have: * `refine IsCompact.exists_forall_le hK ?_ ?_` as one of the suggested solutions * in fact, as the first solution (on the basis that it uses more local hypotheses than alternatives) * none of the spurious results which use `False.elim ?_` * and better display of the result, with hints: ```lean refine IsCompact.exists_forall_le hK ?_ ?_ -- Remaining subgoals: -- ⊢ Set.Nonempty K -- ⊢ ContinuousOn (fun x ↦ f x) K ``` Co-authored-by: Scott Morrison <[email protected]> commit 391cddce21029cb45a255a2ab063c7d3b98b4b60 Author: Jeremy Tan Jie Rui <[email protected]> Date: Tue May 2 16:51:37 2023 +0000 feat: port Topology.Algebra.Module.Determinant (#3766) commit fed5a971cac804f30a3b4b2550bc532e0b1adbaf Author: Scott Morrison <[email protected]> Date: Tue May 2 14:49:42 2023 +0000 fix: don't look too hard for binders when indexing lemmas for library_search (#3724) Co-authored-by: Scott Morrison <[email protected]> commit 3f6f6282cc137af13d6c480744e58dedca712c1e Author: Scott Morrison <[email protected]> Date: Tue May 2 12:23:16 2023 +0000 fix: linarith variable shadowing bug (#3760) As reported on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20bug). Co-authored-by: Scott Morrison <[email protected]> commit 92a23d50515de9ac1baf29a66826ee77305b2b91 Author: Joël Riou <[email protected]> Date: Tue May 2 10:23:03 2023 +0000 feat: port CategoryTheory.Monoidal.Tor (#3754) Co-authored-by: Joël Riou <[email protected]> commit 179b81ee4cadef2f601e1f1265d266ea0cf91cd7 Author: Eric Wieser <[email protected]> Date: Tue May 2 10:23:02 2023 +0000 Revert "feat: port Algebra.Order.ToIntervalMod (#2148)" (#3388) This reverts commit 2d0dd3902a4a796d8f38778fec991ab1d4c2a660. The porting comments say "Would be nice to finish leanprover-community/mathlib#17743 first". The commit message says "Might be best to wait". We should wait; there is no urgency to merge this, and no discussion took place that argued against waiting. commit 3f6b46f277537242649fa82a62efddb09fc8dfea Author: Pol_tta <[email protected]> Date: Tue May 2 10:05:14 2023 +0000 feat: port LinearAlgebra.Determinant (#3694) Co-authored-by: int-y1 <[email protected]> Co-authored-by: Komyyy <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Ruben Van de Velde <[email protected]> Co-authored-by: Eric Wieser <[email protected]> commit 8d401bd92990dec5d9d1aa59094789f607caf2d0 Author: Ruben Van de Velde <[email protected]> Date: Tue May 2 07:59:21 2023 +0000 feat: port Data.Complex.Module (#3737) Co-authored-by: int-y1 <[email protected]> Co-authored-by: Eric Wieser <[email protected]> commit 0227fbbc71c1ce40bb9338c52058d0a34565653c Author: Alex J Best <[email protected]> Date: Mon May 1 22:19:23 2023 +0000 chore: update workflows to avoid deprecation (#3755) Forward port of https://github.com/leanprover-community/mathlib/pull/18761 - https://github.com/leanprover-community/mathlib/pull/18765 but a bit simpler as we dont have as many things set up yet. commit 6d40a326339dc6b42c3ed25a607bb5bfe035bc7f Author: Joël Riou <[email protected]> Date: Mon May 1 22:19:22 2023 +0000 feat: port CategoryTheory.Functor.LeftDerived (#3751) Co-authored-by: Joël Riou <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit e57a8f962faca1a6949a74daec03e5b350995af8 Author: Joël Riou <[email protected]> Date: Mon May 1 22:19:21 2023 +0000 feat: port CategoryTheory.Sites.LeftExact (#3706) commit fc3894f2f75c7b860783e8a90fd767bcb00b2cb9 Author: Pol_tta <[email protected]> Date: Mon May 1 22:19:20 2023 +0000 feat: make `Acc.rec` and many related defs computable (#3535) Lean 4 code generator has had no native supports for `Acc.rec`. This PR makes `Acc.rec` computable. This change makes many defs computable. Especially, computable `PFun.fix` and `Part.hasFix` enables us to reason about `partial` functions. This PR also renames some instances and gives `PFun.lift` `@[coe]` attr. commit eb1f66662c488bafde47edd140eef4a47bc59d2a Author: Bulhwi Cha <[email protected]> Date: Mon May 1 22:02:09 2023 +0000 refactor: delete `import` line (#3745) Delete an unnecessary `import` line. commit 28ae9843458339c54de11f62fce84002528759af Author: Joël Riou <[email protected]> Date: Mon May 1 20:06:10 2023 +0000 feat: port CategoryTheory.Preadditive.ProjectiveResolution (#3740) Co-authored-by: Joël Riou <[email protected]> commit 52e6ad71693190465481e0ae20d97913dbba06e9 Author: Yaël Dillies <[email protected]> Date: Mon May 1 17:47:55 2023 +0000 chore: Move lattice `finset` lemmas around (#3748) Match https://github.com/leanprover-community/mathlib/pull/18900 Co-authored-by: Eric Wieser <[email protected]> commit 5b940a6dc1a1bd5f2f4a6f271059bbea0e3857bc Author: Yury G. Kudryashov <[email protected]> Date: Mon May 1 17:47:54 2023 +0000 feat: port CategoryTheory.Abelian.Exact (#3638) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: Joël Riou <[email protected]> commit 0ea443f63e211696d5a166c82f7469cc2cdc1d82 Author: Yaël Dillies <[email protected]> Date: Mon May 1 15:10:19 2023 +0000 feat: `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#3747) Match https://github.com/leanprover-community/mathlib/pull/18892 * [`order.lattice`@`d6aad9528ddcac270ed35c6f7b5f1d8af25341d6`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/order/lattice?range=d6aad9528ddcac270ed35c6f7b5f1d8af25341d6..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) * [`algebra.group.pi`@`90df25ded755a2cf9651ea850d1abe429b1e4eb1`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=90df25ded755a2cf9651ea850d1abe429b1e4eb1..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) * [`data.set.intervals.pi`@`4020ddee5b4580a409bfda7d2f42726ce86ae674`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/intervals/pi?range=4020ddee5b4580a409bfda7d2f42726ce86ae674..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) Co-authored-by: Eric Wieser <[email protected]> commit e95cccde5645c855b0c08a5fb4d944adf442a4b7 Author: Jeremy Tan Jie Rui <[email protected]> Date: Mon May 1 13:19:51 2023 +0000 feat: port Topology.Category.Profinite.Projective (#3746) commit 55637dc9d43c30243cb0d8578cabcabf4dedbc8c Author: Moritz Firsching <[email protected]> Date: Mon May 1 11:02:54 2023 +0000 feat: port Mathlib.Data.Ordmap.Ordnode (#1455) Co-authored-by: Arien Malec <[email protected]> Co-authored-by: Floris van Doorn <[email protected]> Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: qawbecrdtey <[email protected]> commit 64d186af31d440f3743d6862c0f39cf553fcdca1 Author: Violeta Hernández <[email protected]> Date: Mon May 1 08:43:35 2023 +0000 feat: port ZFC set intersection (#3345) Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: https://github.com/leanprover-community/mathlib/pull/18232 Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Yaël Dillies <[email protected]> commit 5925a364a984ab06f0d1b425339c4bb5cd1b2646 Author: Scott Morrison <[email protected]> Date: Mon May 1 01:58:20 2023 +0000 feat: port Topology.Category.Profinite.Basic (#3705) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: adamtopaz <[email protected]> commit c272f4940037d117009ce720b7aba0bad3986627 Author: Alex J Best <[email protected]> Date: Mon May 1 01:36:18 2023 +0000 feat: annotate build errors in the github files changed tab using an action (#3739) This is suboptimal as it doesn't handle multiline comments, but it is better than nothing, and the implementation works out of the box. This is broadly similar to the support we had in mathlib 3, but the implementation is different as we no longer have json errors as an option, so must instead match an errorformat directly (the gcc one works fine). Supporting multiline error messages appears not to be possible using the builtin output without further processing with the current state of problem matchers supported by github (which follow the vscode design). Thus to get an improvement on this the build output must be piped through a second program that processes it in some way, or a lake build type command should be added that outputs in a required format. Likewise to get annotations for linter failures we will need to add extra information to the linter output, either setting the annotations ourselves (as we did in mathlib 3) or at least adding line numbers to the existing output so that we can at least match it with a problem matcher again. commit 77416707240d45fb64906bc8f7f28d6f29cfda2b Author: Bulhwi Cha <[email protected]> Date: Sun Apr 30 23:31:19 2023 +0000 chore: move theorems on `String` to std4 (#3712) https://github.com/leanprover/std4/pull/124 moves the following from Mathlib4 to Std4: * helper `simp` theorems on `String.Pos` * `String.utf8GetAux.inductionOn` commit 6a64ec0b0f5ee12b611215ac7ad1e0145465a327 Author: Ruben Van de Velde <[email protected]> Date: Sun Apr 30 11:38:03 2023 +0000 feat: port FieldTheory.Tower (#3716) Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Ruben Van de Velde <[email protected]> commit 76707255936de099ae6835e7ddbe5f7bf95a7a36 Author: Joël Riou <[email protected]> Date: Sat Apr 29 23:07:53 2023 +0000 feat: port Algebra.Category.Group.ZModuleEquivalence (#3732) commit 543b8ec1ea21d7a3321234bb0b6532576a897c61 Author: Joël Riou <[email protected]> Date: Sat Apr 29 23:07:52 2023 +0000 feat: port AlgebraicTopology.ExtraDegeneracy (#3729) commit eb11681ef13f0d1aba2ff267a20bd08883484f82 Author: Jeremy Tan Jie Rui <[email protected]> Date: Sat Apr 29 22:52:42 2023 +0000 feat: port CategoryTheory.Monad.Coequalizer (#3733) commit 6a28eee3a21942016a01bbada70ce9a6a40ba8e5 Author: Moritz Firsching <[email protected]> Date: Sat Apr 29 22:28:56 2023 +0000 chore: no newline before aligns (#3735) Co-authored-by: Moritz Firsching <[email protected]> commit a7e9e4ab120a3b6d10251d3c3d24a1e60c13dca8 Author: Yaël Dillies <[email protected]> Date: Sat Apr 29 16:26:38 2023 +0000 feat: `a * b ≠ b ↔ a ≠ 1` (#3726) https://github.com/leanprover-community/mathlib/pull/18635 * [`algebra.group.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..84771a9f5f0bd5e5d6218811556508ddf476dcbd) * [`algebra.order.field.basic`@`44e29dbcff83ba7114a464d592b8c3743987c1e5`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/field/basic?range=44e29dbcff83ba7114a464d592b8c3743987c1e5..84771a9f5f0bd5e5d6218811556508ddf476dcbd) Co-authored-by: Eric Wieser <[email protected]> commit dc012f816b787bcb80007f2bc1b5e6604aa57b28 Author: Jeremy Tan Jie Rui <[email protected]> Date: Sat Apr 29 13:32:59 2023 +0000 feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728) Co-authored-by: ChrisHughes24 <[email protected]> commit 8dd639e1083340aed6138d8ad7f954091b037267 Author: Scott Morrison <[email protected]> Date: Sat Apr 29 13:32:58 2023 +0000 fix: find MathlibExtras from downstream projects (#3721) Co-authored-by: Scott Morrison <[email protected]> commit 73bab6a59163675f3f1f26530bac9c2571eba84b Author: Scott Morrison <[email protected]> Date: Sat Apr 29 13:32:57 2023 +0000 fix: allow library_search to run when maxHeartbeats = 0 (#3720) Co-authored-by: Scott Morrison <[email protected]> commit 301ea2db46c56d28eb73f418ab992b0010e5f75d Author: Yaël Dillies <[email protected]> Date: Sat Apr 29 13:32:56 2023 +0000 chore: Remove `finset.sup_finset_image` (#3713) Match https://github.com/leanprover-community/mathlib/pull/18893 Co-authored-by: Jeremy Tan Jie Rui <[email protected]> commit f667fdec730173011b40f4dcea8c79c33eed39b6 Author: Joël Riou <[email protected]> Date: Sat Apr 29 13:32:55 2023 +0000 feat: port CategoryTheory.Abelian.Transfer (#3424) commit 029b212612c336f75d26163cebd5e129a455847e Author: Alex J Best <[email protected]> Date: Sat Apr 29 10:38:07 2023 +0000 feat: allow several tactics on types that are slightly less obviously Types (#3682) Many tactics attempt to get the universe of the sort of the terms involved by matching on the level being a succ of something. Unfortunately this fails on some nontrivial examples like mvpolynomial which can have type `Sort (max (u+1) (v+1))` Instead we decrement the level manually after matching it. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60ring.60.20tactic.20cannot.20prove.20equality.20about.20.60MvPolynomial.60/near/352549549 This PR modifies ring, ring_nf, nontriviality, polyrith, linarith, and some norm_num handlers to appropriately handle this. Test cases showing examples that failed before (inspired by the case of mvpolynomial, but in principle there could be other interesting types that have multiple universe parameters in this way, some of which may even have a linear order who knows). In doing so we factor out `inferTypeQ'` into its own file `Mathlib.Tactic.Qq` for mathlib-relevant extensions of Qq commit a540fe1433f247fd5cd6561401ab813cf04a5e9e Author: Yury G. Kudryashov <[email protected]> Date: Sat Apr 29 09:57:49 2023 +0000 feat: port LinearAlgebra.ProjectiveSpace.Basic (#3692) commit d2c96a57df11efb8eec9f31377e5de800012433c Author: Jason Yuen <[email protected]> Date: Sat Apr 29 05:39:03 2023 +0000 chore: add hash for Data.MvPolynomial.Polynomial (#3723) commit 288a7d79cf1b6dfd4940082700efa5b8dc15d496 Author: Jason Yuen <[email protected]> Date: Sat Apr 29 03:33:44 2023 +0000 feat: port LinearAlgebra.SymplecticGroup (#3696) commit 3230cdeee0ab5da8fc47680e4d5da87addcc90e7 Author: Alex J Best <[email protected]> Date: Fri Apr 28 23:45:34 2023 +0000 feat: make alias compile code when possible (#3719) commit 36844e9cb778e4e857c8c9b0b0339c876679f4a8 Author: Eric Wieser <[email protected]> Date: Fri Apr 28 23:45:32 2023 +0000 chore: forward-port leanprover-community/mathlib#18880 (#3717) commit 24f74e319f706f55aef284703cddec753ffadb62 Author: Yaël Dillies <[email protected]> Date: Fri Apr 28 23:19:17 2023 +0000 chore: Rename to `AddLocalization` (#3714) This name wasn't properly capitalised. commit aaf828ddcf36204db88d6e02fa5a90da2126a1bb Author: Eric Wieser <[email protected]> Date: Fri Apr 28 21:59:08 2023 +0000 chore: update SHA (#3711) I forgot to update the SHA in #3675 commit b50e5c5aa89de2b79df485083b3f5c1bb00b4b8d Author: Yury G. Kudryashov <[email protected]> Date: Fri Apr 28 21:59:07 2023 +0000 feat: port LinearAlgebra.Matrix.Diagonal (#3695) Some proofs in the last section were failing even with eta-experiment, so I generalized some lemmas from `Field`s to `Semifield`s. commit f5f2fbf04d6c9b0a995807c408ade9e71bad05f1 Author: Adam Topaz <[email protected]> Date: Fri Apr 28 18:56:37 2023 +0000 feat: Port Topology.Category.CompHaus.Projective (#3715) commit 863aebc8ccf10ff0c19a25fad7344e8a585c9108 Author: Xavier-François Roblot <[email protected]> Date: Fri Apr 28 17:46:02 2023 +0000 feat LinearAlgebra.Basis: add basis.restrictScalars (#3707) Mathlib4 version of https://github.com/leanprover-community/mathlib/pull/18814 [`linear_algebra.basis`@`2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e`..`04cdee31e196e30f507e8e9eb2d06e02c9ff6310`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/basis?range=2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e..04cdee31e196e30f507e8e9eb2d06e02c9ff6310)) commit a585b6ffc2dc1351ab8a5aa1534c26f22c2d7910 Author: Yaël Dillies <[email protected]> Date: Fri Apr 28 14:30:45 2023 +0000 feat: Lemmas relating definitions of infinite sets (#3672) Match https://github.com/leanprover-community/mathlib/pull/18620 * [`data.set.finite`@`c941bb9426d62e266612b6d99e6c9fc93e7a1d07`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/finite?range=c941bb9426d62e266612b6d99e6c9fc93e7a1d07..52fa514ec337dd970d71d8de8d0fd68b455a1e54) * [`data.finset.locally_finite`@`f24cc2891c0e328f0ee8c57387103aa462c44b5e`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/locally_finite?range=f24cc2891c0e328f0ee8c57387103aa462c44b5e..52fa514ec337dd970d71d8de8d0fd68b455a1e54) * [`data.nat.lattice`@`2445c98ae4b87eabebdde552593519b9b6dc350c`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/lattice?range=2445c98ae4b87eabebdde552593519b9b6dc350c..52fa514ec337dd970d71d8de8d0fd68b455a1e54) commit 601c82017f39b855b6a697a78d4a244b668996e7 Author: Moritz Firsching <[email protected]> Date: Fri Apr 28 14:00:44 2023 +0000 feat: port LinearAlgebra.Matrix.Transvection (#3700) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: ChrisHughes24 <[email protected]> commit 3d576486048be2cbae503d1c1e7f5a0a85b66a6c Author: Yaël Dillies <[email protected]> Date: Fri Apr 28 11:44:00 2023 +0000 feat: For any `b`, there exists a set `s` of independent atoms such that `Sup s` is the complement of `b` (#3588) Match https://github.com/leanprover-community/mathlib/pull/8475 * [`order.compactly_generated`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/compactly_generated?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..e8cf0cfec5fcab9baf46dc17d30c5e22048468be) * [`order.directed`@`485b24ed47b1b7978d38a1e445158c6224c3f42c`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/directed?range=485b24ed47b1b7978d38a1e445158c6224c3f42c..e8cf0cfec5fcab9baf46dc17d30c5e22048468be) commit d3e6edfe83effc9316d710b3e4421b16162e73d1 Author: Joël Riou <[email protected]> Date: Fri Apr 28 11:10:45 2023 +0000 feat: port CategoryTheory.Action (#3657) commit bc85faaf38cdda2b9c3f808ba563c232f5f815a0 Author: Yury G. Kudryashov <[email protected]> Date: Fri Apr 28 11:10:44 2023 +0000 feat: port CategoryTheory.Preadditive.Projective (#3615) Co-authored-by: Joël Riou <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit b98b04707b0c77941e61f598a4b8c8164a2c2482 Author: Moritz Firsching <[email protected]> Date: Fri Apr 28 10:54:06 2023 +0000 feat: port LinearAlgebra.Matrix.ZPow (#3671) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: Parcly Taxel <[email protected]> commit cd980733e0e92568cb77dbb4a9c0f6b3498dc9ce Author: Jeremy Tan Jie Rui <[email protected]> Date: Fri Apr 28 09:49:14 2023 +0000 feat: port LinearAlgebra.Matrix.FiniteDimensional (#3698) commit 740bbec09993a7a71a993aaf7fdee3571005215c Author: Bulhwi Cha <[email protected]> Date: Fri Apr 28 09:32:10 2023 +0000 refactor: change arguments order (#3701) Change the order of the arguments to `String.utf8GetAux.add_right_cancel`. commit 4d1c8e0454e1470c3cbc8e3aa41d5745acd1cdc1 Author: Jeremy Tan Jie Rui <[email protected]> Date: Fri Apr 28 06:56:28 2023 +0000 feat: port LinearAlgebra.Matrix.InvariantBasisNumber (#3697) commit 15d98e6b55a610e11d16e02aca4fc7be760c5ffd Author: Jeremy Tan Jie Rui <[email protected]> Date: Fri Apr 28 06:56:27 2023 +0000 feat: port AlgebraicTopology.Nerve (#3693) commit e35da366b8e442a61e77516edd8197e8715264b5 Author: Eric Wieser <[email protected]> Date: Fri Apr 28 06:56:26 2023 +0000 forward-port leanprover-community/mathlib#18840 (#3678) commit d456dd3ce4146aa82e05ac02aae437901b534fc1 Author: Eric Wieser <[email protected]> Date: Fri Apr 28 06:56:25 2023 +0000 chore: forward-port leanprover-community/mathlib#18802 (#3677) commit e234e1dbab60d5cb2491ee19f608fe6357d7244c Author: Eric Wieser <[email protected]> Date: Fri Apr 28 06:56:24 2023 +0000 chore: forward-port leanprover-community/mathlib#18869 (#3676) commit bd1736fa511c00b8607b3e1134213cd963b923c1 Author: Eric Wieser <[email protected]> Date: Fri Apr 28 06:56:23 2023 +0000 chore: forward-port leanprover-community/mathlib#18842 (#3675) commit 7d4f125478272f478180c413365372d3069e8a63 Author: Yaël Dillies <[email protected]> Date: Fri Apr 28 06:56:22 2023 +0000 feat: The equivalence between `fin n → fin m` and `fin (m ^ n)` (#3673) Match https://github.com/leanprover-community/mathlib/pull/14817 [`algebra.big_operators.fin`@`f93c11933efbc3c2f0299e47b8ff83e9b539cbf6`..`cdb01be3c499930fd29be05dce960f4d8d201c54`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/big_operators/fin?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..cdb01be3c499930fd29be05dce960f4d8d201c54) Co-authored-by: Eric Wieser <[email protected]> commit 535bb666094594a96afc3f425fe1c5cd49261836 Author: Eric Wieser <[email protected]> Date: Fri Apr 28 06:56:21 2023 +0000 chore: forward-port leanprover-community/mathlib#18833 (#3660) The previously hacky proofs with porting notes can be discarded in favor of the ones from mathport. commit 7f09ac6a714e33333682d4f6ff7c95bac10684d2 Author: Floris van Doorn <[email protected]> Date: Fri Apr 28 06:56:19 2023 +0000 perf: improve performance of `to_additive` (#3632) * `applyReplacementFun` now treats applications `f x_1 ... x_n` as atomic, and recurses directly into `f` and `x_i` (before it recursed on the partial appliations `f x_1 ... x_j`) * I had to reimplement the way `to_additive` reorders arguments, so at the same time I also made it more flexible. We can now reorder with an arbitrary permutation, and you have to specify this by providing a permutation using cycle notation (e.g. `(reorder := 1 2 3, 8 9)` means we're permuting the first three arguments and swapping arguments 8 and 9). This implements the first item of #1074. * `additiveTest` now memorizes the test on previously-visited subexpressions. Thanks to @kmill for this suggestion! The performance on (one of) the slowest declaration(s) to additivize (`MonoidLocalization.lift`) is summarized below (note: `dsimp only` refers to adding a single `dsimp only` tactic in the declaration, which was done in #3580) ``` original: 27400ms better applyReplacementFun: 1550ms better applyReplacementFun + better additiveTest: 176ms dsimp only: 6710ms better applyReplacementFun + dsimp only: 425ms better applyReplacementFun + better additiveTest + dsimp only: 128ms ``` commit ccfc417d5df188a52936f4722ab1162a22b9e162 Author: Pol_tta <[email protected]> Date: Fri Apr 28 05:58:44 2023 +0000 feat: port LinearAlgebra.Matrix.Basis (#3691) Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Komyyy <[email protected]> Co-authored-by: Johan Commelin <[email protected]> commit 6fc9d5e9d711f3812bbd7cd0fbeb2fed11cf9c6e Author: Jeremy Tan Jie Rui <[email protected]> Date: Fri Apr 28 05:41:51 2023 +0000 feat: port LinearAlgebra.FreeModule.Finite.Matrix (#3690) Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Johan Commelin <[email protected]> commit 7b0b99d0366fcca78f849aaef42e8dcd0975ed66 Author: Ruben Van de Velde <[email protected]> Date: Fri Apr 28 03:54:51 2023 +0000 feat: port LinearAlgebra.Matrix.ToLin (#3552) Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit 4f6380966f207897ef1487010c80d15f24769971 Author: Joël Riou <[email protected]> Date: Fri Apr 28 02:53:49 2023 +0000 feat: port AlgebraicTopology.SimplicialSet (#3689) commit 7b88b65bd51282f240fc40b1bd6c1e7d8c227be6 Author: Ruben Van de Velde <[email protected]> Date: Fri Apr 28 02:53:48 2023 +0000 ci: lint references.bib (#3683) Ported from mathlib3. commit b8ad9541c1a9fb132cad12283b3accc56c5ed35e Author: Moritz Firsching <[email protected]> Date: Fri Apr 28 02:53:47 2023 +0000 chore: rename Zpowers -> ZPowers (#3681) Co-authored-by: Moritz Firsching <[email protected]> commit eb417549e64541742039abd0dc9b823388124907 Author: Jeremy Tan Jie Rui <[email protected]> Date: Fri Apr 28 02:33:14 2023 +0000 feat: port Topology.Algebra.Module.Multilinear (#3348) Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: ADedecker <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit fe28ed480a44857c878f429eabc66b9fee4f3a45 Author: Jeremy Tan Jie Rui <[email protected]> Date: Fri Apr 28 01:23:38 2023 +0000 feat: port Topology.Algebra.Module.StrongTopology (#3684) Co-authored-by: ADedecker <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit 1113f1cefa6387fb404087427f48596810d95acb Author: Henrik Böving <[email protected]> Date: Fri Apr 28 00:11:16 2023 +0000 fix: mathlib4_docs cleanup routine (#3631) commit ed822e7be3f58018b6fd816b957fd888db4b35c2 Author: Kevin Buzzard <[email protected]> Date: Thu Apr 27 23:33:25 2023 +0000 feat : port CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (#3605) This was harder than it looked (the proofs are long and broke). Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Scott Morrison <[email protected]> commit 78d77dfbcae2747913005e50dad80692cb1ff940 Author: Adam Topaz <[email protected]> Date: Thu Apr 27 23:18:23 2023 +0000 feat: Port Topology.Category.CompHaus.Basic (#3688) Relatively straightforward port. Co-authored-by: Scott Morrison <[email protected]> commit d1a1c6b104967ffed8ca69ebb4f3ea9a4eb25424 Author: Joël Riou <[email protected]> Date: Thu Apr 27 21:43:33 2023 +0000 feat: port Analysis.Convex.StoneSeparation (#3686) commit 2f36c58966790d0a91aaa910836751e289259f12 Author: Joël Riou <[email protected]> Date: Thu Apr 27 21:43:32 2023 +0000 feat: port CategoryTheory.Noetherian (#3685) commit aaa5e0a421c8b53d60e6b7d1341ade2d5b2e59b3 Author: Felix-Weilacher <[email protected]> Date: Thu Apr 27 21:26:10 2023 +0000 chore: forward port leanprover-community/mathlib#18864 (#3687) Forward port changes from leanprover-community/mathlib#18864 to Topology/Perfect.lean and MeasureTheory/MeasurableSpace.lean Co-authored-by: Eric Wieser <[email protected]> commit 2dab08df0323c6e58ace9b611c7e951602d0a2c0 Author: Joël Riou <[email protected]> Date: Thu Apr 27 15:27:17 2023 +0000 feat: port CategoryTheory.Sites.Adjunction (#3663) commit c934e5d186bdc16bb6f0b181e3ebe1e95acbe333 Author: Eric Rodriguez <[email protected]> Date: Thu Apr 27 14:06:46 2023 +0000 chore: forward-port generalisation (#3679) * [`data.finsupp.basic`@`2651125b48fc5c170ab1111afd0817c903b1fc6c`..`57911c5a05a1b040598e1e1…
- Loading branch information
1 parent
739b4a8
commit f812f94