From f812f94ca3de27161c0cba156fb2563c9e251cd0 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 17 May 2023 21:46:39 -0400 Subject: [PATCH] Squashed commit of the following: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit commit 8377ae6b176cc857b383b04173fa5577d09f1689 Author: Matthew Ballard Date: Wed May 17 21:16:04 2023 -0400 update mathlib.lean commit 8d909eb33ad5e164db2deaf8444b0a21351ec99f Author: Matthew Ballard Date: Wed May 17 21:14:55 2023 -0400 lint commit 6bcb7f5e70763e15c405912988d867fbe0637691 Author: Matthew Ballard Date: Wed May 17 21:10:16 2023 -0400 fix last errors commit 1b85bed8887c82368d7da6f4189aea86e98991cb Author: Scott Morrison Date: Thu May 18 10:46:42 2023 +1000 fixes commit 519af1d828205304827466024ee65506eb99186e Merge: 98bf9f9b 8bf78812 Author: Scott Morrison 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 Date: Sat May 13 08:31:30 2023 -0400 Merge branch 'master' into port/CategoryTheory.Bicategory.Free commit 1910c612e2e43e3c263f68996ed72b9ac5204f6e Author: Matthew Ballard Date: Sat May 13 08:31:19 2023 -0400 add new file commit 7af7463b52e7a6d69eb7478235117c023ec8c6aa Merge: f0adc533 269fb63e Author: Matthew Ballard 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 Date: Wed May 10 05:02:09 2023 +0000 feat: port Analysis.Normed.Group.ControlledClosure (#3880) commit 628125292856eb71f72eeecd4f5f967f006ec773 Author: Kevin Buzzard 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 commit 21708212ef62b7ac824871864a8c3d103f320750 Author: Jason Yuen Date: Wed May 10 04:45:22 2023 +0000 feat: port Topology.ContinuousFunction.LocallyConstant (#3877) commit 5d84f9b67af72c588b96bb7821b2523f821b1bec Author: Jason Yuen Date: Wed May 10 01:01:27 2023 +0000 feat: port MeasureTheory.Covering.VitaliFamily (#3867) commit 4f3e6145116f5ddf98f9f2615f7e4b129bd02dce Author: Matthew Robert Ballard Date: Wed May 10 01:01:26 2023 +0000 feat: port Algebra.Category.Group.EquivalenceGroupAddGroup (#3861) commit 0d738a8fef346fb7f9020b327b61fe7f422d1524 Author: Pol_tta Date: Wed May 10 01:01:24 2023 +0000 feat: port Dynamics.Ergodic.MeasurePreserving (#3821) Co-authored-by: Scott Morrison Co-authored-by: MonadMaverick commit 9c00193316232966719be6916399504da82103c7 Author: Pol_tta Date: Wed May 10 01:01:22 2023 +0000 feat: port MeasureTheory.Measure.OpenPos (#3820) Co-authored-by: Komyyy Co-authored-by: Jeremy Tan Jie Rui commit 55413d4565e6e33a8ff7065b20a3f3f9ba18fc0d Author: Jason Yuen Date: Wed May 10 00:18:41 2023 +0000 feat: port Analysis.Convex.PartitionOfUnity (#3868) commit 468ee3fa8c1a4a81a0a1ce5829afc0e65226ea97 Author: Pol_tta Date: Wed May 10 00:18:39 2023 +0000 feat: port MeasureTheory.Lattice (#3824) Co-authored-by: Scott Morrison Co-authored-by: MonadMaverick commit 01d44eab0e102b78434bd20142f8e1db75e22599 Author: Pol_tta Date: Wed May 10 00:18:37 2023 +0000 feat: port MeasureTheory.Measure.MutuallySingular (#3818) Co-authored-by: Komyyy Co-authored-by: Jeremy Tan Jie Rui commit 3b3411e0739d9a22e8cabc54b724123a8d773333 Author: Kyle Miller 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 Date: Tue May 9 23:59:30 2023 +0000 feat: port Analysis.NormedSpace.CompactOperator (#3805) commit c10b02b9f02a8d212f1ab2cdd18440785e464c58 Author: Scott Morrison Date: Tue May 9 23:06:55 2023 +0000 feat: port CategoryTheory.Functor.Flat (#3703) Co-authored-by: Kevin Buzzard Co-authored-by: Scott Morrison Co-authored-by: Scott Morrison Co-authored-by: Parcly Taxel Co-authored-by: Yaël Dillies commit 64b7fb14e6a9085f2a3e6fa5bcce317a7120cc3a Author: Pol_tta Date: Tue May 9 19:44:35 2023 +0000 feat: port MeasureTheory.Measure.AEMeasurable (#3819) Co-authored-by: Komyyy Co-authored-by: Jeremy Tan Jie Rui commit 15da6c20b0e9b06b46b5c6b325f7d21be2d568b7 Author: Jason Yuen Date: Tue May 9 10:06:14 2023 +0000 feat: port Probability.ProbabilityMassFunction.Basic (#3865) commit 8ecbd9569ffd605712cd21b65d0d8864520dfb66 Author: Matthew Robert Ballard Date: Tue May 9 10:06:13 2023 +0000 feat: port CategoryTheory.Preadditive.InjectiveResolution (#3860) Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> commit da3993ff939d796018ff5e95c41712d1975abfa8 Author: Matthew Robert Ballard Date: Tue May 9 10:06:12 2023 +0000 feat: port Topology.Category.Top.Limits.Konig (#3853) Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> commit c3bace0cd04c23c1dd9ab361b03eb80faa8e2c3d Author: Jason Yuen Date: Tue May 9 09:46:42 2023 +0000 feat: port MeasureTheory.Measure.Sub (#3866) commit 99bb9fb7ca74cba20b2c2588d2fb9595e5cb98b7 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Tue May 9 08:58:57 2023 +0000 feat port: LinearAlgebra.ProjectiveSpace.Subspace (#3832) commit f273bff58209ed6273afcaf85b7bc554a7ceac3a Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue May 9 06:29:09 2023 +0000 chore: tidy various files (#3848) commit cfbec6e28f4c3d117debf58d1338e531cb90a3aa Author: Jason Yuen Date: Tue May 9 06:12:54 2023 +0000 feat: port Topology.PartitionOfUnity (#3863) commit 37807d6a99a0199676e029358f20ac5738d9639f Author: Matthew Robert Ballard Date: Tue May 9 06:12:53 2023 +0000 feat: port CategoryTheory.Preadditive.Injective (#3859) commit b75c4d73f2b15b8234a5dcdca62ad160ae9caf76 Author: Matthew Robert Ballard Date: Tue May 9 06:12:52 2023 +0000 feat: port Topology.Category.Top.Limits.Cofiltered (#3855) commit b1ee18a7fb8e0079cb0c0fd0fea1afd019219fe5 Author: David Renshaw 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 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 Co-authored-by: ChrisHughes24 Co-authored-by: Jeremy Tan Jie Rui commit d52008fd7cc8539b1d1b32c9eac2b0aeac276244 Author: Eric Wieser 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 Date: Mon May 8 21:09:37 2023 +0000 feat: port Topology.ContinuousFunction.Algebra (#3332) Co-authored-by: Eric Wieser Co-authored-by: Scott Morrison Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Christopher Hoskin Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: qawbecrdtey Co-authored-by: Jireh Loreaux commit 6863ef07ca5aa72edacb87d14977f8816aa3951d Author: sgouezel 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 Date: Mon May 8 13:36:25 2023 +0000 chore: fix name in Mathlib.Topology.Algebra.Module (#3850) Co-authored-by: Scott Morrison commit 51e2e32cd407e1965885af13d1a9bb96e0709c05 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Mon May 8 11:53:12 2023 +0000 feat port: Topology.Algebra.Nonarchimedean.AdicTopology (#3826) commit a5f2b200a2c1fb019a358e347353e19f09402bd5 Author: Jason Yuen Date: Mon May 8 11:21:34 2023 +0000 feat: port Data.Complex.Orientation (#3849) commit 2906eb7cfd4f8b36322c63e0209c06e0353a5261 Author: Pol_tta Date: Mon May 8 10:01:09 2023 +0000 feat: port MeasureTheory.Tactic (#3816) commit b5c7cda33ead3895a3e92b9b41112bdc755a433a Author: Jujian Zhang 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 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 <52843868+Komyyy@users.noreply.github.com> commit b840606e7074798762c81e73e53ac4ab2e661de5 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> 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 commit 882005842a71af115186357b21dd4f2bbfe2a597 Author: Jason Yuen Date: Mon May 8 05:55:40 2023 +0000 feat: port Analysis.SpecificLimits.Normed (#3419) Co-authored-by: Moritz Firsching Co-authored-by: Scott Morrison commit c2cf5ba958fb0ac9b1536f66d98b73a486aabaee Author: Pol_tta 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 Date: Mon May 8 03:29:53 2023 +0000 feat: port Data.Sym.Card (#3109) Co-authored-by: int-y1 commit 016b02ed781f7804fe6c002d33eabc205a5e30de Author: Pol_tta Date: Mon May 8 03:07:17 2023 +0000 feat: port Computability.Partrec (#3830) commit 28e49fca3bcedc90c9149a26c10c338ebc00d7a5 Author: Jason Yuen Date: Mon May 8 02:51:12 2023 +0000 feat: port Topology.Category.Top.OpenNhds (#3834) commit a5a10ca18c91a12454b6317e637d69586c33448c Author: Eric Wieser Date: Mon May 8 00:54:18 2023 +0000 chore: forward-port leanprover-community/mathlib#18878 (#3742) commit 4350c4e364eda158598503baf5916729406f4e95 Author: Yury G. Kudryashov Date: Mon May 8 00:54:17 2023 +0000 feat: port Analysis.Normed.Group.Quotient (#3457) Co-authored-by: Mauricio Collares commit cd0670b6fbe9fc3398ce064cd55f7464e15d7353 Author: Moritz Doll 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 Date: Sun May 7 14:02:40 2023 +0000 feat: port Algebra.ContinuedFractions.Computation.Translations (#3794) Co-authored-by: Moritz Firsching Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel commit 0285c2bf3919356b608125ae878487201d15b488 Author: Jeremy Tan Jie Rui Date: Sun May 7 13:25:52 2023 +0000 chore: forward port leanprover-community/mathlib#18951 (#3837) commit 0633b89bb4e7148fcb22a6c26915d79838a11ad5 Author: Jeremy Tan Jie Rui Date: Sun May 7 09:18:13 2023 +0000 chore: forward port leanprover-community/mathlib#18866 (#3813) commit b3b1b7dd2388506eceadab75d83ca8183aeeb496 Author: Scott Morrison 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 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Scott Morrison Co-authored-by: Scott Morrison commit c993a4e8f1a1d2c587b3d939af778d3bf3dff420 Author: Jeremy Tan Jie Rui Date: Sun May 7 08:52:06 2023 +0000 chore: forward port leanprover-community/mathlib#18479 (#3829) commit 038caab459760a87b476351dfd62b7ab2a50bee5 Author: Scott Morrison 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 Co-authored-by: Scott Morrison commit 18c6e24d4a7c5ec87e4c7e9e295e852475c70c55 Author: Eric Wieser Date: Sun May 7 07:13:52 2023 +0000 chore: forward-port leanprover-community/mathlib#18934 (#3806) Co-authored-by: Parcly Taxel commit 424263023c2e9c1588f05d9a28a5abb9ae8ae88b Author: Eric Wieser Date: Sun May 7 07:13:51 2023 +0000 chore: forward-port leanprover-community/mathlib#18902 (#3770) commit 8a2c2bf047940fdad965814424f3a2c1d8a6644d Author: Jeremy Tan Jie Rui 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 郭俊余) 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 Co-authored-by: Jeremy Tan Jie Rui commit 55705f9084276a7a7de523230af1827ba60fb949 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat May 6 19:21:52 2023 +0000 ci: make bors block on the check_imported job (#3827) commit f72485cdca5b6010514168873616232d7765dc90 Author: Scott Morrison Date: Sat May 6 15:10:58 2023 +0000 chore: bump to Lean 4 nightly-2023-05-06 (#3817) Co-authored-by: Scott Morrison commit f1ae5b7ec8d705042684482b8fb06cd34adfcb65 Author: Scott Morrison 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 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Kyle Miller Co-authored-by: Patrick Massot Co-authored-by: Floris van Doorn Co-authored-by: Scott Morrison commit ec38b915d3a36cb7d0adef661259453be01c4728 Author: MonadMaverick Date: Sat May 6 11:29:51 2023 +0000 feat: port MeasureTheory.Measure.NullMeasurable (#3349) Co-authored-by: MonadMaverick Co-authored-by: Jeremy Tan Jie Rui commit d8f1f02fd6a548ea4d1f944972a929089cca5869 Author: Jeremy Tan Jie Rui Date: Sat May 6 08:46:32 2023 +0000 chore: forward port leanprover-community/mathlib#18910 (#3814) commit 79ca50dced9a0a479fd0da6941f7cd67a9927d9e Author: Patrick Massot 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 Co-authored-by: Kyle Miller commit b7ed6f5bb61ecc043f01aa3b27276188ba1a2cdf Author: Yury G. Kudryashov 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 <46200072+xroblot@users.noreply.github.com> Date: Sat May 6 07:33:35 2023 +0000 feat port : RingTheory.Ideal.AssociatedPrime (#3810) commit a31acfcf3520728bef79bcfa4e0275466a0834ab Author: EmilieUthaiwat Date: Sat May 6 07:17:10 2023 +0000 feat: port LinearAlgebra.Lagrange (#3784) commit 2617ac0e6b300c20d8bb10198fafe9332d45df5a Author: MonadMaverick Date: Sat May 6 06:40:03 2023 +0000 feat: port MeasureTheory.Measure.AEDisjoint (#3351) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Komyyy commit 214014d2c39d5fe770fbb305588808bcb1a4aff4 Author: Scott Morrison 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 Co-authored-by: Eric Wieser commit 35f51927282d120df99e96c037ddfb4132e947bf Author: Eric Wieser Date: Fri May 5 14:00:33 2023 +0000 chore: forward-port leanprover-community/mathlib#18906 (#3798) commit ddf1a04c942b901a07d053d2f967f2ad40777e1a Author: Jason Yuen Date: Fri May 5 13:44:48 2023 +0000 feat: port MeasureTheory.Function.AEMeasurableSequence (#3803) commit e0fd3f7dbf994599af312d5f630bf7fcedbb9bce Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri May 5 12:24:18 2023 +0000 chore: tidy various files (#3718) commit f4dd3adaf6847e2e940853c1d3d2b36aaa781425 Author: Eric Wieser 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 Date: Thu May 4 19:07:27 2023 +0000 feat: port Algebra.ContinuedFractions.ConvergentsEquiv (#3795) commit 3a802fc9446bc158d1486997f5f5794e4c402beb Author: Yaël Dillies 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 commit d9ea05decd47313168b7f7febd64643ff7ed1932 Author: Eric Wieser Date: Thu May 4 11:23:11 2023 +0000 chore: forward-port leanprover-community/mathlib#18922 (#3779) commit 4b452a9fec289cc8ed1e18098680ab0db19079d4 Author: Eric Wieser Date: Thu May 4 11:23:10 2023 +0000 chore: forward-port leanprover-community/mathlib#18876 (#3753) commit 45acfec0369c6720452249bdf860cbeafa89c25b Author: Eric Wieser Date: Thu May 4 11:23:09 2023 +0000 chore: forward-port leanprover-community/mathlib#18879 (#3741) commit 700eb94e185cb781b1f8945cb350ff3051f4a52a Author: Moritz Firsching Date: Thu May 4 09:12:04 2023 +0000 feat: port Algebra.ContinuedFractions.TerminatedStable (#3792) Co-authored-by: Moritz Firsching commit d7a6de21586b9f2fd41676da624f6fc4ccd3eb18 Author: Jason Yuen Date: Thu May 4 09:12:03 2023 +0000 feat: port Algebra.ContinuedFractions.Computation.Basic (#3788) Co-authored-by: Moritz Firsching commit c643d1282c5c47f210c9497d1e19867dbd1bcb74 Author: MonadMaverick Date: Thu May 4 08:44:21 2023 +0000 feat: port MeasureTheory.Measure.MeasureSpaceDef (#3325) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Komyyy commit 6ee07bd7ff39032233031f056c2649ccda4cafef Author: Moritz Firsching Date: Thu May 4 08:21:57 2023 +0000 feat: port Algebra.ContinuedFractions.ContinuantsRecurrence (#3791) Co-authored-by: Moritz Firsching commit ac2e5438c8c07b7c63166df1bdf15076028c4159 Author: Moritz Firsching Date: Thu May 4 05:47:35 2023 +0000 feat: port Algebra.ContinuedFractions.Translations (#3783) Co-authored-by: Moritz Firsching commit e34f9b0fc494772fc304aeffa32e829278a17962 Author: Kyle Miller 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 Date: Wed May 3 22:31:52 2023 +0000 chore: update Mathlib/Tactic.lean (#3727) Co-authored-by: Scott Morrison commit 2f62a68be3bd7b099d591820492b5eb668f3843e Author: Alex J Best 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 <68410468+thorimur@users.noreply.github.com> 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 commit 8cad0a826486d2a0005de7e353e12f2ae143b78e Author: Jason Yuen Date: Wed May 3 13:39:19 2023 +0000 feat: port LinearAlgebra.AffineSpace.FiniteDimensional (#3670) commit 052deed907b6ffc756bd7ce4ecdedf4d6db1068d Author: JeEyben <124388640+JeEyben@users.noreply.github.com> Date: Wed May 3 13:39:17 2023 +0000 feat: port RingTheory.Localization.InvSubmonoid (#3384) Co-authored-by: int-y1 commit 5a77592a11f98444a19c2ea97fad0291fe408b96 Author: Jason Yuen Date: Wed May 3 13:39:15 2023 +0000 feat: port Algebra.ContinuedFractions.Basic (#3379) Co-authored-by: Jon Eugster commit 8f6e4d2054a99fd8c847cacfe57b408b8b18646a Author: Moritz Firsching Date: Wed May 3 13:39:13 2023 +0000 feat: port CategoryTheory.Monoidal.Free.Basic (#2808) Co-authored-by: Moritz Firsching Co-authored-by: Scott Morrison Co-authored-by: Joël Riou Co-authored-by: Johan Commelin commit 30a890eb4e9dbda9dd9dc42c4e2f260b59abb214 Author: Scott Morrison 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 commit 814f492f80e97836913d1b788911a1ddc76b6f42 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> 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 commit 0ab5e61ca44a52206df99830a0facaf91d8b803e Author: Moritz Doll Date: Wed May 3 11:33:41 2023 +0000 docs: fix names in Analysis.LocallyConvex.Bounded (#3774) commit ac0fd896f1bb1f197f25f5f654a859b4a02d8516 Author: MonadMaverick Date: Wed May 3 11:02:26 2023 +0000 feat: port MeasureTheory.Measure.OuterMeasure (#3674) Co-authored-by: Scott Morrison Co-authored-by: Komyyy Co-authored-by: Johan Commelin commit ae90d57d66ab4137eb22d9152cdd2d6aa0f19cd6 Author: Jason Yuen Date: Wed May 3 06:27:24 2023 +0000 feat: port LinearAlgebra.AffineSpace.Matrix (#3775) commit 3ad45ada879ff7d1eb0c425df6bf8d4bec66adba Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Date: Wed May 3 01:24:20 2023 +0000 feat port: Algebra.FreeModule.Determinant (#3767) commit c577bee1ea0537d6a4488ad569f3252ed2123784 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:19 2023 +0000 feat: port Data.Complex.Determinant (#3765) commit c89277f05e074a327f79381c14d659b05e68168b Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:17 2023 +0000 feat: port Analysis.SpecialFunctions.Trigonometric.Chebyshev (#3764) commit 1dac593b7e1c149c4d234973754b4347de968595 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:16 2023 +0000 feat: port Analysis.Convex.Complex (#3763) commit efb20cbedfb68cb1b2967449ef92b374c0f9724b Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:16 2023 +0000 feat: port Data.Matrix.Rank (#3762) commit a65601d186c742e05cece1797b1046322f8f16f4 Author: Joël Riou Date: Wed May 3 01:24:14 2023 +0000 feat: port CategoryTheory.Category.Groupoid (#3761) commit 4ddf8c7c266db2c9486475955bfb75a6ccafc360 Author: Yaël Dillies 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 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 commit 391cddce21029cb45a255a2ab063c7d3b98b4b60 Author: Jeremy Tan Jie Rui Date: Tue May 2 16:51:37 2023 +0000 feat: port Topology.Algebra.Module.Determinant (#3766) commit fed5a971cac804f30a3b4b2550bc532e0b1adbaf Author: Scott Morrison 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 commit 3f6f6282cc137af13d6c480744e58dedca712c1e Author: Scott Morrison 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 commit 92a23d50515de9ac1baf29a66826ee77305b2b91 Author: Joël Riou Date: Tue May 2 10:23:03 2023 +0000 feat: port CategoryTheory.Monoidal.Tor (#3754) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> commit 179b81ee4cadef2f601e1f1265d266ea0cf91cd7 Author: Eric Wieser 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 Date: Tue May 2 10:05:14 2023 +0000 feat: port LinearAlgebra.Determinant (#3694) Co-authored-by: int-y1 Co-authored-by: Komyyy Co-authored-by: Scott Morrison Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Eric Wieser commit 8d401bd92990dec5d9d1aa59094789f607caf2d0 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue May 2 07:59:21 2023 +0000 feat: port Data.Complex.Module (#3737) Co-authored-by: int-y1 Co-authored-by: Eric Wieser commit 0227fbbc71c1ce40bb9338c52058d0a34565653c Author: Alex J Best 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 Date: Mon May 1 22:19:22 2023 +0000 feat: port CategoryTheory.Functor.LeftDerived (#3751) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> Co-authored-by: Scott Morrison commit e57a8f962faca1a6949a74daec03e5b350995af8 Author: Joël Riou Date: Mon May 1 22:19:21 2023 +0000 feat: port CategoryTheory.Sites.LeftExact (#3706) commit fc3894f2f75c7b860783e8a90fd767bcb00b2cb9 Author: Pol_tta 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 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 Date: Mon May 1 20:06:10 2023 +0000 feat: port CategoryTheory.Preadditive.ProjectiveResolution (#3740) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> commit 52e6ad71693190465481e0ae20d97913dbba06e9 Author: Yaël Dillies 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 commit 5b940a6dc1a1bd5f2f4a6f271059bbea0e3857bc Author: Yury G. Kudryashov Date: Mon May 1 17:47:54 2023 +0000 feat: port CategoryTheory.Abelian.Exact (#3638) Co-authored-by: Moritz Firsching Co-authored-by: Joël Riou commit 0ea443f63e211696d5a166c82f7469cc2cdc1d82 Author: Yaël Dillies 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 commit e95cccde5645c855b0c08a5fb4d944adf442a4b7 Author: Jeremy Tan Jie Rui Date: Mon May 1 13:19:51 2023 +0000 feat: port Topology.Category.Profinite.Projective (#3746) commit 55637dc9d43c30243cb0d8578cabcabf4dedbc8c Author: Moritz Firsching Date: Mon May 1 11:02:54 2023 +0000 feat: port Mathlib.Data.Ordmap.Ordnode (#1455) Co-authored-by: Arien Malec Co-authored-by: Floris van Doorn Co-authored-by: Moritz Firsching Co-authored-by: qawbecrdtey commit 64d186af31d440f3743d6862c0f39cf553fcdca1 Author: Violeta Hernández 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 Co-authored-by: Yaël Dillies commit 5925a364a984ab06f0d1b425339c4bb5cd1b2646 Author: Scott Morrison Date: Mon May 1 01:58:20 2023 +0000 feat: port Topology.Category.Profinite.Basic (#3705) Co-authored-by: Scott Morrison Co-authored-by: adamtopaz commit c272f4940037d117009ce720b7aba0bad3986627 Author: Alex J Best 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 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 Date: Sun Apr 30 11:38:03 2023 +0000 feat: port FieldTheory.Tower (#3716) Co-authored-by: Eric Wieser Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> commit 76707255936de099ae6835e7ddbe5f7bf95a7a36 Author: Joël Riou Date: Sat Apr 29 23:07:53 2023 +0000 feat: port Algebra.Category.Group.ZModuleEquivalence (#3732) commit 543b8ec1ea21d7a3321234bb0b6532576a897c61 Author: Joël Riou Date: Sat Apr 29 23:07:52 2023 +0000 feat: port AlgebraicTopology.ExtraDegeneracy (#3729) commit eb11681ef13f0d1aba2ff267a20bd08883484f82 Author: Jeremy Tan Jie Rui Date: Sat Apr 29 22:52:42 2023 +0000 feat: port CategoryTheory.Monad.Coequalizer (#3733) commit 6a28eee3a21942016a01bbada70ce9a6a40ba8e5 Author: Moritz Firsching Date: Sat Apr 29 22:28:56 2023 +0000 chore: no newline before aligns (#3735) Co-authored-by: Moritz Firsching commit a7e9e4ab120a3b6d10251d3c3d24a1e60c13dca8 Author: Yaël Dillies 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 commit dc012f816b787bcb80007f2bc1b5e6604aa57b28 Author: Jeremy Tan Jie Rui Date: Sat Apr 29 13:32:59 2023 +0000 feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728) Co-authored-by: ChrisHughes24 commit 8dd639e1083340aed6138d8ad7f954091b037267 Author: Scott Morrison Date: Sat Apr 29 13:32:58 2023 +0000 fix: find MathlibExtras from downstream projects (#3721) Co-authored-by: Scott Morrison commit 73bab6a59163675f3f1f26530bac9c2571eba84b Author: Scott Morrison Date: Sat Apr 29 13:32:57 2023 +0000 fix: allow library_search to run when maxHeartbeats = 0 (#3720) Co-authored-by: Scott Morrison commit 301ea2db46c56d28eb73f418ab992b0010e5f75d Author: Yaël Dillies 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 commit f667fdec730173011b40f4dcea8c79c33eed39b6 Author: Joël Riou Date: Sat Apr 29 13:32:55 2023 +0000 feat: port CategoryTheory.Abelian.Transfer (#3424) commit 029b212612c336f75d26163cebd5e129a455847e Author: Alex J Best 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 Date: Sat Apr 29 09:57:49 2023 +0000 feat: port LinearAlgebra.ProjectiveSpace.Basic (#3692) commit d2c96a57df11efb8eec9f31377e5de800012433c Author: Jason Yuen Date: Sat Apr 29 05:39:03 2023 +0000 chore: add hash for Data.MvPolynomial.Polynomial (#3723) commit 288a7d79cf1b6dfd4940082700efa5b8dc15d496 Author: Jason Yuen Date: Sat Apr 29 03:33:44 2023 +0000 feat: port LinearAlgebra.SymplecticGroup (#3696) commit 3230cdeee0ab5da8fc47680e4d5da87addcc90e7 Author: Alex J Best Date: Fri Apr 28 23:45:34 2023 +0000 feat: make alias compile code when possible (#3719) commit 36844e9cb778e4e857c8c9b0b0339c876679f4a8 Author: Eric Wieser Date: Fri Apr 28 23:45:32 2023 +0000 chore: forward-port leanprover-community/mathlib#18880 (#3717) commit 24f74e319f706f55aef284703cddec753ffadb62 Author: Yaël Dillies 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 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 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 Date: Fri Apr 28 18:56:37 2023 +0000 feat: Port Topology.Category.CompHaus.Projective (#3715) commit 863aebc8ccf10ff0c19a25fad7344e8a585c9108 Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> 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 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 Date: Fri Apr 28 14:00:44 2023 +0000 feat: port LinearAlgebra.Matrix.Transvection (#3700) Co-authored-by: Moritz Firsching Co-authored-by: ChrisHughes24 commit 3d576486048be2cbae503d1c1e7f5a0a85b66a6c Author: Yaël Dillies 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 Date: Fri Apr 28 11:10:45 2023 +0000 feat: port CategoryTheory.Action (#3657) commit bc85faaf38cdda2b9c3f808ba563c232f5f815a0 Author: Yury G. Kudryashov Date: Fri Apr 28 11:10:44 2023 +0000 feat: port CategoryTheory.Preadditive.Projective (#3615) Co-authored-by: Joël Riou Co-authored-by: Scott Morrison commit b98b04707b0c77941e61f598a4b8c8164a2c2482 Author: Moritz Firsching Date: Fri Apr 28 10:54:06 2023 +0000 feat: port LinearAlgebra.Matrix.ZPow (#3671) Co-authored-by: Moritz Firsching Co-authored-by: Parcly Taxel commit cd980733e0e92568cb77dbb4a9c0f6b3498dc9ce Author: Jeremy Tan Jie Rui Date: Fri Apr 28 09:49:14 2023 +0000 feat: port LinearAlgebra.Matrix.FiniteDimensional (#3698) commit 740bbec09993a7a71a993aaf7fdee3571005215c Author: Bulhwi Cha 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 Date: Fri Apr 28 06:56:28 2023 +0000 feat: port LinearAlgebra.Matrix.InvariantBasisNumber (#3697) commit 15d98e6b55a610e11d16e02aca4fc7be760c5ffd Author: Jeremy Tan Jie Rui Date: Fri Apr 28 06:56:27 2023 +0000 feat: port AlgebraicTopology.Nerve (#3693) commit e35da366b8e442a61e77516edd8197e8715264b5 Author: Eric Wieser Date: Fri Apr 28 06:56:26 2023 +0000 forward-port leanprover-community/mathlib#18840 (#3678) commit d456dd3ce4146aa82e05ac02aae437901b534fc1 Author: Eric Wieser Date: Fri Apr 28 06:56:25 2023 +0000 chore: forward-port leanprover-community/mathlib#18802 (#3677) commit e234e1dbab60d5cb2491ee19f608fe6357d7244c Author: Eric Wieser Date: Fri Apr 28 06:56:24 2023 +0000 chore: forward-port leanprover-community/mathlib#18869 (#3676) commit bd1736fa511c00b8607b3e1134213cd963b923c1 Author: Eric Wieser Date: Fri Apr 28 06:56:23 2023 +0000 chore: forward-port leanprover-community/mathlib#18842 (#3675) commit 7d4f125478272f478180c413365372d3069e8a63 Author: Yaël Dillies 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 commit 535bb666094594a96afc3f425fe1c5cd49261836 Author: Eric Wieser 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 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 <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 05:58:44 2023 +0000 feat: port LinearAlgebra.Matrix.Basis (#3691) Co-authored-by: Parcly Taxel Co-authored-by: Eric Wieser Co-authored-by: Scott Morrison Co-authored-by: Komyyy Co-authored-by: Johan Commelin commit 6fc9d5e9d711f3812bbd7cd0fbeb2fed11cf9c6e Author: Jeremy Tan Jie Rui <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 05:41:51 2023 +0000 feat: port LinearAlgebra.FreeModule.Finite.Matrix (#3690) Co-authored-by: Parcly Taxel Co-authored-by: Eric Wieser Co-authored-by: Scott Morrison Co-authored-by: Johan Commelin commit 7b0b99d0366fcca78f849aaef42e8dcd0975ed66 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 03:54:51 2023 +0000 feat: port LinearAlgebra.Matrix.ToLin (#3552) Co-authored-by: Parcly Taxel Co-authored-by: Eric Wieser Co-authored-by: Scott Morrison commit 4f6380966f207897ef1487010c80d15f24769971 Author: Joël Riou Date: Fri Apr 28 02:53:49 2023 +0000 feat: port AlgebraicTopology.SimplicialSet (#3689) commit 7b88b65bd51282f240fc40b1bd6c1e7d8c227be6 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 02:53:48 2023 +0000 ci: lint references.bib (#3683) Ported from mathlib3. commit b8ad9541c1a9fb132cad12283b3accc56c5ed35e Author: Moritz Firsching Date: Fri Apr 28 02:53:47 2023 +0000 chore: rename Zpowers -> ZPowers (#3681) Co-authored-by: Moritz Firsching commit eb417549e64541742039abd0dc9b823388124907 Author: Jeremy Tan Jie Rui Date: Fri Apr 28 02:33:14 2023 +0000 feat: port Topology.Algebra.Module.Multilinear (#3348) Co-authored-by: Eric Wieser Co-authored-by: ADedecker Co-authored-by: Scott Morrison commit fe28ed480a44857c878f429eabc66b9fee4f3a45 Author: Jeremy Tan Jie Rui Date: Fri Apr 28 01:23:38 2023 +0000 feat: port Topology.Algebra.Module.StrongTopology (#3684) Co-authored-by: ADedecker Co-authored-by: Scott Morrison commit 1113f1cefa6387fb404087427f48596810d95acb Author: Henrik Böving Date: Fri Apr 28 00:11:16 2023 +0000 fix: mathlib4_docs cleanup routine (#3631) commit ed822e7be3f58018b6fd816b957fd888db4b35c2 Author: Kevin Buzzard 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 Co-authored-by: Scott Morrison commit 78d77dfbcae2747913005e50dad80692cb1ff940 Author: Adam Topaz Date: Thu Apr 27 23:18:23 2023 +0000 feat: Port Topology.Category.CompHaus.Basic (#3688) Relatively straightforward port. Co-authored-by: Scott Morrison commit d1a1c6b104967ffed8ca69ebb4f3ea9a4eb25424 Author: Joël Riou Date: Thu Apr 27 21:43:33 2023 +0000 feat: port Analysis.Convex.StoneSeparation (#3686) commit 2f36c58966790d0a91aaa910836751e289259f12 Author: Joël Riou Date: Thu Apr 27 21:43:32 2023 +0000 feat: port CategoryTheory.Noetherian (#3685) commit aaa5e0a421c8b53d60e6b7d1341ade2d5b2e59b3 Author: Felix-Weilacher 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 commit 2dab08df0323c6e58ace9b611c7e951602d0a2c0 Author: Joël Riou Date: Thu Apr 27 15:27:17 2023 +0000 feat: port CategoryTheory.Sites.Adjunction (#3663) commit c934e5d186bdc16bb6f0b181e3ebe1e95acbe333 Author: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> Date: Thu Apr 27 14:06:46 2023 +0000 chore: forward-port generalisation (#3679) * [`data.finsupp.basic`@`2651125b48fc5c170ab1111afd0817c903b1fc6c`..`57911c5a05a1b040598e1e15b189f035ac5cc33c`](https://leanprover-community.github.io/mathlib-port-status/file/data/finsupp/basic?range=2651125b48fc5c170ab1111afd0817c903b1fc6c..57911c5a05a1b040598e1e15b189f035ac5cc33c) commit 61deb6d2082aed5b476773d9ef390ffecab8bd2d Author: Jeremy Tan Jie Rui Date: Thu Apr 27 14:06:45 2023 +0000 feat: port Topology.Algebra.UniformConvergence (#3664) Co-authored-by: Scott Morrison commit 129f0cd1aa8af4b70cf251f5d724d638dfe1f7b2 Author: Matthew Robert Ballard Date: Thu Apr 27 14:06:43 2023 +0000 feat: port Topology.Category.Top.Limits.Basic (#3487) Co-authored-by: Scott Morrison Co-authored-by: Scott Morrison Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel Co-authored-by: adamtopaz commit 014f4b7b748e1300f0e3580a79ad4f67a723ae22 Author: Scott Morrison Date: Thu Apr 27 12:44:20 2023 +0000 chore: use etaExperiment rather than hacking with instances (#3668) This is to fix timeouts in https://github.com/leanprover-community/mathlib4/pull/3552. See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233552.20.28LinearAlgebra.2EMatrix.2EToLin.29. Co-authored-by: Scott Morrison commit 5da04b2a99bc742bafdcec6c5765b0d126fc6db6 Author: Scott Morrison Date: Thu Apr 27 08:42:08 2023 +0000 chore: use TypeMax in CategoryTheory.Limits.Types (#3653) Per discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233463.20universe.20constraint.20issues Co-authored-by: Scott Morrison Co-authored-by: Matthew Ballard commit 7f9d406a54a6ddfd2954f0328adbba96351c4b8c Author: Pol_tta Date: Thu Apr 27 06:19:30 2023 +0000 feat: port LinearAlgebra.Matrix.Block (#3667) commit 69ef22790023ac4ecb94eb632a07f58f3847f89c Author: Bulhwi Cha Date: Thu Apr 27 06:19:29 2023 +0000 doc: move comments (#3666) Two comments were in the wrong places. commit c110a371954632a6316c59765ba289f3d3ea8dc9 Author: Eric Wieser Date: Thu Apr 27 06:19:28 2023 +0000 fix: correct field names in `IsCompl` (#3661) These are proofs not propositions so should be `lowerCamelCase`. Co-authored-by: Parcly Taxel commit 3aa7ccad258677f1cfcde1465e59473c735686d5 Author: Scott Morrison Date: Thu Apr 27 06:19:27 2023 +0000 feat: instant library_search (#3404) Well, not quite instant, but very much faster. This works by creating an extra file in the `build` directory containing a cache of the `library_search` discrimination tree. * If you modify a file, then open another file, `library_search` will not see the modified declarations. * However after a `lake exe cache get` or a `lake env lean Extras/LibrarySearch.lean`, you will see the modifications. * In particular CI will automatically do the work of building this cache. * This will increase the size of a `lake exe cache get` download (by about 20mb). To accommodate the cache file, we create a new `build/extra/` directory, that can store `.olean` format cache files. Our `cache` executable now manages files in this directory too. Co-authored-by: Scott Morrison Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: EmilieUthaiwat Co-authored-by: Eric Wieser Co-authored-by: Yaël Dillies Co-authored-by: Jireh Loreaux Co-authored-by: Gabriel Ebner Co-authored-by: Violeta Hernández commit 0d34b122d0ed66402b53b43b8a2af7e44ffa4ad0 Author: Scott Morrison Date: Thu Apr 27 06:05:34 2023 +0000 chore: copy across references.bib (#3665) Co-authored-by: Scott Morrison commit c8ecd1cfdd089c55011cff78fc527eac7239ba59 Author: Jeremy Tan Jie Rui Date: Thu Apr 27 02:53:43 2023 +0000 feat: port CategoryTheory.Simple (#3510) commit 36eb621579ff0d32909005877187902912d87da2 Author: Joël Riou Date: Thu Apr 27 02:37:38 2023 +0000 feat: port Topology.Category.Top.Opens (#3662) commit a6b9901d3f51488cf7748ffc6ac8f7a222ee4bb0 Author: Jeremy Tan Jie Rui Date: Wed Apr 26 23:45:09 2023 +0000 feat: port Analysis.LocallyConvex.Bounded (#3656) commit a85449779d224a64e4cd35b9576d6a007cdd885a Author: Eric Rodriguez Date: Wed Apr 26 12:39:02 2023 +0000 chore: forward-port leanprover-community/mathlib#18852 (#3646) This additionally makes a further small generalization to some of the finsupp instances (labelled with porting notes) which should be backported. The new statement of `Rat.smul_one_eq_coe` fixes a proof in `Mathlib/Analysis/NormedSpace/Basic.lean` that was mangled during porting. Co-authored-by: Eric Wieser commit b32f01a669c6f3e174c45e37312e184e565734af Author: Jason Yuen Date: Wed Apr 26 11:37:33 2023 +0000 feat: port Analysis.BoxIntegral.Partition.Split (#3658) commit 82bbfd1702c29a3291ad6683fa05384b808b6739 Author: Yury G. Kudryashov Date: Wed Apr 26 07:58:11 2023 +0000 feat: port Topology.Instances.Matrix (#3655) commit 1af0bb433142a92e0c980bda3668a3f0e7407e2d Author: Bulhwi Cha Date: Wed Apr 26 05:15:50 2023 +0000 doc: fix typo and omission (#3614) * Capitalize the first letter of the docstring of `String.leftpad`. * Enclose in backticks 'A' in the docstring of `String.head`. commit afdc0e1725bf410cd6f27585e968f9a9cdc6d520 Author: Jeremy Tan Jie Rui Date: Wed Apr 26 04:57:05 2023 +0000 feat: port Analysis.Seminorm (#3484) Co-authored-by: Scott Morrison Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> Co-authored-by: Eric Wieser commit 70dd49f500b4b04ebd78dff077586c75cdd7aa5a Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed Apr 26 04:18:25 2023 +0000 feat: port Analysis.BoxIntegral.Partition.Basic (#3438) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: int-y1 commit 93a1c0c4a822e59c49e41d912bdab7d41ee615d4 Author: Yury G. Kudryashov Date: Tue Apr 25 20:39:42 2023 +0000 feat: port Analysis.Convex.Join (#3633) commit 0d45f992f310f3579f5291f31b4b514a26118343 Author: Jeremy Tan Jie Rui Date: Tue Apr 25 17:50:27 2023 +0000 feat: port Analysis.NormedSpace.Star.Basic (#3650) commit 1c941ac3d247eb97fdc885c0df90f6ac44026efc Author: Eric Wieser Date: Tue Apr 25 17:50:26 2023 +0000 fix: add missing `_root_` (#3630) Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your `#align` statement complains the def doesn't exist, **don't change the #align**; work out why it doesn't exist instead. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel commit 2c927c7b9baa50c50d5283366264d5c36c34cb31 Author: Jeremy Tan Jie Rui Date: Tue Apr 25 15:53:42 2023 +0000 feat: port Analysis.NormedSpace.ConformalLinearMap (#3648) commit ae5c72b9c1d5a8293faa89474ed8e84294a1648a Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue Apr 25 15:53:41 2023 +0000 feat: port LinearAlgebra.Matrix.NonsingularInverse (#3647) commit 09eb0542ff6c70519dad766f3572145367cc4655 Author: Joël Riou Date: Tue Apr 25 15:37:40 2023 +0000 feat: port Algebra.Category.Module.Tannaka (#3645) commit 4c683c5a4d14cea2f2da6ca730d040dab056cf0e Author: Jason Yuen Date: Tue Apr 25 11:43:00 2023 +0000 feat: port Analysis.Convex.Independent (#3641) commit 22c1fbe5e2b004407d43a6d075db20af22fbb5b9 Author: Jeremy Tan Jie Rui Date: Tue Apr 25 11:42:58 2023 +0000 chore: fix #align lines (#3640) This PR fixes two things: * Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks. * **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.) commit 381b81bfb3f9fb575f4503f5b3bd338c706ba8e5 Author: Jason Yuen Date: Tue Apr 25 11:42:57 2023 +0000 feat: port Analysis.Convex.Caratheodory (#3639) commit 4642a69fb4c973da62e97aa0bebe74d36a610e8f Author: Joël Riou Date: Tue Apr 25 11:42:56 2023 +0000 feat: port CategoryTheory.Adjunction.AdjointFunctorTheorems (#3628) Co-authored-by: Moritz Firsching Co-authored-by: qawbecrdtey commit 91f46c807436b9a49df062f7ef96dfee26a57da8 Author: Jeremy Tan Jie Rui Date: Tue Apr 25 11:42:55 2023 +0000 feat: port LinearAlgebra.FiniteDimensional (#3466) Co-authored-by: Parcly Taxel Co-authored-by: Eric Wieser Co-authored-by: Johan Commelin Co-authored-by: Scott Morrison commit df73e9efe617dedaf95e4e4bf7da4df8730d2b56 Author: Filippo A. E. Nuccio Date: Tue Apr 25 11:42:53 2023 +0000 feat: port Analysis.NormedSpace.LinearIsometry (#3289) Co-authored-by: Parcly Taxel Co-authored-by: Scott Morrison commit 83e5d02291e001759284364acb34a5bbd3b25d64 Author: Jason Yuen Date: Tue Apr 25 11:29:21 2023 +0000 feat: port Analysis.Convex.SimplicialComplex.Basic (#3643) commit d872ea6939095b897026a58731f90bbfdb39352b Author: Joël Riou Date: Tue Apr 25 11:14:28 2023 +0000 feat: port CategoryTheory.Preadditive.Generator (#3644) commit 1c0afd96abb9db48577055ff7507a9113f9387a1 Author: Joël Riou Date: Tue Apr 25 09:36:42 2023 +0000 feat: port CategoryTheory.Limits.Constructions.WeaklyInitial (#3627) Co-authored-by: qawbecrdtey Co-authored-by: Joël Riou commit 496f7b347f764615618ab044a9c0ac05d27e790f Author: Yaël Dillies Date: Tue Apr 25 08:27:23 2023 +0000 feat: Dot product of block matrices (#3642) Match https://github.com/leanprover-community/mathlib/pull/8289 [`data.matrix.block`@`3e068ece210655b7b9a9477c3aff38a492400aa1`..`eba5bb3155cab51d80af00e8d7d69fa271b1302b`](https://leanprover-community.github.io/mathlib-port-status/file/data/matrix/block?range=3e068ece210655b7b9a9477c3aff38a492400aa1..eba5bb3155cab51d80af00e8d7d69fa271b1302b) commit 087f9d6972c81b5408207f9ffcbe2b0a0a8c9703 Author: Yaël Dillies Date: Tue Apr 25 08:05:48 2023 +0000 chore: Generalise `ess_sup` lemmas (#3590) Match https://github.com/leanprover-community/mathlib/pull/18669 * [`order.filter.ennreal`@`57ac39bd365c2f80589a700f9fbb664d3a1a30c2`..`52932b3a083d4142e78a15dc928084a22fea9ba0`](https://leanprover-community.github.io/mathlib-port-status/file/order/filter/ennreal?range=57ac39bd365c2f80589a700f9fbb664d3a1a30c2..52932b3a083d4142e78a15dc928084a22fea9ba0) * [`topology.algebra.order.liminf_limsup`@`98e83c3d541c77cdb7da20d79611a780ff8e7d90`..`52932b3a083d4142e78a15dc928084a22fea9ba0`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/order/liminf_limsup?range=98e83c3d541c77cdb7da20d79611a780ff8e7d90..52932b3a083d4142e78a15dc928084a22fea9ba0) commit 86a996908e91759c8c7f5c26510ef5d58876cfae Author: Moritz Firsching Date: Tue Apr 25 06:14:50 2023 +0000 feat: port CategoryTheory.Limits.Shapes.WideEqualizers (#2713) Co-authored-by: Moritz Firsching Co-authored-by: qawbecrdtey Co-authored-by: Joël Riou commit 1698ce9c98ba53760f9752bfd7fdde8472129861 Author: Moritz Firsching Date: Tue Apr 25 06:01:15 2023 +0000 feat: port CategoryTheory.Subobject.Comma (#3502) Co-authored-by: Moritz Firsching Co-authored-by: Joël Riou commit 3f353472f4995ad05c18f66337daca84c95d065c Author: Gabriel Ebner Date: Mon Apr 24 23:44:09 2023 +0000 fix: enable ↦ in server mode (#3556) Apparently we didn't enable the `pp.unicode.fun` in server mode, so you got inconsistent output depending on whether you run the lean file on the command-line (↦) or in the editor (=>). This change makes the options uniform. commit 3d1825d795fa02dc0181f06187ac39667b644423 Author: Jeremy Tan Jie Rui Date: Mon Apr 24 22:52:33 2023 +0000 feat: port Analysis.Convex.Normed (#3626) Co-authored-by: Moritz Doll Co-authored-by: Parcly Taxel Co-authored-by: Scott Morrison commit f65546c6b4ce38b33cdfb5e3076ed756c84db572 Author: Joël Riou Date: Mon Apr 24 22:52:32 2023 +0000 feat: port CategoryTheory.Generator (#3623) commit 063039717bef223ca0d969212057ed2caeb990e1 Author: Joël Riou Date: Mon Apr 24 22:52:31 2023 +0000 feat: port CategoryTheory.Abelian.Opposite (#3595) commit 30734d580ee9f201cc9102185f2f1473333731a0 Author: Yury G. Kudryashov Date: Mon Apr 24 22:52:30 2023 +0000 feat: port Data.Real.Hyperreal (#3586) commit 805d78d86817ea0f0bf3ca02b48145c2f3b2f7d4 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon Apr 24 22:04:18 2023 +0000 chore: tidy various files (#3629) commit ed85ae5b679ae044a28ce9f0eee826680fa0d66a Author: Jeremy Tan Jie Rui Date: Mon Apr 24 21:46:25 2023 +0000 feat: port Analysis.Convex.Jensen (#3622) Co-authored-by: Moritz Doll Co-authored-by: Parcly Taxel Co-authored-by: Scott Morrison commit 678c6528ef2fdc68d9d28f7cfa80df65dceb1b12 Author: Moritz Doll Date: Mon Apr 24 21:32:33 2023 +0000 feat: port Analysis.Convex.Topology (#3624) commit d9cadaee19feebfe114484b20f7dcafeaef258ed Author: Kyle Miller Date: Mon Apr 24 15:51:54 2023 +0000 fix: make `apply_fun` instantiate metavariables when analyzing expression (#3621) `apply_fun` would erroneously raise an error when the goal is a metavariable, rather than instantiating it. Now it instantiates it and puts the goal into weak head normal form with reducible transparancy. commit a12d3c1b3d0adadd0cee840d766242b72d567012 Author: Joël Riou Date: Mon Apr 24 14:36:15 2023 +0000 feat: port CategoryTheory.Linear.Yoneda (#3619) commit 454028add2ec17e7ca5b1ec78d55eacd354f3cf8 Author: Jason Yuen Date: Mon Apr 24 14:36:14 2023 +0000 feat: port Analysis.Convex.Combination (#3598) Co-authored-by: Moritz Doll Co-authored-by: Parcly Taxel commit 7c5abc4dfb8403613f3c1de35211f9faf8a570d4 Author: EmilieUthaiwat Date: Mon Apr 24 14:36:13 2023 +0000 feat: port LinearAlgebra.Vandermonde (#3596) Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com> Co-authored-by: ChrisHughes24 commit 66b8f0b73c00a303ccd36c5cfa6a8cadeddcade2 Author: Scott Morrison Date: Mon Apr 24 13:28:37 2023 +0000 chore: port missing instance priorities (#3613) See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathport.20drops.20priorities.20in.20.60attribute.20.5Binstance.5D.60. `mathport` has been dropping the priorities on instances when using the `attribute` command. This PR adds back all the priorities, except for `local attribute`, and instances involving coercions, which I didn't want to mess with. Co-authored-by: Scott Morrison commit 0e3f8427e720ec2ce8424302063af58b7eb3766f Author: Yury G. Kudryashov Date: Mon Apr 24 12:12:13 2023 +0000 feat: port Algebra.Homology.ShortExact.Preadditive (#3611) commit 8ead87d664a52a37014bb0ec158b31eee33ee9ca Author: Jason Yuen Date: Mon Apr 24 11:35:23 2023 +0000 feat: port Topology.ExtremallyDisconnected (#3616) commit 7e39eeaec4ab7cbbf2f254325d841bf97fbe1ed3 Author: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> Date: Mon Apr 24 11:35:22 2023 +0000 chore: forward-port leanprover-community/mathlib#18856 (#3609) Forward-ports https://github.com/leanprover-community/mathlib/pull/18856 and https://github.com/leanprover-community/mathlib/pull/18858 commit 450fc21ed78e4da4ca54b8314783809da9b6c04b Author: Joël Riou Date: Mon Apr 24 11:35:20 2023 +0000 feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence (#3594) commit a5532440329b4c22cda05f6cafd35a84e0b4c2b1 Author: Floris van Doorn Date: Mon Apr 24 11:35:19 2023 +0000 chore: forward-port leanprover-community/mathlib#18601 (#3579) * leanprover-community/mathlib#18601 * https://leanprover-community.github.io/mathlib-port-status/file/topology/fiber_bundle/basic commit 11325e7f8a071792064e3146c85abe2086ddbbee Author: Yaël Dillies Date: Mon Apr 24 11:35:18 2023 +0000 feat: Order on the localization (#3567) Match https://github.com/leanprover-community/mathlib/pull/18724 and https://github.com/leanprover-community/mathlib/pull/18846 Co-authored-by: Eric Wieser commit fe76a1b5ad8929c3d3a97bcf0421e69c9466c75c Author: Yaël Dillies Date: Mon Apr 24 08:51:27 2023 +0000 feat: `insert` and `erase` lemmas (#3569) Match https://github.com/leanprover-community/mathlib/pull/18729 * [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4) * [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4) * [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4) * [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4) commit 314d4ecee7615a27389893d86816345e684d7ed3 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon Apr 24 05:58:32 2023 +0000 chore: tidy various files (#3606) commit efa52c792997cb10d30133daa332e2dfcf9a4e4a Author: Joël Riou Date: Mon Apr 24 05:58:31 2023 +0000 feat: port CategoryTheory.Preadditive.Yoneda.Basic (#3603) commit a6f6a95c3c9c2843f600793eb83858e92b0477d2 Author: Joël Riou Date: Mon Apr 24 05:58:30 2023 +0000 feat: port Algebra.Homology.HomotopyCategory (#3602) commit 77d4aecacaf82a7d6d015517739d8908a57ebce6 Author: Joël Riou Date: Mon Apr 24 05:58:29 2023 +0000 feat: port AlgebraicTopology.DoldKan.Normalized (#3591) commit 570f11aa11b416330e9366595cbf5099ad30b932 Author: Joël Riou Date: Mon Apr 24 05:58:28 2023 +0000 feat: port AlgebraicTopology.DoldKan.EquivalenceAdditive (#3581) Co-authored-by: Scott Morrison Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> commit 5284992d04f921776ddc70f497d694e1f2a8cdf0 Author: ymonbru <109665681+ymonbru@users.noreply.github.com> Date: Mon Apr 24 05:58:26 2023 +0000 feat: port LinearAlgebra.Matrix.Circulant (#3465) Co-authored-by: Jason Yuen Co-authored-by: int-y1 commit d7503071e60b39ee92b55c005674e2f4af2bb6ac Author: Christopher Hoskin Date: Mon Apr 24 04:16:29 2023 +0000 feat: forward-port leanprover-community/mathlib#18517 (#2543) Matches https://github.com/leanprover-community/mathlib/pull/18517 This result is required in #2508. Co-authored-by: Yaël Dillies Co-authored-by: Eric Wieser commit 6b5086bff56be12ca2fc6e1a9ebfce6b5c3425a3 Author: Bulhwi Cha Date: Mon Apr 24 02:11:21 2023 +0000 feat: port Data.String.Defs (#3612) * Add `isSuffixOf`, `isSuffixOf?`, and `getRest` functions. * Add `#align` statements. * Indent function bodies. commit 7a6b2bc3fdc940725a2893daa04709d2b9b2fe77 Author: Yaël Dillies Date: Mon Apr 24 00:27:46 2023 +0000 feat: Miscellaneous defs and lemmas (#3589) Match https://github.com/leanprover-community/mathlib/pull/8289 Co-authored-by: Eric Wieser commit 7c1c4b8039811709acd83f65e46f49c2bcc52da5 Author: Joël Riou Date: Sun Apr 23 17:44:57 2023 +0000 feat: port CategoryTheory.Abelian.Subobject (#3607) commit e71e2ea08de0fd1079f85d3e0d62b6119d09a4dc Author: Joël Riou Date: Sun Apr 23 17:29:09 2023 +0000 feat: port CategoryTheory.ConcreteCategory.UnbundledHom (#3608) commit e24dbaf368bfb6c69c2129457cea9a44288de23a Author: Eric Wieser Date: Sun Apr 23 17:08:25 2023 +0000 chore: forward-port leanprover-community/mathlib#18616 (#3574) commit 30308d5fcd33a70aa0e74971415f7bf355d25821 Author: Kevin Buzzard Date: Sun Apr 23 09:27:40 2023 +0000 feat: port CategoryTheory.Limits.Preserves.FunctorCategory (#3599) Straightforward. commit b8740cb3dcc78ffc220364758b968ffb415b6ba9 Author: Jason Yuen Date: Sun Apr 23 09:27:39 2023 +0000 feat: port LinearAlgebra.Matrix.AbsoluteValue (#3597) commit 17d77d83638a4f50d842cc24683f42a586d0ad25 Author: Yaël Dillies Date: Sun Apr 23 09:27:38 2023 +0000 feat: `Function.update` is monotone (#3587) Match leanprover-community/mathlib#6418 and leanprover-community/mathlib#18841 * [`order.basic`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/basic?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`order.monotone.basic`@`ac5a7cec422c3909db52e13dde2e729657d19b0e`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/monotone/basic?range=ac5a7cec422c3909db52e13dde2e729657d19b0e..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`algebra.group.pi`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..90df25ded755a2cf9651ea850d1abe429b1e4eb1) commit 76330b1be012f801568485b086afec2934b232b6 Author: Eric Wieser Date: Sun Apr 23 09:27:37 2023 +0000 chore: forward-port leanprover-community/mathlib#18835 (#3573) commit 8711ff7cc74e96395e24e8a53c61c39b9c83b8be Author: Eric Wieser Date: Sun Apr 23 07:33:31 2023 +0000 chore: forward-port leanprover-community/mathlib#18831 (#3572) commit c0b4d07b8fa474f2159ed804934ec2224a3278f1 Author: Kyle Miller Date: Sat Apr 22 23:19:19 2023 +0000 feat: use more function coercions in `apply_fun` (#3582) When `apply_fun f` is applied to the main goal, it creates the expression `Function.Injective f`, which requires that `f` be a function. Now `apply_fun` will insert a function coercion here if needed. Furthermore, `apply_fun` is now aware of `Equiv.injective`. commit b0ba06622ec05c4734a96f6ac1970ed0e8002abb Author: Joël Riou Date: Sat Apr 22 23:19:17 2023 +0000 feat: port AlgebraicTopology.DoldKan.NCompGamma (#3576) Co-authored-by: Scott Morrison commit eb5a96a8446ab7fac3557d1ca8d7637e7afd2ab8 Author: Moritz Firsching Date: Sat Apr 22 23:05:58 2023 +0000 feat: port CategoryTheory.Limits.Presheaf (#3208) Co-authored-by: Kevin Buzzard Co-authored-by: Joël Riou Co-authored-by: Adam Topaz Co-authored-by: Newell Jensen Co-authored-by: Scott Morrison Co-authored-by: Gabriel Ebner Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Patrick Massot Co-authored-by: Wrenna Robson Co-authored-by: Sebastian Ullrich Co-authored-by: Floris van Doorn Co-authored-by: Henrik Böving Co-authored-by: Pol_tta commit aff8f34cbb0c0c2b42f3c7458d340968e826a820 Author: Kevin Buzzard Date: Sat Apr 22 18:50:07 2023 +0000 feat : add ext lemma for `Type u` (#3593) This lemma, which was not needed in mathlib3, simplifies several proofs (back to the state they were in in mathlib3). Note on what's going on here: Lean 3 `ext` would fall back on "try all ext lemmas" if it failed, and thus it could see through lots of definitional equalities. Lean 4 `ext` doesn't do this (because it's inefficient) and so we need to add more `ext` lemmas in order to recover Lean 3 functionality. commit d4fbb04aedbaa2708a162acdfdc1e69fc8c3affb Author: Joël Riou Date: Sat Apr 22 16:39:40 2023 +0000 feat: port AlgebraicTopology.DoldKan.GammaCompN (#3568) Co-authored-by: Scott Morrison commit f9886d5057ea21303134262d2a770d9e25b4fbd0 Author: Jeremy Tan Jie Rui Date: Sat Apr 22 09:23:40 2023 +0000 feat: port LinearAlgebra.AffineSpace.Basis (#3578) Co-authored-by: Scott Morrison commit 4ebeb081f256332e4a8fe720e4f901c94f66b7b9 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat Apr 22 02:22:20 2023 +0000 chore: tidy various files (#3584) commit 77bd7966d4339cc48d681f2c04ddf32031cbb359 Author: Pol_tta Date: Sat Apr 22 02:22:19 2023 +0000 fix: Fix `Polynomial.repr` (#3442) I misunderstood the `Repr` instance when I port this file, In Lean 4, `Repr` returns `Format`, not `String`, so my porting of `Polynomial.repr` was unnatural. Co-authored-by: Eric Wieser Co-authored-by: Johan Commelin Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com> commit 43d4e83f7526d0091e2b2e71c5bd148c8ef10763 Author: Gabriel Ebner Date: Sat Apr 22 02:08:54 2023 +0000 fix: computable `KleeneAlgebra (Language α)` instance (#3585) This is another case of https://github.com/leanprover/lean4/issues/2096 commit 076a825029f6748e4300be47ae16b5e9847bcaf7 Author: Joël Riou Date: Sat Apr 22 01:34:23 2023 +0000 feat: port AlgebraicTopology.DoldKan.FunctorGamma (#3566) commit 550081fe6717985dfbc1295f04fd9ec6fc45668f Author: Henrik Böving Date: Fri Apr 21 23:10:49 2023 +0000 feat: move doc-gen CI here (#3520) Creates a Github Action which runs doc-gen4 from within the mathlib4. This is done due to the speed issues of the original doc-gen4 CI as suggested on Zulip. While I ran these scripts locally it might very well be that I made some mistake that will mess this up in CI. Furthermore someone with privileges needs to configure a secret `MATHLIB4_DOCS_KEY` with an ed25519 SSH key that has push access to `leanprover-community/mathlib4_docs` in order for the script to upload the generated docs. Co-authored-by: Gabriel Ebner commit 6f90956496e78a3381b7a0b71f882b440c343c9c Author: Floris van Doorn Date: Fri Apr 21 19:24:26 2023 +0000 perf: dsimp only to mitigate to_additive slowness (#3580) * `to_additive` is slow on this file. I'll try to improve performance in `to_additive`, but this behavior is exposed by working with gigantic proof terms. * The `dsimp only` in `Submonoid.LocalizationMap.lift` changes `to_additive` time from ~27s to ~7s (still needs improving, but this puts a band-aid on it). commit a7dab0198f87330574330d00a5060eebe5cdba85 Author: Patrick Massot Date: Fri Apr 21 15:12:32 2023 +0000 chore: Algebra.RingQuot cleanup (#3577) Those changes were meant to be part of #3383 that got prematurely merged after some abusive relabeling. commit c6d7e631d660824b6802f06d20d1a37da8b633d7 Author: Sebastian Ullrich Date: Fri Apr 21 15:12:31 2023 +0000 fix: sync file list expected by cache with Lake changes (#3571) The `.c.trace` files no longer exist, see https://github.com/leanprover/lake/commit/6499494befc24e388d12f3d9411f99aae0769491#diff-43ead6410f2dcb31276401eb765b8ada18c8e288626dfa8d6123cfab46961e7aL81-L83. commit ba4db649ae1ccd8cff3d426d730c2438ac31cd48 Author: Wrenna Robson Date: Fri Apr 21 15:12:29 2023 +0000 feat: port Data.Polynomial.Module (#3407) Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: EmilieUthaiwat Co-authored-by: Eric Wieser Co-authored-by: Yaël Dillies Co-authored-by: Jireh Loreaux Co-authored-by: Gabriel Ebner Co-authored-by: Violeta Hernández Co-authored-by: Wrenna Robson Co-authored-by: int-y1 Co-authored-by: Scott Morrison Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com> Co-authored-by: Parcly Taxel commit 587de04b95d10fce9a9a97ff3b68b32b0a156fd7 Author: Joël Riou Date: Fri Apr 21 12:33:33 2023 +0000 feat: port AlgebraicTopology.DoldKan.SplitSimplicialObject (#3563) commit b87d5f529120f719a76d892367cffdffc8bf6345 Author: Jeremy Tan Jie Rui Date: Fri Apr 21 10:29:37 2023 +0000 feat: port RingTheory.MvPolynomial.Ideal (#3565) commit c89b9a7e4d5a043471d52bb800a25af70ff699e8 Author: Jeremy Tan Jie Rui Date: Fri Apr 21 08:03:17 2023 +0000 feat: port LinearAlgebra.Matrix.Nondegenerate (#3564) commit 3270b09a2b026779ace9911e0c3072a7e44637ad Author: Jeremy Tan Jie Rui Date: Fri Apr 21 08:03:16 2023 +0000 feat: port CategoryTheory.Adjunction.Over (#3562) commit 3fa2b5d919676782412aae1862c9f522e49b7f8f Author: Joël Riou Date: Fri Apr 21 08:03:15 2023 +0000 feat: port AlgebraicTopology.DoldKan.Degeneracies (#3561) commit fa2c19aa05154199cc196298afd8c5b7a11a5575 Author: Joël Riou Date: Fri Apr 21 08:03:14 2023 +0000 feat: port AlgebraicTopology.DoldKan.NReflectsIso (#3548) Co-authored-by: Parcly Taxel Co-authored-by: Jeremy Tan Jie Rui commit dea12fa72d713ebf925a16e5c3ffafebae121e11 Author: Patrick Massot Date: Fri Apr 21 08:03:11 2023 +0000 feat: port Algebra.RingQuot (#3383) commit 6804222e880492a0f99da50e23c0311c63db7eb4 Author: Jeremy Tan Jie Rui Date: Fri Apr 21 08:03:10 2023 +0000 feat: port LinearAlgebra.AffineSpace.Independent (#3341) Co-authored-by: Moritz Firsching Co-authored-by: Scott Morrison commit 6001e1f50d1607085739734ab9eb7e94b5773fb9 Author: Gabriel Ebner Date: Fri Apr 21 05:17:59 2023 +0000 chore: bump to nightly-2023-04-20 (#3557) commit aca946a68859aad5b7e93d1ce8dd1caac5d7704e Author: Joël Riou Date: Fri Apr 21 04:55:31 2023 +0000 feat: port AlgebraicTopology.DoldKan.Decomposition (#3544) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel commit 28a81909ae60c481b5cde5bcbe72d65139145275 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 21 04:27:55 2023 +0000 feat: port LinearAlgebra.Matrix.Adjugate (#3554) Co-authored-by: Jeremy Tan Jie Rui commit 236ddd964bd623058389c3607b4735e6a983ffb6 Author: Gabriel Ebner Date: Fri Apr 21 04:11:45 2023 +0000 feat: make `ListM` safe (#3559) Hide the unsafe inductive powering `ListM` behind a safe API using `implemented_by`. commit dfa5b6bd178c1eab7f229878cc7b1bcddf0d5961 Author: Scott Morrison Date: Fri Apr 21 02:11:58 2023 +0000 chore: simplify how solve_by_elim works when not backtracking (#3480) We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See https://github.com/leanprover-community/mathlib4/pull/856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code... Since https://github.com/leanprover-community/mathlib4/pull/2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that. Co-authored-by: Scott Morrison commit eb3e8fd0738a1b1d7db4e29b1f4841003b8d4874 Author: Newell Jensen Date: Fri Apr 21 02:11:57 2023 +0000 feat: port Algebra.MonoidAlgebra.Ideal (#3106) Co-authored-by: Eric Wieser commit 4b3f0cb7e85d927f12009b5ab788334100240e75 Author: Adam Topaz Date: Thu Apr 20 18:32:12 2023 +0000 feat: Port CategoryTheory.Monad.Limits (#3533) Co-authored-by: Jeremy Tan Jie Rui commit d9655dd4021e3908e851bcca151649959a61ee60 Author: Joël Riou Date: Thu Apr 20 17:57:47 2023 +0000 feat: port AlgebraicTopology.DoldKan.FunctorN (#3543) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel commit 2d45cec80dcd8c5e2ab352dcb52c5440b4061adf Author: Joël Riou Date: Thu Apr 20 17:11:32 2023 +0000 feat: port AlgebraicTopology.DoldKan.PInfty (#3539) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel commit f40690090a0fd9d6450beef92f6cb76dcc8090c8 Author: Jeremy Tan Jie Rui Date: Thu Apr 20 16:23:08 2023 +0000 feat: port CategoryTheory.Monad.Products (#3553) commit 92898d0812f46b4ece48b7a3ec384c340e703ccb Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu Apr 20 15:58:07 2023 +0000 feat: port LinearAlgebra.Matrix.Polynomial (#3550) commit 18c80e6dd9c2f3ea54c5a4f59aaa705d89b60a4a Author: Moritz Firsching Date: Thu Apr 20 15:36:22 2023 +0000 feat: port Data.Matrix.Reflection (#3551) Co-authored-by: Moritz Firsching commit b30970d7577f15ac48553a5e4e4cd45bbab2877a Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu Apr 20 15:22:30 2023 +0000 feat: port LinearAlgebra.Matrix.Reindex (#3549) commit 7538b6f055dd1526d41ae48efd6578723f13d918 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu Apr 20 15:22:29 2023 +0000 feat: port LinearAlgebra.Matrix.MvPolynomial (#3547) commit fe54b923eaddc77882fa3dc0bf532d59e0038d58 Author: Adam Topaz Date: Thu Apr 20 15:22:27 2023 +0000 feat: Port CategoryTheory.Monad.Adjunction (#3528) ~~This is still WIP.~~ There may be a change to `reassoc` that would make this nicer, see [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20reassoc.3F/near/351111877) commit 413f4895f1dc1770703029aef577e4c89b996ba6 Author: Joël Riou Date: Thu Apr 20 12:31:24 2023 +0000 feat: port AlgebraicTopology.DoldKan.Projections (#3536) Co-authored-by: Jeremy Tan Jie Rui commit 27af7fb1003519d63606198c05ce3e961e0ccb3b Author: Jeremy Tan Jie Rui Date: Thu Apr 20 12:31:22 2023 +0000 feat: port Data.MvPolynomial.Funext (#3225) Co-authored-by: Scott Morrison Co-authored-by: Johan Commelin commit f4af9a661988ecdfa980d0188ce011f25de3f3ad Author: Chris Hughes Date: Thu Apr 20 12:31:21 2023 +0000 feat: port RingTheory.ChainOfDivisors (#3056) Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> commit a87ba08aa1090fe901c409779388c1c6ddbfae62 Author: Jeremy Tan Jie Rui Date: Thu Apr 20 11:28:09 2023 +0000 chore: forward port leanprover-community/mathlib#18442 (#3545) * leanprover-community/mathlib#18442 commit 26db6cbbb260959e5d08ddc266a051ebce93f88e Author: Moritz Doll Date: Thu Apr 20 11:28:07 2023 +0000 feat: inverse of LinearPMap (#3527) commit 833f6762e34b203bb83cf086a7be08838e5f8abe Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Date: Thu Apr 20 11:28:06 2023 +0000 feat: port LinearAlgebra.FreeModule.PID (#3434) Co-authored-by: Jeremy Tan Jie Rui commit 44db8ff57080e84cc98239510c3c3b229324f8ce Author: Jeremy Tan Jie Rui Date: Thu Apr 20 10:27:47 2023 +0000 feat: port CategoryTheory.Preadditive.EilenbergMoore (#3546) commit 6812cb785f8e093c170911ada24aba6a775e9a49 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu Apr 20 10:27:46 2023 +0000 feat: port LinearAlgebra.Matrix.Determinant (#3540) commit a832353e64a320427a7956dc50bf361472b60865 Author: Joël Riou Date: Thu Apr 20 10:27:45 2023 +0000 feat: port AlgebraicTopology.DoldKan.Faces (#3526) Co-authored-by: Joël Riou commit d4f0d73937fb5b0ef3c5bfa7abfd17684a8c4e20 Author: Pol_tta Date: Thu Apr 20 10:27:43 2023 +0000 feat: port Data.Seq.Parallel (#3512) This PR also make `Prod.rec` computable. Co-authored-by: Jeremy Tan Jie Rui commit 3854f4f7230329d6a622d02cef5253ce8c001108 Author: Scott Morrison Date: Thu Apr 20 08:29:25 2023 +0000 chore: add .DS_Store to .gitignore (#3538) mac users should have this in their `.gitignore` file, but sometimes don't, as evidenced by https://github.com/leanprover-community/mathlib4/pull/3511, which then unfortunately broke the port-status bot for a day! Co-authored-by: Scott Morrison commit 20313ef1054da9ce7a99dcb1e7bd92281661f758 Author: Moritz Firsching Date: Thu Apr 20 08:29:24 2023 +0000 chore: remove `clear` (#3537) Those used to be necessary because of a linarith bug, which was fixed in #2611 Co-authored-by: Moritz Firsching commit 201b154390aab392d0a6eb55ed75cb41d0ce3d09 Author: Scott Morrison Date: Thu Apr 20 08:29:23 2023 +0000 feat: improve propose documentation (#3534) Per suggestion on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20.60propose.60.20tactic/near/350961701). Co-authored-by: Scott Morrison commit 34dd882765c3ca0e411ff76679fc83c950f016ea Author: Scott Morrison Date: Thu Apr 20 08:29:21 2023 +0000 feat: port observe tactic from mathlib (#3516) Co-authored-by: Scott Morrison Co-authored-by: Jeremy Tan Jie Rui commit a4686637d10ec7832d66111d87edeeac6099a815 Author: Scott Morrison Date: Thu Apr 20 08:29:20 2023 +0000 chore: have linarith print the goal when it fails (#3273) This makes `linarith` print the goal (including hypotheses) when it fails, as many other tactics do. This was motivated by watching the `sagredo` tactic trying to use `linarith`, but failing to see that it didn't quite have the correct hypotheses yet. Once it gave up on using `linarith`, it tried `contradiction`, which printed a more helpful error message (in which a human, although not quite GPT, could easily see the inequalities weren't quite right). Co-authored-by: Scott Morrison commit ed627e8603f3ccb59eb4aece43de87e37f93cf4d Author: Scott Morrison Date: Thu Apr 20 08:29:09 2023 +0000 chore: fix simps projections in CategoryTheory.Monad.Basic (#3269) This fixes a regression of `@[simps]` to `@[simp]` from #2969, per [zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.232969.20simps.20bug.3F.20.28Monad.2EBasic.29). There are a few incidental changes to `@[simps]` arguments in this PR, just removing arguments that had no effect on behaviour. Co-authored-by: Scott Morrison commit d5d16c038c0080e6488089645a487e95a4a45249 Author: Felix-Weilacher Date: Thu Apr 20 06:30:56 2023 +0000 chore: forward port last part of leanprover-community/mathlib#18248 (#3508) Co-authored-by: Parcly Taxel commit 5ee711f39e34f8782e81951f10db55cd0f234aa5 Author: Pol_tta Date: Thu Apr 20 06:30:55 2023 +0000 feat: port Data.Seq.WSeq (#3405) This PR also make `Option.recOn` computable. Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com> Co-authored-by: Scott Morrison commit db4a999d849402ce88a108adac33742b4cf34396 Author: Chris Hughes Date: Thu Apr 20 06:30:54 2023 +0000 chore: use FunLike.coe as coercion for OrderIso and RelEmbedding (#3082) The changes I made were. Use `FunLike.coe` instead of the previous definition for the coercion from `RelEmbedding` To functions and `OrderIso` to functions. The previous definition was ```lean instance : CoeFun (r ↪r s) fun _ => α → β := -- ⟨fun o => o.toEmbedding⟩ ``` This does not display nicely. I also restored the `simp` attributes on a few lemmas that had their `simp` attributes removed during the port. Eventually we might want a `RelEmbeddingLike` class, but this PR does not implement that. I also added a few lemmas that proved that coercions to function commute with `RelEmbedding.toRelHom` or similar. The other changes are just fixing the build. One strange issue is that the lemma `Finset.mapEmbedding_apply` seems to be harder to use, it has to be used with `rw` instead of `simp` Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> commit 27bf8bae46d4ac40bbcfafadf700674d9e44e6ca Author: Jeremy Tan Jie Rui Date: Thu Apr 20 04:08:33 2023 +0000 feat: port CategoryTheory.Idempotents.HomologicalComplex (#3532) commit 073b188149a66b0bbdbc46449e4030d400904186 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu Apr 20 04:08:32 2023 +0000 chore: tidy various files (#3530) commit 71e37247e36e17198c36088d30c9175ae72711c4 Author: Joël Riou Date: Thu Apr 20 04:08:31 2023 +0000 feat: port AlgebraicTopology.DoldKan.Homotopies (#3523) Co-authored-by: Joël Riou Co-authored-by: Scott Morrison commit bb86afcd387da48147b83de92bdcab05b791d7bd Author: Eric Wieser Date: Thu Apr 20 04:08:29 2023 +0000 feat: port Data.Matrix.Notation (#3427) This PR also fixes the doc on `Data.Fin.VecNotation` and adds the unexpander for the `![x, y, ...]` notation. Co-authored-by: Komyyy Co-authored-by: Kyle Miller Co-authored-by: Jeremy Tan Jie Rui commit 44cd35fe4d05301a3efb0f0c09ef41f473a6dc38 Author: Mario Carneiro Date: Thu Apr 20 04:08:28 2023 +0000 fix: discard linarith wrong type equalities, style (#2611) Mostly style fixes in linarith, but also fixes #2610 Co-authored-by: Scott Morrison Co-authored-by: Alex J Best commit 514388b547c2a082763ad5a0feabe6913b24dacd Author: Shrys Date: Thu Apr 20 04:08:26 2023 +0000 feat: port Data.Bitvec.Basic (#2179) Co-authored-by: casavaca <96765450+casavaca@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> commit e85a5e5404e682e30fb6c2d00245eccb9b7d5a06 Author: Adam Topaz Date: Thu Apr 20 03:35:24 2023 +0000 chore: Upgrade `reassoc`'s simplification skills (#3531) See [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20reassoc.3F/near/351111877) The only lemmas added to `reassoc`'s simplification set are: ```lean Functor.id_obj, Functor.id_map, Functor.comp_obj, Functor.comp_map ``` all of which are definitional equalities. commit 5bbb6b42c5e53067e5ec86f7bf7b869895836c0c Author: Yury G. Kudryashov Date: Thu Apr 20 03:04:51 2023 +0000 feat: port Topology.MetricSpace.Polish (#3357) Co-authored-by: Scott Morrison commit e933e1932787daad246e79f8b3c7c0a18c5581b4 Author: Moritz Doll Date: Thu Apr 20 01:28:06 2023 +0000 feat: more algebra for LinearPMap (#3521) commit ce035cf77446126f2c836b2d07aa8ee03ed339a0 Author: Eric Wieser Date: Wed Apr 19 23:15:39 2023 +0000 chore: port `fin.reflect` (#3486) This definition was deleted during porting. Co-authored-by: Gabriel Ebner commit 1d38f4511c299223598419422a2f109cb5a6082d Author: Gabriel Ebner Date: Wed Apr 19 22:55:05 2023 +0000 chore: bump std4 (#3529) commit 097302efc66fc63f6ac7a023e09c4dec477d05ac Author: Joël Riou Date: Wed Apr 19 22:29:07 2023 +0000 feat: port Algebra.Homology.Homotopy (#3524) Co-authored-by: ChrisHughes24 Co-authored-by: Parcly Taxel Co-authored-by: Jeremy Tan Jie Rui commit c7f90468167a1af73902299f3098937132712063 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed Apr 19 21:22:35 2023 +0000 chore: avoid RBTree.ofList in Cache (#3507) Unlike fromList, ofList is not tail recursive and hence susceptible to stack overflow. commit 0550be048e5d8caa099ab9664dcdd7ce4e9b2b11 Author: Joël Riou Date: Wed Apr 19 15:37:15 2023 +0000 feat: port AlgebraicTopology.DoldKan.Notations (#3522) Co-authored-by: Joël Riou commit 2e9a3bfe62d8b73a361c06ac5c1ad1c1acf22992 Author: Adam Topaz Date: Wed Apr 19 15:24:18 2023 +0000 Feat: Port CategoryTheory.Monad.Algebra (#3525) Co-authored-by: ChrisHughes24 commit c980e9e53d9605712cff5455d00faa959274eea5 Author: Joël Riou Date: Wed Apr 19 14:33:30 2023 +0000 feat: port AlgebraicTopology.AlternatingFaceMapComplex (#3519) Co-authored-by: Joël Riou commit 3c2d274deb00582af4f6caa0058bf6559fac65c9 Author: Joël Riou Date: Wed Apr 19 13:55:34 2023 +0000 feat: port Algebra.Homology.Additive (#3517) Co-authored-by: Joël Riou commit 8784a44451981f44623879c9b02d97f62da1bd63 Author: Joël Riou Date: Wed Apr 19 11:37:18 2023 +0000 feat: port CategoryTheory.Preadditive.Opposite (#3505) Co-authored-by: Joël Riou commit 9e71b14eb4d2a5e3074c0df8614ec8585e50d29f Author: Jannis Limperg Date: Wed Apr 19 11:37:17 2023 +0000 chore: bump Aesop to 2023-04-18 version (#3501) commit 542e28123d76e3231fb2a8735c895ea0a50ad2ba Author: Joël Riou Date: Wed Apr 19 11:37:16 2023 +0000 feat: port AlgebraicTopology.CechNerve (#3500) commit f951c54862fe12782745524b044e0321db315c32 Author: Kevin Buzzard Date: Wed Apr 19 11:37:14 2023 +0000 feat: port/CategoryTheory.Sites.Limits (#3463) Co-authored-by: Joël Riou Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: adamtopaz commit 27fcfe343c680c065de1c5d714fa110441b8eb11 Author: Jeremy Tan Jie Rui Date: Wed Apr 19 11:19:14 2023 +0000 feat: port Algebra.Category.ModuleCat.Products (#3515) commit 6deb39988c5fe28f6766a4ffddaf9243c72b9a00 Author: David Loeffler Date: Wed Apr 19 11:19:12 2023 +0000 feat: port Analysis.NormedSpace.BallAction (#3513) commit e300a9bad55bdfbf96afdfc8de962631280e1d83 Author: Jeremy Tan Jie Rui Date: Wed Apr 19 11:19:11 2023 +0000 feat: port Data.Complex.Cardinality (#3506) commit 475188aa9efa5be144f64c0491ff81398c390081 Author: David Loeffler Date: Wed Apr 19 11:04:23 2023 +0000 feat: port RingTheory.Localization.Submodule (#3514) Co-authored-by: Jeremy Tan Jie Rui commit d666712828b97ba8c205616f11623306b3039bc3 Author: Jeremy Tan Jie Rui Date: Wed Apr 19 09:11:28 2023 +0000 feat: port Logic.Equiv.TransferInstance (#3206) Co-authored-by: Joël Riou Co-authored-by: Eric Wieser commit 1dcba993d1f5b4e90be8527fc206b5c40e8feb89 Author: Scott Morrison Date: Wed Apr 19 07:15:58 2023 +0000 chore: fix push_neg on > (#3518) Co-authored-by: Scott Morrison commit 4f380d2a1aa5ddf7c3385d9c517112a6ebefb725 Author: Gabriel Ebner Date: Wed Apr 19 00:18:14 2023 +0000 fix: disable unsafe closed term extraction (#3509) The compiler extracts the closed term `Option.get none ◾` here, which causes a segfault in compiled code depending on mathlib, like e.g. mathport. commit a92e265cb6269d93050e55f5f294672354ce5be6 Author: Adam Topaz Date: Tue Apr 18 14:23:57 2023 +0000 feat: Port CategoryTheory.Monad.Types (#3504) Fairly straightforward port. commit cc3bf17c0a4743c863ef323a9ba81dc669174934 Author: Jeremy Tan Jie Rui Date: Tue Apr 18 14:23:56 2023 +0000 feat: port CategoryTheory.Subobject.Types (#3503) commit 8a89070f48a8f7d8d3f2999cd24f9e467d9dcd46 Author: Scott Morrison Date: Tue Apr 18 12:01:57 2023 +0000 feat: `propose`, a forwards-reasoning analogue of `library_search`. (#2898) * `propose using a, b, c` tries to find a lemma which makes use of each of the local hypotheses `a, b, c`, and reports any results via trace messages. * `propose : h using a, b, c` only returns lemmas whose type matches `h` (which may contain `_`). * `propose! using a, b, c` will also call `have` to add results to the local goal state. `propose` should not be left in proofs; it is a search tool, like `library_search`. Co-authored-by: Scott Morrison Co-authored-by: Jeremy Tan Jie Rui commit d17db8bd43293ef1d2651020ac9f2c327377a78e Author: Joël Riou Date: Tue Apr 18 11:49:25 2023 +0000 feat: port Algebra.Homology.Exact (#3468) Co-authored-by: Jeremy Tan Jie Rui commit 8e490bdcf0ea1a52b3dc668c474c5f69f93bb3e3 Author: Jeremy Tan Jie Rui Date: Tue Apr 18 11:36:55 2023 +0000 feat: port Topology.MetricSpace.CantorScheme (#3498) commit f199a16dbe7b62e925c9665fec2b528e2b89b5ba Author: Jeremy Tan Jie Rui Date: Tue Apr 18 11:25:28 2023 +0000 feat: port Algebra.Homology.Functor (#3493) Co-authored-by: Scott Morrison commit 5f47835184a1982b4fe2d2c2fd91d566cbbad563 Author: Scott Morrison Date: Tue Apr 18 11:25:27 2023 +0000 feat: depth first and best first search using ListM (#3221) Implementations of depth first search, best first search, and beam search, for graphs described by a neighbours function `α → ListM m α`. There are also wrappers for using `α → List α`. This is only intended for use in meta code. Co-authored-by: Scott Morrison commit 3c49b6b246592b4edce671f15b9258c4351593d9 Author: Scott Morrison Date: Tue Apr 18 11:25:26 2023 +0000 feat: add 'cache get-' flag that does not decompress (#3179) Perhaps a big obscure for end-users, but useful if you would like to make sure something is in the cache, for later. Co-authored-by: Scott Morrison commit a471f7ce52511e051e63a7883820a3590ae30cb4 Author: Jason Yuen Date: Tue Apr 18 11:12:29 2023 +0000 feat: port Topology.Algebra.Valuation (#3499) commit 59b787831e44c858d6079dc77a6e3e0dfdb0a5c7 Author: Jeremy Tan Jie Rui Date: Tue Apr 18 11:12:28 2023 +0000 chore: forward port leanprover-community/mathlib#18815 and part of leanprover-community/mathlib#18248 (#3496) commit 0eb98cb44ecda7864ad41e17f6affd849088b354 Author: Joël Riou Date: Tue Apr 18 11:12:27 2023 +0000 feat: port Algebra.Homology.Single (#3495) Co-authored-by: Joël Riou commit d37bbe97d72c4bf71780b82ae69b603449f1545f Author: Jason Yuen Date: Tue Apr 18 11:12:26 2023 +0000 feat: port ModelTheory.Encoding (#3494) commit 65c3c0b01697e840a4b7ff88ffbdd3d091623efc Author: Pol_tta Date: Tue Apr 18 11:12:24 2023 +0000 feat: port `apply_congr` (#3471) commit 2cc2e62303ae13b8694d1b72a3aca0049d33ffbe Author: Jeremy Tan Jie Rui Date: Tue Apr 18 10:57:09 2023 +0000 feat: port Algebra.Homology.Flip (#3492) commit c78238fd93e3d41b4e5b27d038abbd7a141d45ba Author: Jason Yuen Date: Tue Apr 18 10:45:15 2023 +0000 feat: port Algebra.Homology.Homology (#3491) Co-authored-by: Joël Riou commit 957ef18d73c28319a0206975eeeaaa78b39a0cbe Author: Jeremy Tan Jie Rui Date: Tue Apr 18 10:45:14 2023 +0000 feat: port Data.Real.Cardinality (#3312) Co-authored-by: ChrisHughes24 commit a3fae7f4b123b793ec785f536f0f18341982aa29 Author: Scott Morrison Date: Tue Apr 18 10:28:57 2023 +0000 chore: refactor of library_search, and don't timeout (#3228) This is a refactor of `library_search`, separating the logic of applying lemmas and flow control (i.e. stopping if we find a good one). This version has an intermediate function that returns a lazy list of candidate results, using the new `ListM` API. As an easy add-on, we make sure `library_search` never times out Co-authored-by: Scott Morrison commit 9506d51827f0df9e9871e92490882da8dd1529db Author: EmilieUthaiwat Date: Tue Apr 18 05:52:59 2023 +0000 feat: port RingTheory.Localization.Ideal (#3452) Co-authored-by: Riccardo Brasca Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> commit d97f3142e27eae9eb176e3c22b702f26b327efa7 Author: Lucas Date: Tue Apr 18 03:37:05 2023 +0000 feat: port Topology.UrysohnsLemma (#3490) Co-authored-by: Lucas V. R Co-authored-by: Jeremy Tan Jie Rui commit f8177799abd67c4d6f0cb1ccae22540948eb052c Author: Moritz Doll Date: Tue Apr 18 03:37:04 2023 +0000 chore: forward port 18648 (#3489) * [`data.finset.lattice`@`1c857a1f6798cb054be942199463c2cf904cb937`..`a968611b6a772cf7bdf61146e6d62fc882c92372`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/lattice?range=1c857a1f6798cb054be942199463c2cf904cb937..a968611b6a772cf7bdf61146e6d62fc882c92372) commit ad2d88eb52001b7d8de9432131f9dfe7d0441344 Author: Kevin Buzzard Date: Tue Apr 18 03:37:03 2023 +0000 doc: add and clarify some docstrings in LinearAlgebra.Dimension (#3488) commit 0f84059fe5c554bef98c357bf358faf5ec9280c5 Author: Jason Yuen Date: Tue Apr 18 03:37:02 2023 +0000 feat: port Data.QPF.Univariate.Basic (#3470) commit 91dbd4557560090b9946f00cd33cc870fe98b936 Author: Jason Yuen Date: Tue Apr 18 03:37:00 2023 +0000 feat: port Control.Bitraversable.Lemmas (#3460) commit 34a4e01aed2236d6c6ac11cd2d9573bb5ef755d4 Author: Moritz Firsching Date: Tue Apr 18 03:36:59 2023 +0000 feat: Int.odd_pow (#3402) analogous to `Int.even_pow` and `Int.even_pow'` Co-authored-by: Moritz Firsching commit 344f06193aaf1ede17f0780811b2a174c4796bbb Author: Kyle Miller Date: Tue Apr 18 03:36:58 2023 +0000 feat: `Fintype` deriving handler (#3198) Adds a handler to derive `Fintype` instances for non-recursive types without indices. Has an optimized implementation for enum types as well where it produces an underlying list (`enumList`) of its elements. For non-enum types, the `Fintype` instance comes from an equivalence to a "proxy type" made from `Sum`, `Sigma`, `PLift`, `Empty`, and `Unit`. Also adds a `derive_fintype%` elaborator to derive `Fintype` instances in the middle of terms. This is useful in case, for example, a `Fintype` instance needs an additional `DecidableEq` instance. This elaborator is defined in terms of a `proxy_equiv%` elaborator that constructs the proxy type and the the equivalence from it. The machinery for `proxy_equiv%` is made to be somewhat configurable. commit 5e627382465ad820cf50e95ceb564ad0cf9257d8 Author: Kyle Miller Date: Tue Apr 18 03:36:57 2023 +0000 feat: `with` clauses for `congr!`/`convert`/`convert_to` (#3060) Adds `with` clauses to `congr!` and friends consisting of a list of `rintro` patterns. These patterns are used when these tactics intro variables. commit eb93259744898f958a2eeaaf9240895b09bf8863 Author: Pol_tta Date: Tue Apr 18 03:36:55 2023 +0000 feat: port Computability.TMComputable (#2800) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: EmilieUthaiwat Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Scott Morrison commit f86b7034a92b65c99f5af4c142aeaed4ac703c30 Author: Joël Riou Date: Tue Apr 18 01:37:27 2023 +0000 chore: made Opposite a structure (#3193) The opposite category is no longer a type synonym, but a structure. Co-authored-by: Scott Morrison Co-authored-by: Parcly Taxel Co-authored-by: Scott Morrison commit 6e721e1b92324df768861c4c01f5ecfbfda1a39f Author: Scott Morrison Date: Mon Apr 17 21:44:06 2023 +0000 chore: bump dependencies (#3475) Co-authored-by: Scott Morrison commit 6140f3dcc33f5f17979d11d7b38afe45e37eabce Author: Joël Riou Date: Mon Apr 17 21:44:04 2023 +0000 feat: port AlgebraicTopology.MooreComplex (#3467) Co-authored-by: Jeremy Tan Jie Rui commit 0b5e38839f35a73645990a65b1f47a2688730c7b Author: Violeta Hernández Date: Mon Apr 17 21:44:02 2023 +0000 golf: `SetTheory/Ordinal/CantorNormalForm` (#3189) We open the `List` namespace and golf `CNF_lt_snd`. Mathlib 3: https://github.com/leanprover-community/mathlib/pull/16009 Co-authored-by: Jeremy Tan Jie Rui commit 59857f760bf11986e84ab5ce3dbccf7fc9ec81ec Author: Joël Riou Date: Mon Apr 17 21:32:26 2023 +0000 feat: port Algebra.Homology.ImageToKernel (#3459) Co-authored-by: Jeremy Tan Jie Rui commit 2679caf9925b67f2464070216c252a9ebba1b334 Author: Eric Wieser Date: Mon Apr 17 19:53:11 2023 +0000 feat: add pretty-printer hints to matrix literals (#3485) commit 80d52a3936d1dd56c9d65525575a80a83f4737e5 Author: Joël Riou Date: Mon Apr 17 19:17:24 2023 +0000 feat: port Algebra.Homology.HomologicalComplex (#3451) Co-authored-by: Jeremy Tan Jie Rui commit 7ae59ef5c4f2b790ef841c2eb0c273ca38892b9d Author: Joël Riou Date: Mon Apr 17 18:22:33 2023 +0000 feat: port CategoryTheory.Subobject.Limits (#3450) Co-authored-by: Jeremy Tan Jie Rui commit 1980e5622e3206c867684a33c1e24e3ec798bb19 Author: Joël Riou Date: Mon Apr 17 17:56:07 2023 +0000 feat: port CategoryTheory.Subobject.Lattice (#3447) Co-authored-by: Jeremy Tan Jie Rui commit ab63c1341d6bcf7ff36dae3a62055dcf79f2165f Author: Joël Riou Date: Mon Apr 17 17:25:05 2023 +0000 feat: port CategoryTheory.Subobject.WellPowered (#3446) Co-authored-by: Jeremy Tan Jie Rui commit 9598bc36448c5a8333f18139bef4e454daca4326 Author: Joël Riou Date: Mon Apr 17 16:37:47 2023 +0000 feat: port CategoryTheory.Subobject.FactorThru (#3445) Co-authored-by: Jeremy Tan Jie Rui commit 84041e3f5c83ace4d402a58085524586d4e88137 Author: Joël Riou Date: Mon Apr 17 15:59:33 2023 +0000 feat: port CategoryTheory.Subobject.Basic (#3444) Co-authored-by: Jeremy Tan Jie Rui commit c650bff06d931673ee1f8ec37c6abb8f0e14685b Author: Chris Hughes Date: Mon Apr 17 15:32:58 2023 +0000 chore: ModelTheory.Syntax: whitespace fix (#3482) The diff is not very helpful, but I made sure the comments about the notation were closer to the notation they were about by removing a newline above and adding one below. commit cbac54c8bc0153002e0945fb44e6958709ea973d Author: Jeremy Tan Jie Rui Date: Mon Apr 17 15:15:49 2023 +0000 feat: port Analysis.NormedSpace.AddTorsor (#3477) commit 616b53aae6c616cad39c63e46be3a33ac644af17 Author: Jason Yuen Date: Mon Apr 17 14:55:00 2023 +0000 feat: port Analysis.SpecialFunctions.Polynomials (#3478) commit 65d20d23f0988eb2f1d22dd9a548ab05d85c404e Author: Jon Eugster Date: Mon Apr 17 14:54:59 2023 +0000 feat: port Topology.Algebra.Nonarchimedean.Bases (#3476) commit 6e51f8f03278225b0372920ad78b215a0be4e406 Author: Jeremy Tan Jie Rui Date: Mon Apr 17 14:43:34 2023 +0000 feat: port Analysis.NormedSpace.Pointwise (#3479) commit f32de66ca9eaf9e1b61e8bc1c4f4c591cf7f143f Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon Apr 17 14:24:14 2023 +0000 chore: tidy various files (#3483) commit 2d65534c00d013ca514fbe6b2b25898dad46a69c Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon Apr 17 12:04:16 2023 +0000 chore: fix names in DiscreteQuotient (#3481) commit 9291f3c0eeb727b5e56acb90aa70fdf5d16602c4 Author: Chris Hughes Date: Mon Apr 17 11:39:40 2023 +0000 feat: port ModelTheory.Syntax (#3195) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel commit 9703376fd9bb8001a1e9d6de7e1bda2094fe309e Author: Chris Hughes Date: Mon Apr 17 11:13:23 2023 +0000 feat: port NumberTheory.PellMatiyasevic (#3083) Co-authored-by: Scott Morrison commit 4ba652c7c70f3538ef834f48cde24ce74e8eae86 Author: Jason Yuen Date: Mon Apr 17 10:44:03 2023 +0000 feat: port Analysis.BoxIntegral.Box.SubboxInduction (#3440) commit ec482f9d205f5190bb32482055293f6cb996bbc6 Author: Yury G. Kudryashov Date: Mon Apr 17 10:44:02 2023 +0000 feat: the product of a compact space and a paracompact space is a paracompact space (#3296) Co-authored-by: Scott Morrison commit cd11a025d54fbfa71e5a4f62ad7beb21116c26e3 Author: Yury G. Kudryashov Date: Mon Apr 17 10:44:01 2023 +0000 feat: use `HomotopyLike` for `HomotopyWith` (#3197) Also fix some `simp`/`simps`. commit e41e2865f6189f1bde9556299bb406327a155950 Author: Yury G. Kudryashov Date: Mon Apr 17 10:43:59 2023 +0000 feat: add constructions about continuous map and homotopies (#2984) * Add `ContinuousMap.fst`, `ContinuousMap.snd`, `ContinuousMap.eval`, and `ContinuousMap.piMap`. * Add `ContinuousMap.Homotopy.prodMk`, `ContinuousMap.Homotopy.prodMap`, `ContinuousMap.Homotopy.pi`, `ContinuousMap.Homotopy.piMap`. * Add `ContinuousMap.Homotopic.prodMk`, `ContinuousMap.Homotopic.prodMap`, `ContinuousMap.Homotopic.pi`, `ContinuousMap.Homotopic.piMap`. * Add `ContinuousMap.HomotopyEquiv.prodCongr` and `ContinuousMap.HomotopyEquiv.piCongrRight`. commit b67a2ea096459c89e12d54e3e50c735a7d2af0b6 Author: Yury G. Kudryashov Date: Mon Apr 17 10:23:59 2023 +0000 chore: golf (#3473) - Golf `TopologicalGroup.toUniformSpace`. - Slightly golf `GroupSeminorm.toSeminormedGroup` commit c82702ee6ce5eb19b3397da4afef522797e0d09c Author: Joël Riou Date: Mon Apr 17 08:52:29 2023 +0000 feat: port CategoryTheory.Sites.Whiskering (#3461) commit 12e26e53ff84391488d3836ffad9c47ab4362ec2 Author: Jeremy Tan Jie Rui Date: Mon Apr 17 08:52:27 2023 +0000 feat: port Order.Category.DistLatCat (#3458) commit 3d7d40132841884b34a1ba9813e4ddee6a146e34 Author: Jeremy Tan Jie Rui Date: Mon Apr 17 08:52:26 2023 +0000 feat: port Analysis.Convex.Exposed (#3453) commit c3f058bada0cd38296dc4b3403538c6be392e4d9 Author: Joël Riou Date: Mon Apr 17 08:52:25 2023 +0000 feat: port AlgebraicTopology.TopologicalSimplex (#3437) Co-authored-by: Jeremy Tan Jie Rui commit 60222a7a7b8e21d234914ba4f27387757e7bd1f5 Author: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Mon Apr 17 08:52:23 2023 +0000 feat: port Analysis.Normed.Ring.Seminorm (#3211) ~~This is currently stuck on an issue as indicated in line 111.~~ edit: fixed by the `etaExperiment` option Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Jason Yuen Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: int-y1 commit cd344cf9b62b26a200ed5d36f09c37645ca5106a Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon Apr 17 07:18:40 2023 +0000 chore: tidy various files (#3474) commit 54662f10d2fbc0ef3783c00bff965a7def5e3e6f Author: Scott Morrison Date: Mon Apr 17 07:18:38 2023 +0000 chore: copy over some nth_rewrite tests from mathlib3 (#3462) There's a somewhat unsatisfactory situation here: when `nth_rewrite` was ported from mathlib3 to mathlib4, its behaviour changed significantly. Now it is "just" a syntax level tactic for accessing the "Occurrences" argument of the underlying rewrite machinery. However in mathlib3 is actually had different behaviour, allowing rewriting in individual locations even when the lemma matched in different ways. (Both Lean 3 and Lean 4 have a stuck metavariables problem in this situation.) This PR restores the tests from mathlib3, with the ones broken because of this regression just commented out, and an explanation added. Hopefully one day we'll fix this up. Co-authored-by: Scott Morrison commit 16367abbc58efab7b0e75751911151faea4c1b5c Author: Jason Yuen Date: Mon Apr 17 07:18:37 2023 +0000 feat: port GroupTheory.FreeAbelianGroupFinsupp (#3441) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Parcly Taxel commit 352d0350ef70197cfa81bcc7a55652b1c9c05228 Author: Yury G. Kudryashov Date: Mon Apr 17 07:01:44 2023 +0000 feat: port Dynamics.Circle.RotationNumber.TranslationNumber (#3433) commit b6de124139e4e315213a90e1a4f5e46050a41ed5 Author: Jason Yuen Date: Mon Apr 17 07:01:43 2023 +0000 feat: port Geometry.Manifold.LocalInvariantProperties (#3401) commit fd557ea4d311c408fe8b7bf5b5965ea273eae3dd Author: ymonbru Date: Mon Apr 17 07:01:42 2023 +0000 feat: port Data.Num.Prime (#3386) Co-authored-by: ymonbru <109665681+ymonbru@users.noreply.github.com> Co-authored-by: int-y1 Co-authored-by: Parcly Taxel commit 33edda5243834d36f29b177b5e94b4cab13b75a4 Author: Moritz Firsching Date: Mon Apr 17 07:01:41 2023 +0000 feat: port Topology.MetricSpace.Closeds (#3338) Co-authored-by: Moritz Firsching Co-authored-by: int-y1 commit 97084735ae07eb9e048eea82a1c0d45ea11767e1 Author: Eric Wieser Date: Mon Apr 17 06:46:11 2023 +0000 chore: forward-port leanprover-community/mathlib#18784 (#3454) commit dc26f0fb6c8284b992316b991fa5e9b2712508f4 Author: Jason Yuen Date: Mon Apr 17 06:46:10 2023 +0000 feat: port Analysis.Asymptotics.AsymptoticEquivalent (#3417) Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: ADedecker commit a71adcfdf40ddd840b9811c6c0a9eee974173bf9 Author: Moritz Firsching Date: Mon Apr 17 06:46:08 2023 +0000 feat: port Topology.MetricSpace.Baire (#3315) Co-authored-by: Moritz Firsching Co-authored-by: int-y1 Co-authored-by: Eric Wieser commit f9f63cc44fc46a7a4cbcc8b6c105f6d190269154 Author: Moritz Doll Date: Mon Apr 17 06:32:39 2023 +0000 feat: port Analysis.Normed.Group.AddTorsor (#3063) Co-authored-by: Scott Morrison Co-authored-by: Parcly Taxel Co-authored-by: Eric Wieser commit e2bc2050c673bbe750340f847c0539b0c959f5d5 Author: Yury G. Kudryashov Date: Sun Apr 16 16:21:33 2023 +0000 feat: port Analysis.Convex.Body (#3431) commit beb8acdc25deb71909975d5c984984f99d833ad6 Author: Jeremy Tan Jie Rui Date: Sun Apr 16 11:41:35 2023 +0000 feat: port LinearAlgebra.FreeModule.Finite.Rank (#3455) Co-authored-by: Parcly Taxel Co-authored-by: Eric Wieser Co-authored-by: Jeremy Tan Jie Rui commit 003158eb3a635a53b12d2cea4b2e18f73e9315f0 Author: Jeremy Tan Jie Rui Date: Sun Apr 16 08:18:09 2023 +0000 chore: forward port leanprover-community/mathlib#18811 (#3456) Co-authored-by: Parcly Taxel commit 552255298ca12332962be185f1c48135a36c2ba7 Author: Jeremy Tan Jie Rui Date: Sat Apr 15 20:36:42 2023 +0000 chore: forward port mathlib#18810, 18798, 18738 (#3443) * `algebra.order.sub.defs`, `data.real.nnreal`: leanprover-community/mathlib#18810, which is itself a backport. Also fixes a docstring typo. * `linear_algebra.matrix.dot_product`: leanprover-community/mathlib#18798 * `data.matrix.basic`: leanprover-community/mathlib#18738 Co-authored-by: Parcly Taxel commit b47a0159a18f774307790ce50f32d6da586df09d Author: Pol_tta Date: Sat Apr 15 09:12:03 2023 +0000 doc: Fix typo in `Data.Seq.Seq` (#3439) commit 768568d3bba544b4bf3f15218fe0134e11343c3a Author: Joël Riou Date: Sat Apr 15 00:49:35 2023 +0000 feat: port CategoryTheory.Subobject.MonoOver (#3423) Co-authored-by: Joël Riou commit 1dbb495df6b83033d2b7af1377247fe82f67aefd Author: Yury G. Kudryashov <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat Apr 15 00:49:34 2023 +0000 feat: port NumberTheory.LucasLehmer (#2988) This generalizes some results from `LeftCancelMonoid` to work around an issue in `LucasLehmer.order_ineq`. Co-authored-by: Yury G. Kudryashov Co-authored-by: Scott Morrison commit ebb08bc20b578320ed80ae5af245cc6233d060fd Author: Anand Rao <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 14 23:46:11 2023 +0000 feat: Port `RingTheory.NonUnitalSubsemiring.Basic` (#1774) Co-authored-by: ART0 <18333981+0Art0@users.noreply.github.com> Co-authored-by: Scott Morrison commit 19be7c22e6d05f2b0cef8943c266f18775af94f0 Author: Eric Wieser Date: Fri Apr 14 22:04:15 2023 +0000 feat: port `pi_fin.reflect` instance (#3430) This was skipped during the initial port of this file. There are some golfing discussions [here on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unquoteExpr.3A.20inst.E2.9C.9D.C2.B2.2E2.20.3A.20Expr/near/349273797) that we could revisit later Co-authored-by: Gabriel Ebner commit 0e46075803b15abf1055d7919f28cec2aebfb9a3 Author: Matthew Robert Ballard Date: Fri Apr 14 16:45:16 2023 +0000 feat: port Topology.Category.Top.EpiMono (#3394) Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: EmilieUthaiwat Co-authored-by: Matthew Ballard Co-authored-by: Scott Morrison commit 81241a1a7e72413c161d02502b72d8528d7c30aa Author: Jason Yuen <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 14 15:26:42 2023 +0000 feat: port Analysis.BoxIntegral.Box.Basic (#2625) Co-authored-by: int-y1 Co-authored-by: Moritz Firsching commit 48b57d7d44d14c2df318020038f521dd91fdaacb Author: Matthew Robert Ballard Date: Fri Apr 14 14:34:45 2023 +0000 feat: port LinearAlgebra.FreeModule.Rank (#3377) This PR also fixes the order of universes in `Cardinal.lift_lift`. Co-authored-by: Matthew Ballard Co-authored-by: ChrisHughes24 commit 9f85ec0f5963674d2390bf03e3213a357f08a090 Author: Kevin Buzzard Date: Fri Apr 14 12:58:18 2023 +0000 fix: OrderedSub should be a Prop (#3436) This mistake was present in mathlib3 too. Co-authored-by: Eric Wieser commit 41678bcaa9b4915b73bd047ddd5140cc06e0279b Author: Jason Yuen Date: Fri Apr 14 12:58:16 2023 +0000 feat: port Order.Filter.ZeroAndBoundedAtFilter (#3435) commit 35c59fda61e50eea83bf2888f2620570bfeab4d7 Author: Joël Riou Date: Fri Apr 14 12:58:15 2023 +0000 feat: port AlgebraicTopology.SplitSimplicialObject (#3432) commit 910241390c801b213a926ef24acbfc9fd8cc0c75 Author: Jeremy Tan Jie Rui Date: Fri Apr 14 12:58:14 2023 +0000 feat: port Analysis.Asymptotics.SuperpolynomialDecay (#3421) Co-authored-by: Parcly Taxel Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: ChrisHughes24 commit d351ee0baca400d35d6da46a53cfa6cd7116ea72 Author: Matej Penciak Date: Fri Apr 14 12:58:13 2023 +0000 feat: port CategoryTheory.Limits.Over (#3172) Co-authored-by: Joël Riou commit 496035552dbac4722dc2bdb21f5c2ab70f632637 Author: Moritz Firsching Date: Mon Feb 27 15:51:11 2023 +0100 naming and misc commit abbda8adf1366ca973cc09d4df27a1fe0d408536 Author: Moritz Firsching Date: Fri Feb 24 15:32:20 2023 +0100 first half fixed commit b6b81aaea72992d50d3ac1caebacfd6a919a8337 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 14 16:15:00 2023 +0200 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit 32a5cae67060d1f87a8b3defe1eb996f884e2c66 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 14 16:15:00 2023 +0200 Initial file copy from mathport commit 6c02a3ae82415738d188941475979e9343277041 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 14 16:15:00 2023 +0200 feat: port CategoryTheory.Bicategory.Free commit f0adc53309047e326413f06945d5a0811f0ac73f Merge: 8ce19a1b 955518b4 Author: Matthew Ballard Date: Fri Mar 10 20:46:39 2023 -0500 Merge branch 'master' into port/CategoryTheory.Bicategory.Free commit 8ce19a1bf847fd9c9a0b882de95216d6c9dd6ac2 Author: Moritz Firsching Date: Mon Feb 27 15:51:11 2023 +0100 naming and misc commit 66d4322fc1a2b17b151298e0168f5e768f98fac7 Author: Moritz Firsching Date: Mon Feb 27 15:15:35 2023 +0100 remove extra line commit d7f5b9f580a9eafebc8ff9ebb3f2ece78e872287 Merge: 2d581ce5 13f9beb8 Author: Moritz Firsching Date: Mon Feb 27 15:12:04 2023 +0100 Merge branch 'master' into port/CategoryTheory.Bicategory.Free commit 2d581ce56eefbe4a32e9a8363a251c469fddab3d Author: Moritz Firsching Date: Fri Feb 24 15:32:20 2023 +0100 first half fixed commit aa4cfbf3664801ac14c00d8dbfb5b059f78a09cd Author: Moritz Firsching Date: Fri Feb 24 14:39:20 2023 +0100 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit ed2d586f305f1f004b3080d7ae1918792c92b2ad Author: Moritz Firsching Date: Fri Feb 24 14:39:20 2023 +0100 Initial file copy from mathport commit bca24d649468bb3ae3b4d74063fa78585810a221 Author: Moritz Firsching Date: Fri Feb 24 14:39:20 2023 +0100 feat: port CategoryTheory.Bicategory.Free commit 483ee10bcf3aa3983112a60a2518ee3428c037bc Author: Moritz Doll Date: Fri Feb 24 13:10:02 2023 +0000 feat: port Topology.UniformSpace.Compact (#2472) commit f816238c933f4dfc7e5432f3a7c02411bd768023 Author: Johan Commelin Date: Fri Feb 24 10:36:03 2023 +0000 chore: bump to nightly-2023-02-23 (#2477) commit 5b1ea1681f68104b15c5c0ec3e35327d78605c44 Author: casavaca <96765450+casavaca@users.noreply.github.com> Date: Fri Feb 24 10:36:02 2023 +0000 feat: Port SetTheory.Cardinal.Divisibility (#2473) Co-authored-by: Moritz Firsching commit 0acf5105282320d724551d246dd74faa7ffb0cd0 Author: Yaël Dillies Date: Fri Feb 24 09:35:39 2023 +0000 feat: `range (f ∘ e) = range f` (#1616) Match https://github.com/leanprover-community/mathlib/pull/18190 commit 5237ddd2dc73d19712bbdb0d6d84626e8c8a9079 Author: casavaca <96765450+casavaca@users.noreply.github.com> Date: Fri Feb 24 08:05:23 2023 +0000 feat: Port SetTheory.Cardinal.Continuum (#2474) commit 185fdccd2d9f5f11b84a2ee7eb5a8d10ed2a3fe2 Author: casavaca <96765450+casavaca@users.noreply.github.com> Date: Fri Feb 24 08:05:22 2023 +0000 feat: Port SetTheory.Ordinal.CantorNormalForm (#2471) commit ae271d489595e6cc1e420407d4fa5587bed2fce4 Author: Adam Topaz Date: Fri Feb 24 08:05:20 2023 +0000 feat: Port CategoryTheory.Adjunction.Mates (#2455) commit 7e1a3e16fa969c41abba8ae6a366eb1064c2ce24 Author: Moritz Firsching Date: Fri Feb 24 07:53:38 2023 +0000 feat: port Data.W.Cardinal (#2465) Co-authored-by: Moritz Firsching commit 19dca4430130b358d8db84efbf1de572c1e89149 Author: Moritz Doll Date: Fri Feb 24 07:37:08 2023 +0000 feat: port Topology.UniformSpace.Equicontinuity (#2457) Co-authored-by: RemyDegenne commit 54b5a3537ec5619b5406474aaf79874598c94b38 Author: Moritz Doll Date: Fri Feb 24 03:17:26 2023 +0000 feat: port Topology.UniformSpace.UniformConvergenceTopology (#2159) Co-authored-by: RemyDegenne commit 334031cc6d28b12de03d754ae63524ff0a4d3d94 Author: Moritz Doll Date: Fri Feb 24 00:08:53 2023 +0000 feat: port LinearAlgebra.LinearPMap (#2422) Co-authored-by: Komyyy commit b7ee6f4ccf2875807a088c35bc2b4fed7cc09b4e Author: Adam Topaz Date: Thu Feb 23 16:09:56 2023 +0000 fix: CategoryTheory.Iso add simps tag (#2421) See zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simps.20.2B.20Trans/near/329103653 commit 58c9e93dac8acba475d872e0ce127d4becf06018 Author: Matthew Robert Ballard Date: Thu Feb 23 15:33:19 2023 +0000 feat: port CategoryTheory.Functor.ReflectsIsomorphisms (#2332) Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Matthew Ballard Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> commit 81b6e873749e3723ac7f888c657676b56a15401f Author: Adam Topaz Date: Thu Feb 23 14:26:58 2023 +0000 fix: Add simps tag to Trans instance for Equiv (#2456) See zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simps.20.2B.20Trans/near/329103653 commit af1d5ba8baa251c18737adf3e3da82e3b5c5f537 Author: Chris Hughes Date: Thu Feb 23 13:50:55 2023 +0000 feat: port SetTheory.Cardinal.Ordinal (#2463) commit b6f441b58401fd2526254cc38ee8616267abf9c3 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu Feb 23 12:36:49 2023 +0000 chore: tidy various files (#2462) commit 41f6ba55a8def258434c3d256d3fedd676b10827 Author: Johan Commelin Date: Thu Feb 23 12:36:48 2023 +0000 feat: port LinearAlgebra.LinearIndependent (#2436) Co-authored-by: Komyyy commit 103beb0e79b3fa2b2b89964a7f6b5fc3b779c41c Author: Matthew Robert Ballard Date: Thu Feb 23 12:36:47 2023 +0000 feat: port CategoryTheory.Functor.EpiMono (#2331) Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Matthew Ballard Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> commit c07df1e9b25eae359d3fa7bb42d8ac8cfd2e0e31 Author: Chris Hughes Date: Thu Feb 23 12:23:46 2023 +0000 feat: port CategoryTheory.Monoidal.Functor (#2445) commit efe30d28b3c6e14401312f8fd54158e3f56bfccf Author: Kevin Buzzard Date: Thu Feb 23 11:26:16 2023 +0000 remove `#lint` commit 400006c7b05251a704c99e091d757bd47b26e9f9 Author: Kevin Buzzard Date: Thu Feb 23 11:25:57 2023 +0000 placate linter commit 53d4e66af0a613de3b2b54b8e73b0269604b9fc7 Author: Kevin Buzzard Date: Thu Feb 23 10:49:05 2023 +0000 update module docstring commit a92c01fe4d6842c57b8364d211860446b02f690f Author: Kevin Buzzard Date: Thu Feb 23 10:25:11 2023 +0000 removing some more primes from structure fields commit 05b51bfce7c185da8fbe90f6d120cb3befacb8c6 Author: Kevin Buzzard Date: Thu Feb 23 10:12:21 2023 +0000 remove "restate_axiom" stuff and remove primes from structure fields commit d39507aec2543ad5f2dae65a17b1df214b6c6230 Author: Kevin Buzzard Date: Thu Feb 23 10:09:13 2023 +0000 fix noisy reassoc commit 8905e3feb805a413ac1eae14ce91ad2adf7c3f62 Author: Kevin Buzzard Date: Thu Feb 23 10:03:15 2023 +0000 fix long lines commit 60987db0c63293ee12ba0a505b5f2f89ede093ec Merge: 22cb2fce 6c48d9a5 Author: Kevin Buzzard Date: Thu Feb 23 10:00:38 2023 +0000 Merge branch 'master' into port/CategoryTheory.Bicategory.Functor commit 22cb2fce5c3fabdf73fffd1ae54e752d254cb870 Author: Kevin Buzzard Date: Mon Feb 20 22:55:52 2023 +0000 compiles (but noisy) commit bbed9597dac14b4c911b4691eb847b9eb0874e40 Author: Kevin Buzzard Date: Mon Feb 20 22:17:01 2023 +0000 lots of progress commit 2ac549969ee4ddc6ee815c19b9f832744b0bbbb6 Merge: 15a5bd26 2c9e6a14 Author: Kevin Buzzard Date: Fri Feb 17 22:57:54 2023 +0000 Merge branch 'port/CategoryTheory.Bicategory.Functor' of github.com:leanprover-community/mathlib4 into port/CategoryTheory.Bicategory.Functor commit 15a5bd26fc4f02d4edc12b0b75216a73454c5128 Author: Kevin Buzzard Date: Fri Feb 17 22:57:48 2023 +0000 minor progress commit 2c9e6a149d70c3bc21f4c209e7cb0a3a56dcf4bb Author: Matthew Ballard Date: Thu Feb 16 13:48:21 2023 -0500 fix align errors; add aligns removed the primes from fields in oplaxfunctor and restate_axiom calls, aligned new names and fixed errors from Lean 3 -> Lean 4 conventions commit 799f9b8a44504104759d415dcfcc53a7ac8eabda Author: Kevin Buzzard Date: Thu Feb 16 06:47:46 2023 +0000 parking for a while commit f4b5f453a88aba632e23a81a821b985a6b24d1f0 Author: Kevin Buzzard Date: Thu Feb 16 06:23:44 2023 +0000 more WIP commit ff654847f23e34c44d8bba58150abbac10e029a6 Author: Kevin Buzzard Date: Thu Feb 16 05:04:05 2023 +0000 WIP commit 1daf2155a15c76b2a12562e4e4e40f7f20ff9fc4 Author: Kevin Buzzard Date: Wed Feb 15 16:15:32 2023 +0000 up to line 276; now taking a break commit 6bc3bc8e45930910a03923f3068cd2b8b09d67f2 Author: Kevin Buzzard Date: Wed Feb 15 15:54:27 2023 +0000 reassoc issue commit b68a41b695cac16e0a9ce07bd9b7815b67ed79d0 Author: Kevin Buzzard Date: Wed Feb 15 14:36:44 2023 +0000 Mathbin -> Mathlib and add (manually) to Mathlib.lean commit 4c805941ae469fad526414ae162dcb7678a82a58 Author: Kevin Buzzard Date: Wed Feb 15 14:13:49 2023 +0000 Initial file copy from mathport commit 9411ae09fd5c7e0aa4de676e0b8c52d9c44df902 Author: Kevin Buzzard Date: Wed Feb 15 14:13:49 2023 +0000 feat: port CategoryTheory.Bicategory.Functor --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Bicategory/Free.lean | 405 ++++++++++++++++++++ 2 files changed, 406 insertions(+) create mode 100644 Mathlib/CategoryTheory/Bicategory/Free.lean diff --git a/Mathlib.lean b/Mathlib.lean index 91c4268a0344f..81bd67cbe1543 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -473,6 +473,7 @@ import Mathlib.CategoryTheory.Balanced import Mathlib.CategoryTheory.Bicategory.Basic import Mathlib.CategoryTheory.Bicategory.Coherence import Mathlib.CategoryTheory.Bicategory.End +import Mathlib.CategoryTheory.Bicategory.Free import Mathlib.CategoryTheory.Bicategory.Functor import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete import Mathlib.CategoryTheory.Bicategory.Strict diff --git a/Mathlib/CategoryTheory/Bicategory/Free.lean b/Mathlib/CategoryTheory/Bicategory/Free.lean new file mode 100644 index 0000000000000..5db66646e49b4 --- /dev/null +++ b/Mathlib/CategoryTheory/Bicategory/Free.lean @@ -0,0 +1,405 @@ +/- +Copyright (c) 2022 Yuma Mizuno. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yuma Mizuno + +! This file was ported from Lean 3 source module category_theory.bicategory.free +! leanprover-community/mathlib commit 3d7987cda72abc473c7cdbbb075170e9ac620042 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.Bicategory.Functor + +/-! +# Free bicategories + +We define the free bicategory over a quiver. In this bicategory, the 1-morphisms are freely +generated by the arrows in the quiver, and the 2-morphisms are freely generated by the formal +identities, the formal unitors, and the formal associators modulo the relation derived from the +axioms of a bicategory. + +## Main definitions + +* `FreeBicategory B`: the free bicategory over a quiver `B`. +* `FreeBicategory.lift F`: the pseudofunctor from `FreeBicategory B` to `C` associated with a + prefunctor `F` from `B` to `C`. +-/ + + +universe w w₁ w₂ v v₁ v₂ u u₁ u₂ + +namespace CategoryTheory + +open Category Bicategory + +open Bicategory + +/-- Free bicategory over a quiver. Its objects are the same as those in the underlying quiver. -/ +def FreeBicategory (B : Type u) := + B +#align category_theory.free_bicategory CategoryTheory.FreeBicategory + +instance (B : Type u) : ∀ [Inhabited B], Inhabited (FreeBicategory B) := by + intro h + exact id h + +namespace FreeBicategory + +section + +variable {B : Type u} [Quiver.{v + 1} B] + +/-- 1-morphisms in the free bicategory. -/ +inductive Hom : B → B → Type max u v + | of {a b : B} (f : a ⟶ b) : Hom a b + | id (a : B) : Hom a a + | comp {a b c : B} (f : Hom a b) (g : Hom b c) : Hom a c +#align category_theory.free_bicategory.hom CategoryTheory.FreeBicategory.Hom + +instance (a b : B) [Inhabited (a ⟶ b)] : Inhabited (Hom a b) := + ⟨Hom.of default⟩ + +instance quiver : Quiver.{max u v + 1} (FreeBicategory B) where + Hom := fun a b : B => Hom a b + +instance categoryStruct : CategoryStruct.{max u v} (FreeBicategory B) where + id := fun a : B => Hom.id a + comp := @fun _ _ _ => Hom.comp + +/-- Representatives of 2-morphisms in the free bicategory. -/ +-- porting note: no such linter +-- @[nolint has_nonempty_instance] +inductive Hom₂ : ∀ {a b : FreeBicategory B}, (a ⟶ b) → (a ⟶ b) → Type max u v + | id {a b} (f : a ⟶ b) : Hom₂ f f + | vcomp {a b} {f g h : a ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h) : Hom₂ f h + | whisker_left {a b c} (f : a ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h) : + Hom₂ (f ≫ g) (f ≫ h)-- `η` cannot be earlier than `h` since it is a recursive argument. + | whisker_right {a b c} {f g : a ⟶ b} (h : b ⟶ c) (η : Hom₂ f g) : Hom₂ (f.comp h) (g.comp h) + | associator {a b c d} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : + Hom₂ ((f ≫ g) ≫ h) (f ≫ (g ≫ h)) + | associator_inv {a b c d} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : + Hom₂ (f ≫ (g ≫ h)) ((f ≫ g) ≫ h) + | right_unitor {a b} (f : a ⟶ b) : Hom₂ (f ≫ (𝟙 b)) f + | right_unitor_inv {a b} (f : a ⟶ b) : Hom₂ f (f ≫ (𝟙 b)) + | left_unitor {a b} (f : a ⟶ b) : Hom₂ ((𝟙 a) ≫ f) f + | left_unitor_inv {a b} (f : a ⟶ b) : Hom₂ f ((𝟙 a) ≫ f) +#align category_theory.free_bicategory.hom₂ CategoryTheory.FreeBicategory.Hom₂ + +section + +-- porting note: commenting out redundant binder annotation update +-- variable {B} + +-- mathport name: vcomp +-- The following notations are only used in the definition of `Rel` to simplify the notation. +local infixr:0 " ≫ " => Hom₂.vcomp + +-- mathport name: id +local notation "𝟙" => Hom₂.id + +-- mathport name: whisker_left +local notation f " ◁ " η => Hom₂.whisker_left f η + +-- mathport name: whisker_right +local notation η " ▷ " h => Hom₂.whisker_right h η + +-- mathport name: associator +local notation "α_" => Hom₂.associator + +-- mathport name: left_unitor +local notation "λ_" => Hom₂.left_unitor + +-- mathport name: right_unitor +local notation "ρ_" => Hom₂.right_unitor + +-- mathport name: associator_inv +local notation "α⁻¹_" => Hom₂.associator_inv + +-- mathport name: left_unitor_inv +local notation "λ⁻¹_" => Hom₂.left_unitor_inv + +-- mathport name: right_unitor_inv +local notation "ρ⁻¹_" => Hom₂.right_unitor_inv + +/-- Relations between 2-morphisms in the free bicategory. -/ +inductive Rel : ∀ {a b : FreeBicategory B} {f g : a ⟶ b}, Hom₂ f g → Hom₂ f g → Prop + | vcomp_right {a b} {f g h : Hom a b} (η : Hom₂ f g) (θ₁ θ₂ : Hom₂ g h) : + Rel θ₁ θ₂ → Rel (η ≫ θ₁) (η ≫ θ₂) + | vcomp_left {a b} {f g h : Hom a b} (η₁ η₂ : Hom₂ f g) (θ : Hom₂ g h) : + Rel η₁ η₂ → Rel (η₁ ≫ θ) (η₂ ≫ θ) + | id_comp {a b} {f g : Hom a b} (η : Hom₂ f g) : Rel (𝟙 f ≫ η) η + | comp_id {a b} {f g : Hom a b} (η : Hom₂ f g) : Rel (η ≫ 𝟙 g) η + | assoc {a b} {f g h i : Hom a b} (η : Hom₂ f g) (θ : Hom₂ g h) (ι : Hom₂ h i) : + Rel ((η ≫ θ) ≫ ι) (η ≫ θ ≫ ι) + | whisker_left {a b c} (f : Hom a b) (g h : Hom b c) (η η' : Hom₂ g h) : + Rel η η' → Rel (f ◁ η) (f ◁ η') + | whisker_left_id {a b c} (f : Hom a b) (g : Hom b c) : Rel (f ◁ 𝟙 g) (𝟙 (f.comp g)) + | whisker_left_comp {a b c} (f : Hom a b) {g h i : Hom b c} (η : Hom₂ g h) (θ : Hom₂ h i) : + Rel (f ◁ η ≫ θ) ((f ◁ η) ≫ f ◁ θ) + | id_whisker_left {a b} {f g : Hom a b} (η : Hom₂ f g) : Rel (Hom.id a ◁ η) (λ_ f ≫ η ≫ λ⁻¹_ g) + | comp_whisker_left {a b c d} (f : Hom a b) (g : Hom b c) {h h' : Hom c d} (η : Hom₂ h h') : + Rel (f.comp g ◁ η) (α_ f g h ≫ (f ◁ g ◁ η) ≫ α⁻¹_ f g h') + | whisker_right {a b c} (f g : Hom a b) (h : Hom b c) (η η' : Hom₂ f g) : + Rel η η' → Rel (η ▷ h) (η' ▷ h) + | id_whisker_right {a b c} (f : Hom a b) (g : Hom b c) : Rel (𝟙 f ▷ g) (𝟙 (f.comp g)) + | comp_whisker_right {a b c} {f g h : Hom a b} (i : Hom b c) (η : Hom₂ f g) (θ : Hom₂ g h) : + Rel ((η ≫ θ) ▷ i) ((η ▷ i) ≫ θ ▷ i) + | whisker_right_id {a b} {f g : Hom a b} (η : Hom₂ f g) : Rel (η ▷ Hom.id b) (ρ_ f ≫ η ≫ ρ⁻¹_ g) + | whisker_right_comp {a b c d} {f f' : Hom a b} (g : Hom b c) (h : Hom c d) (η : Hom₂ f f') : + Rel (η ▷ g.comp h) (α⁻¹_ f g h ≫ ((η ▷ g) ▷ h) ≫ α_ f' g h) + | whisker_assoc {a b c d} (f : Hom a b) {g g' : Hom b c} (η : Hom₂ g g') (h : Hom c d) : + Rel ((f ◁ η) ▷ h) (α_ f g h ≫ (f ◁ η ▷ h) ≫ α⁻¹_ f g' h) + | whisker_exchange {a b c} {f g : Hom a b} {h i : Hom b c} (η : Hom₂ f g) (θ : Hom₂ h i) : + Rel ((f ◁ θ) ≫ η ▷ i) ((η ▷ h) ≫ g ◁ θ) + | associator_hom_inv {a b c d} (f : Hom a b) (g : Hom b c) (h : Hom c d) : + Rel (α_ f g h ≫ α⁻¹_ f g h) (𝟙 ((f.comp g).comp h)) + | associator_inv_hom {a b c d} (f : Hom a b) (g : Hom b c) (h : Hom c d) : + Rel (α⁻¹_ f g h ≫ α_ f g h) (𝟙 (f.comp (g.comp h))) + | left_unitor_hom_inv {a b} (f : Hom a b) : Rel (λ_ f ≫ λ⁻¹_ f) (𝟙 ((Hom.id a).comp f)) + | left_unitor_inv_hom {a b} (f : Hom a b) : Rel (λ⁻¹_ f ≫ λ_ f) (𝟙 f) + | right_unitor_hom_inv {a b} (f : Hom a b) : Rel (ρ_ f ≫ ρ⁻¹_ f) (𝟙 (f.comp (Hom.id b))) + | right_unitor_inv_hom {a b} (f : Hom a b) : Rel (ρ⁻¹_ f ≫ ρ_ f) (𝟙 f) + | pentagon {a b c d e} (f : Hom a b) (g : Hom b c) (h : Hom c d) (i : Hom d e) : + Rel ((α_ f g h ▷ i) ≫ α_ f (g.comp h) i ≫ f ◁ α_ g h i) + (α_ (f.comp g) h i ≫ α_ f g (h.comp i)) + | triangle {a b c} (f : Hom a b) (g : Hom b c) : Rel (α_ f (Hom.id b) g ≫ f ◁ λ_ g) (ρ_ f ▷ g) +#align category_theory.free_bicategory.rel CategoryTheory.FreeBicategory.Rel + +end + +-- porting note: commenting out redundant binder annotation update +-- variable {B} + +instance homCategory (a b : FreeBicategory B) : Category (a ⟶ b) where + Hom f g := Quot (@Rel _ _ a b f g) + id f := Quot.mk Rel (Hom₂.id f) + comp := @fun f g h => Quot.map₂ Hom₂.vcomp Rel.vcomp_right Rel.vcomp_left + id_comp := by + rintro f g ⟨η⟩ + exact Quot.sound (Rel.id_comp η) + comp_id := by + rintro f g ⟨η⟩ + exact Quot.sound (Rel.comp_id η) + assoc := by + rintro f g h i ⟨η⟩ ⟨θ⟩ ⟨ι⟩ + exact Quot.sound (Rel.assoc η θ ι) +#align category_theory.free_bicategory.hom_category CategoryTheory.FreeBicategory.homCategory + +/-- Bicategory structure on the free bicategory. -/ +instance bicategory : Bicategory (FreeBicategory B) where + homCategory := @fun (a b : B) => FreeBicategory.homCategory a b + whiskerLeft := @fun a b c f g h η => Quot.map (Hom₂.whisker_left f) (Rel.whisker_left f g h) η + whiskerLeft_id := @fun a b c f g => Quot.sound (Rel.whisker_left_id f g) + associator := @fun a b c d f g h => + { hom := Quot.mk Rel (Hom₂.associator f g h) + inv := Quot.mk Rel (Hom₂.associator_inv f g h) + hom_inv_id := Quot.sound (Rel.associator_hom_inv f g h) + inv_hom_id := Quot.sound (Rel.associator_inv_hom f g h) } + leftUnitor := @fun a b f => + { hom := Quot.mk Rel (Hom₂.left_unitor f) + inv := Quot.mk Rel (Hom₂.left_unitor_inv f) + hom_inv_id := Quot.sound (Rel.left_unitor_hom_inv f) + inv_hom_id := Quot.sound (Rel.left_unitor_inv_hom f) } + rightUnitor := @fun a b f => + { hom := Quot.mk Rel (Hom₂.right_unitor f) + inv := Quot.mk Rel (Hom₂.right_unitor_inv f) + hom_inv_id := Quot.sound (Rel.right_unitor_hom_inv f) + inv_hom_id := Quot.sound (Rel.right_unitor_inv_hom f) } + whiskerLeft_comp := by + rintro a b c f g h i ⟨η⟩ ⟨θ⟩ + exact Quot.sound (Rel.whisker_left_comp f η θ) + id_whiskerLeft := by + rintro a b f g ⟨η⟩ + exact Quot.sound (Rel.id_whisker_left η) + comp_whiskerLeft := by + rintro a b c d f g h h' ⟨η⟩ + exact Quot.sound (Rel.comp_whisker_left f g η) + whiskerRight := @fun a b c f g η h => Quot.map (Hom₂.whisker_right h) (Rel.whisker_right f g h) η + id_whiskerRight := @fun a b c f g => Quot.sound (Rel.id_whisker_right f g) + comp_whiskerRight := by + rintro a b c f g h ⟨η⟩ ⟨θ⟩ i + exact Quot.sound (Rel.comp_whisker_right i η θ) + whiskerRight_id := by + rintro a b f g ⟨η⟩ + exact Quot.sound (Rel.whisker_right_id η) + whiskerRight_comp := by + rintro a b c d f f' ⟨η⟩ g h + exact Quot.sound (Rel.whisker_right_comp g h η) + whisker_assoc := by + rintro a b c d f g g' ⟨η⟩ h + exact Quot.sound (Rel.whisker_assoc f η h) + whisker_exchange := by + rintro a b c f g h i ⟨η⟩ ⟨θ⟩ + exact Quot.sound (Rel.whisker_exchange η θ) + pentagon := @fun a b c d e f g h i => Quot.sound (Rel.pentagon f g h i) + triangle := @fun a b c f g => Quot.sound (Rel.triangle f g) +#align category_theory.free_bicategory.bicategory CategoryTheory.FreeBicategory.bicategory + +variable {a b c d : FreeBicategory B} + +abbrev Hom₂.mk {f g : a ⟶ b} (η : Hom₂ f g) : f ⟶ g := + Quot.mk Rel η + +@[simp] +theorem mk_vcomp {f g h : a ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h) : + (η.vcomp θ).mk = (η.mk ≫ θ.mk : f ⟶ h) := + rfl +#align category_theory.free_bicategory.mk_vcomp CategoryTheory.FreeBicategory.mk_vcomp + +@[simp] +theorem mk_whisker_left (f : a ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h) : + (Hom₂.whisker_left f η).mk = (f ◁ η.mk : f ≫ g ⟶ f ≫ h) := + rfl +#align category_theory.free_bicategory.mk_whisker_left CategoryTheory.FreeBicategory.mk_whisker_left + +@[simp] +theorem mk_whisker_right {f g : a ⟶ b} (η : Hom₂ f g) (h : b ⟶ c) : + (Hom₂.whisker_right h η).mk = (η.mk ▷ h : f ≫ h ⟶ g ≫ h) := + rfl +#align category_theory.free_bicategory.mk_whisker_right CategoryTheory.FreeBicategory.mk_whisker_right + +variable (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) + +-- Porting note: I can not get this to typecheck, and I don't understand why. +-- theorem id_def : Hom.id a = 𝟙 a := +-- rfl +-- #align category_theory.free_bicategory.id_def CategoryTheory.FreeBicategory.id_def +#noalign category_theory.free_bicategory.id_def + +theorem comp_def : Hom.comp f g = f ≫ g := + rfl +#align category_theory.free_bicategory.comp_def CategoryTheory.FreeBicategory.comp_def + +@[simp] +theorem mk_id : Quot.mk _ (Hom₂.id f) = 𝟙 f := + rfl +#align category_theory.free_bicategory.mk_id CategoryTheory.FreeBicategory.mk_id + +@[simp] +theorem mk_associator_hom : Quot.mk _ (Hom₂.associator f g h) = (α_ f g h).hom := + rfl +#align category_theory.free_bicategory.mk_associator_hom CategoryTheory.FreeBicategory.mk_associator_hom + +@[simp] +theorem mk_associator_inv : Quot.mk _ (Hom₂.associator_inv f g h) = (α_ f g h).inv := + rfl +#align category_theory.free_bicategory.mk_associator_inv CategoryTheory.FreeBicategory.mk_associator_inv + +@[simp] +theorem mk_left_unitor_hom : Quot.mk _ (Hom₂.left_unitor f) = (λ_ f).hom := + rfl +#align category_theory.free_bicategory.mk_left_unitor_hom CategoryTheory.FreeBicategory.mk_left_unitor_hom + +@[simp] +theorem mk_left_unitor_inv : Quot.mk _ (Hom₂.left_unitor_inv f) = (λ_ f).inv := + rfl +#align category_theory.free_bicategory.mk_left_unitor_inv CategoryTheory.FreeBicategory.mk_left_unitor_inv + +@[simp] +theorem mk_right_unitor_hom : Quot.mk _ (Hom₂.right_unitor f) = (ρ_ f).hom := + rfl +#align category_theory.free_bicategory.mk_right_unitor_hom CategoryTheory.FreeBicategory.mk_right_unitor_hom + +@[simp] +theorem mk_right_unitor_inv : Quot.mk _ (Hom₂.right_unitor_inv f) = (ρ_ f).inv := + rfl +#align category_theory.free_bicategory.mk_right_unitor_inv CategoryTheory.FreeBicategory.mk_right_unitor_inv + +/-- Canonical prefunctor from `B` to `free_bicategory B`. -/ +@[simps] +def of : Prefunctor B (FreeBicategory B) where + obj := id + map := @fun _ _ => Hom.of +#align category_theory.free_bicategory.of CategoryTheory.FreeBicategory.of + +end + +section + +variable {B : Type u₁} [Quiver.{v₁ + 1} B] {C : Type u₂} [CategoryStruct.{v₂} C] + +variable (F : Prefunctor B C) + +/-- Auxiliary definition for `lift`. -/ +@[simp] +def liftHom : ∀ {a b : FreeBicategory B}, (a ⟶ b) → (F.obj a ⟶ F.obj b) + | _, _, Hom.of f => F.map f + | _, _, Hom.id a => 𝟙 (F.obj a) + | _, _, Hom.comp f g => liftHom f ≫ liftHom g +#align category_theory.free_bicategory.lift_hom CategoryTheory.FreeBicategory.liftHom + +@[simp] +theorem liftHom_id (a : FreeBicategory B) : liftHom F (𝟙 a) = 𝟙 (F.obj a) := + rfl +#align category_theory.free_bicategory.lift_hom_id CategoryTheory.FreeBicategory.liftHom_id + +@[simp] +theorem liftHom_comp {a b c : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) : + liftHom F (f ≫ g) = liftHom F f ≫ liftHom F g := + rfl +#align category_theory.free_bicategory.lift_hom_comp CategoryTheory.FreeBicategory.liftHom_comp + +end + +section + +variable {B : Type u₁} [Quiver.{v₁ + 1} B] {C : Type u₂} [Bicategory.{w₂, v₂} C] + +variable (F : Prefunctor B C) + +/-- Auxiliary definition for `lift`. -/ +-- @[simp] -- Porting note: adding `@[simp]` causes a PANIC. +def liftHom₂ : ∀ {a b : FreeBicategory B} {f g : a ⟶ b}, Hom₂ f g → (liftHom F f ⟶ liftHom F g) + | _, _, _, _, Hom₂.id _ => 𝟙 _ + | _, _, _, _, Hom₂.associator _ _ _ => (α_ _ _ _).hom + | _, _, _, _, Hom₂.associator_inv _ _ _ => (α_ _ _ _).inv + | _, _, _, _, Hom₂.left_unitor _ => (λ_ _).hom + | _, _, _, _, Hom₂.left_unitor_inv _ => (λ_ _).inv + | _, _, _, _, Hom₂.right_unitor _ => (ρ_ _).hom + | _, _, _, _, Hom₂.right_unitor_inv _ => (ρ_ _).inv + | _, _, _, _, Hom₂.vcomp η θ => liftHom₂ η ≫ liftHom₂ θ + | _, _, _, _, Hom₂.whisker_left f η => liftHom F f ◁ liftHom₂ η + | _, _, _, _, Hom₂.whisker_right h η => liftHom₂ η ▷ liftHom F h +#align category_theory.free_bicategory.lift_hom₂ CategoryTheory.FreeBicategory.liftHom₂ + +attribute [local simp] whisker_exchange + +theorem liftHom₂_congr {a b : FreeBicategory B} {f g : a ⟶ b} {η θ : Hom₂ f g} (H : Rel η θ) : + liftHom₂ F η = liftHom₂ F θ := by induction H <;> (dsimp [liftHom₂]; aesop_cat) +#align category_theory.free_bicategory.lift_hom₂_congr CategoryTheory.FreeBicategory.liftHom₂_congr + +/-- A prefunctor from a quiver `B` to a bicategory `C` can be lifted to a pseudofunctor from +`free_bicategory B` to `C`. +-/ +@[simps] +def lift : Pseudofunctor (FreeBicategory B) C where + obj := F.obj + map := liftHom F + mapId a := Iso.refl _ + mapComp f g := Iso.refl _ + map₂ := Quot.lift (liftHom₂ F) fun η θ H => liftHom₂_congr F H + map₂_id := by aesop_cat + -- Porting note: We'd really prefer not to be doing this by hand. + -- in mathlib3 `tidy` did these inductions for us. + map₂_comp := by + intros a b f g h η θ + apply Quot.rec _ _ η + · intro η + apply Quot.rec _ _ θ + · intro θ; rfl + · intros; rfl + · intros; rfl + -- Porting note: still borked from here. The infoview doesn't update properly for me. + map₂_whisker_left := by + intro a b c f g h η + apply Quot.rec _ _ η + · intros; aesop_cat + · intros; rfl + map₂_whisker_right := by intro _ _ _ _ _ η h; dsimp; apply Quot.rec _ _ η <;> aesop_cat +#align category_theory.free_bicategory.lift CategoryTheory.FreeBicategory.lift + +end + +end FreeBicategory + +end CategoryTheory